Documentation

TauCeti.LinearAlgebra.Matrix.SpecialLinearGroup.Projective

Extension of scalars for projective special linear groups #

This file defines the map on projective special linear groups induced by a ring homomorphism and proves its identity, composition, and representative formulas.

Main declarations #

source
theorem TauCeti.SpecialLinear.map_center_le_comap_center (n : ℕ) {R : Type v} [CommRing R] {S : Type w} [CommRing S] (f : R →+* S) :
Subgroup.center (Matrix.SpecialLinearGroup (Fin n) R) ≤ Subgroup.comap (Matrix.SpecialLinearGroup.map f) (Subgroup.center (Matrix.SpecialLinearGroup (Fin n) S))

Entrywise application of a ring homomorphism carries the center of a special linear group into the center of the target special linear group.

source
noncomputable def TauCeti.SpecialLinear.projectiveMap (n : ℕ) {R : Type v} [CommRing R] {S : Type w} [CommRing S] (f : R →+* S) :
Matrix.ProjectiveSpecialLinearGroup (Fin n) R →* Matrix.ProjectiveSpecialLinearGroup (Fin n) S

Extension of scalars on projective special linear groups.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.SpecialLinear.projectiveMap_mk (n : ℕ) {R : Type v} [CommRing R] {S : Type w} [CommRing S] (f : R →+* S) (g : Matrix.SpecialLinearGroup (Fin n) R) :
    (projectiveMap n f) ↑g = ↑((Matrix.SpecialLinearGroup.map f) g)

    Extension of scalars on projective special linear groups is computed on representatives by entrywise application of the ring homomorphism.

    source
    @[simp]
    theorem TauCeti.SpecialLinear.projectiveMap_id (n : ℕ) {R : Type v} [CommRing R] :
    projectiveMap n (RingHom.id R) = MonoidHom.id (Matrix.ProjectiveSpecialLinearGroup (Fin n) R)

    Extension of scalars by the identity is the identity on projective special linear groups.

    source
    @[simp]
    theorem TauCeti.SpecialLinear.projectiveMap_comp (n : ℕ) {R : Type v} [CommRing R] {S : Type w} [CommRing S] {T : Type u} [CommRing T] (f : R →+* S) (g : S →+* T) :
    (projectiveMap n g).comp (projectiveMap n f) = projectiveMap n (g.comp f)

    Successive extensions of scalars compose on projective special linear groups.