LeanPool.BruhatTits.Utils.RingHom

def GL.map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) {α : Type u_3} [DecidableEq α] [Fintype α] (g : GL α R) : GL α S

Map an element of GL along a ring homomorphism.

Equations

• «GL».map f g = { val := f.mapMatrix ↑g, inv := f.mapMatrix g.inv, val_inv := ⋯, inv_val := ⋯ }

@[simp]

theorem GL.val_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) {α : Type u_3} [DecidableEq α] [Fintype α] (g : GL α R) : ↑(map f g) = f.mapMatrix ↑g

@[simp]

theorem GL.map_apply {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) {α : Type u_3} [DecidableEq α] [Fintype α] (i j : α) (g : GL α R) : ↑(map f g) i j = f (↑g i j)

theorem GL.map_one {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) {α : Type u_3} [DecidableEq α] [Fintype α] : map f 1 = 1

theorem GL.map_mul {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) {α : Type u_3} [DecidableEq α] [Fintype α] (g h : GL α R) : map f (g * h) = map f g * map f h

theorem GL.map_inv {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) {α : Type u_3} [DecidableEq α] [Fintype α] (g : GL α R) : map f g⁻¹ = (map f g)⁻¹

theorem GL.map_det {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) {α : Type u_3} [DecidableEq α] [Fintype α] (g : GL α R) : Matrix.GeneralLinearGroup.det (map f g) = (Units.map ↑f) (Matrix.GeneralLinearGroup.det g)

theorem GL.map_mul_map_inv {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) {α : Type u_3} [DecidableEq α] [Fintype α] (g : GL α R) : map f g * map f g⁻¹ = 1

theorem GL.map_inv_mul_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) {α : Type u_3} [DecidableEq α] [Fintype α] (g : GL α R) : map f g⁻¹ * map f g = 1

theorem GL.coe_map_mul_map_inv {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) {α : Type u_3} [DecidableEq α] [Fintype α] (g : GL α R) : (↑g).map ⇑f * (↑g)⁻¹.map ⇑f = 1

theorem GL.coe_map_inv_mul_map {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) {α : Type u_3} [DecidableEq α] [Fintype α] (g : GL α R) : (↑g)⁻¹.map ⇑f * (↑g).map ⇑f = 1

theorem GL_map_eq {ι : Type u_4} [DecidableEq ι] [Fintype ι] {R : Type u_5} {S : Type u_6} [CommRing R] [CommRing S] (g : GL ι R) (f : R →+* S) : «GL».map f g = (Matrix.GeneralLinearGroup.map f) g

theorem GL.mem_range_map_iff {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {f : R →+* S} (hf : Function.Injective ⇑f) {ι : Type u_4} [Fintype ι] [DecidableEq ι] (g : GL ι S) : g ∈ Set.range ⇑(Matrix.GeneralLinearGroup.map f) ↔ (∀ (i j : ι), ↑g i j ∈ Set.range ⇑f) ∧ ↑(Matrix.GeneralLinearGroup.det g)⁻¹ ∈ Set.range ⇑f

@[implicit_reducible]

instance instCoeHeadMatrixSubtypeMemSubringLeanPool {K : Type u_4} [CommRing K] (R : Subring K) {α : Type u_5} {β : Type u_6} : CoeHead (Matrix α β ↥R) (Matrix α β K)

Coerce matrices over R to matrices over K.

Equations

• instCoeHeadMatrixSubtypeMemSubringLeanPool R = { coe := fun (g : Matrix α β ↥R) => g.map ⇑R.subtype }

@[implicit_reducible]

instance instCoeHeadGeneralLinearGroupSubtypeMemSubringLeanPool {K : Type u_4} [CommRing K] (R : Subring K) {α : Type u_5} [DecidableEq α] [Fintype α] : CoeHead (GL α ↥R) (GL α K)

Coerce invertible matrices over R to matrices over K.

Equations

• instCoeHeadGeneralLinearGroupSubtypeMemSubringLeanPool R = { coe := fun (g : GL α ↥R) => «GL».map R.subtype g }

@[simp]

theorem Subring.coe_map_mul_map_inv {α : Type u_3} [DecidableEq α] [Fintype α] {K : Type u_4} [CommRing K] (R : Subring K) (g : GL α ↥R) : (↑g).map Subtype.val * (↑g)⁻¹.map Subtype.val = 1

@[simp]

theorem Subring.coe_map_inv_mul_map {α : Type u_3} [DecidableEq α] [Fintype α] {K : Type u_4} [CommRing K] (R : Subring K) (g : GL α ↥R) : (↑g)⁻¹.map Subtype.val * (↑g).map Subtype.val = 1

@[simp]

theorem Subring.coe_det {α : Type u_3} [DecidableEq α] [Fintype α] {K : Type u_4} [CommRing K] (R : Subring K) (g : Matrix α α ↥R) : (g.map Subtype.val).det = ↑g.det