Change of scalars on general linear groups

Matrix.GeneralLinearGroup.map f : GL n R →* GL n S applies a ring hom f : R →+* S entrywise. Mathlib gives its functoriality (map_id, map_comp, map_comp_apply) but says nothing about injectivity, nor about how the map interacts with the positive-determinant subgroup — both of which a construction transporting a group of matrices along a change of scalars needs.

Main results

• Matrix.GeneralLinearGroup.map_injective: entrywise application of an injective ring hom is injective on general linear groups.
• Matrix.GeneralLinearGroup.map_mem_glpos: a strictly monotone ring hom carries GLPos to GLPos, so a change of scalars restricts to the positive-determinant subgroups.
• Subgroup.map_mapGL: extending a subgroup of SL(n, R) to GL n S and then to GL n T agrees with extending it directly to GL n T.

theorem Matrix.GeneralLinearGroup.map_injective {n : Type u_1} {R : Type u_2} {S : Type u_3} [DecidableEq n] [Fintype n] [CommRing R] [CommRing S] {f : R →+* S} (hf : Function.Injective ⇑f) : Function.Injective ⇑(map f)

Entrywise application of an injective ring hom is injective on GL n. A matrix over R is determined by its image over S, and a unit by its underlying matrix.

theorem Matrix.GeneralLinearGroup.map_mem_glpos {n : Type u_1} {R : Type u_2} {S : Type u_3} [DecidableEq n] [Fintype n] [CommRing R] [CommRing S] [LinearOrder R] [IsStrictOrderedRing R] [LinearOrder S] [IsStrictOrderedRing S] {f : R →+* S} (hf : StrictMono ⇑f) {g : GL n R} (hg : g ∈ GLPos n R) : (map f) g ∈ GLPos n S

A strictly monotone change of scalars restricts to the positive-determinant subgroups.

This is the side condition for cutting Matrix.GeneralLinearGroup.map f down to a homomorphism GLPos n R →* GLPos n S; for f = algebraMap ℚ ℝ the hypothesis is Rat.cast_strictMono. Contrast Matrix.SpecialLinearGroup.toGLPos, which lands in GLPos because the determinant is 1: here it is only positive, and monotonicity of f is what keeps it so.

@[simp]

theorem Subgroup.map_mapGL {n : Type u_1} {R : Type u_2} {S : Type u_3} {T : Type u_4} [DecidableEq n] [Fintype n] [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T] (G : Subgroup (Matrix.SpecialLinearGroup n R)) : map (Matrix.GeneralLinearGroup.map (algebraMap S T)) (map (Matrix.SpecialLinearGroup.mapGL S) G) = map (Matrix.SpecialLinearGroup.mapGL T) G

Extending a subgroup of the special linear group first to S and then to T agrees with extending it directly to T. This is the subgroup form of Matrix.SpecialLinearGroup.map_mapGL, used for instance for integral levels extended to ℚ and then to ℝ.