English
The linear map associated to toLin' coincides with the matrix linear map after coercion.
Русский
Линейное отображение, связанное с toLin', совпадает с линейным отображением матрицы после переноса по коэффициентам.
LaTeX
$$↑(SpecialLinearGroup.toLin' A) = Matrix.toLin' (↑ₘA)$$
Lean4
/-- An equivalence of groups, from the center of the special linear group to the roots of unity. -/
@[simps]
def center_equiv_rootsOfUnity' (i : n) : center (SpecialLinearGroup n R) ≃* rootsOfUnity (Fintype.card n) R
where
toFun
A :=
haveI : Nonempty n := ⟨i⟩
rootsOfUnity.mkOfPowEq (↑ₘA i i) <|
by
obtain ⟨r, hr, hr'⟩ := mem_center_iff.mp A.property
replace hr' : A.val i i = r := by simp only [← hr', scalar_apply, diagonal_apply_eq]
simp only [hr', hr]
invFun
a :=
⟨⟨a • (1 : Matrix n n R), by aesop⟩, Subgroup.mem_center_iff.mpr fun B ↦ Subtype.val_injective <| by simp [coe_mul]⟩
left_inv
A := by
refine SetCoe.ext <| SetCoe.ext ?_
obtain ⟨r, _, hr⟩ := mem_center_iff.mp A.property
simpa [← hr, Submonoid.smul_def, Units.smul_def] using smul_one_eq_diagonal r
right_inv
a := by
obtain ⟨⟨a, _⟩, ha⟩ := a
exact SetCoe.ext <| Units.ext <| by simp
map_mul' A
B := by
dsimp
ext
simp only [rootsOfUnity.val_mkOfPowEq_coe, Subgroup.coe_mul, Units.val_mul]
rw [← scalar_eq_coe_self_center A i, ← scalar_eq_coe_self_center B i]
simp
