homSelfLinearEquivEndMulOpposite — Mathlib

English

There is a canonical linear equivalence between the endomorphisms of G and the opposite End(G) as a module over End(G)ᵐᵒᵖ: (G → G) ≃ₗ[(End G)ᵐᵒᵖ] End(G)ᵐᵒᵖ.

Русский

Существуют канонические линейные эквиваленты между эндоморфизмами G и противоположной End(G) как модулей над End(G)ᵐᵒᵖ: (G → G) ≃ₗ[(End G)ᵐᵒᵖ] End(G)ᵐᵒᵖ.

LaTeX

$$$ (\\,G \\to G\\,) \\cong_{\\mathrm{End}(G)^{\\mathrm{op}}} (\\mathrm{End}(G))^{\\mathrm{op}} $$$

Lean4

/-- `G ⟶ G` and `(End G)ᵐᵒᵖ` are isomorphic as `(End G)ᵐᵒᵖ`-modules. -/
@[simps]
def homSelfLinearEquivEndMulOpposite (G : C) : (G ⟶ G) ≃ₗ[(End G)ᵐᵒᵖ] (End G)ᵐᵒᵖ
    where
  toFun f := ⟨f⟩
  map_add' := by cat_disch
  map_smul' := by cat_disch
  invFun := fun ⟨f⟩ => f
  left_inv := by cat_disch
  right_inv := by cat_disch

Похожие утверждения