Entrywise maps of special orthogonal matrices

A ring homomorphism maps a special orthogonal matrix entrywise to a special orthogonal matrix. This expresses the functoriality of special orthogonal groups under coefficient-ring maps and supports their base-change constructions.

Main declarations

• Matrix.SpecialOrthogonalGroup.map: entrywise mapping of special orthogonal matrices.

theorem Matrix.SpecialOrthogonalGroup.map_mem {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u} [CommRing R] {S : Type v} [CommRing S] (f : R →+* S) {M : Matrix n n R} (hM : M ∈ specialOrthogonalGroup n R) : M.map ⇑f ∈ specialOrthogonalGroup n S

A ring homomorphism maps special orthogonal matrices to special orthogonal matrices.

def Matrix.SpecialOrthogonalGroup.map {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u} [CommRing R] {S : Type v} [CommRing S] (f : R →+* S) : ↥(specialOrthogonalGroup n R) →* ↥(specialOrthogonalGroup n S)

A ring homomorphism maps special orthogonal matrices entrywise.

Equations

• Matrix.SpecialOrthogonalGroup.map f = { toFun := fun (M : ↥(Matrix.specialOrthogonalGroup n R)) => ⟨(↑M).map ⇑f, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Matrix.SpecialOrthogonalGroup.coe_map {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u} [CommRing R] {S : Type v} [CommRing S] (f : R →+* S) (M : ↥(specialOrthogonalGroup n R)) : ↑((map f) M) = (↑M).map ⇑f

Entrywise mapping of a special orthogonal matrix has the expected underlying matrix.

theorem Matrix.SpecialOrthogonalGroup.map_apply {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u} [CommRing R] {S : Type v} [CommRing S] (f : R →+* S) (M : ↥(specialOrthogonalGroup n R)) (i j : n) : ↑((map f) M) i j = f (↑M i j)

A coefficient-ring map acts entrywise on special orthogonal matrices.

@[simp]

theorem Matrix.SpecialOrthogonalGroup.map_id {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u} [CommRing R] : map (RingHom.id R) = MonoidHom.id ↥(specialOrthogonalGroup n R)

Mapping coefficients along the identity ring homomorphism is the identity.

@[simp]

theorem Matrix.SpecialOrthogonalGroup.map_comp {n : Type u_1} [Fintype n] [DecidableEq n] {R : Type u} [CommRing R] {S : Type u_2} {T : Type u_3} [CommRing S] [CommRing T] (f : R →+* S) (g : S →+* T) : map (g.comp f) = (map g).comp (map f)

Successive coefficient-ring maps agree with mapping along their composite.