algConj — Mathlib

English

The construction algConj defines an algebra isomorphism between endomorphism algebras induced by a linear equivalence.

Русский

Конструкция algConj задает изоморфизм алгебр конечномерных эндоморфизмов, индуцируемый линейным эквивалентом.

LaTeX

$$$\text{algConj}(e) : \operatorname{End}_S M_1 \cong_\_{R} \operatorname{End}_S M_2$$$

Lean4

/-- A linear equivalence of two modules induces an equivalence of algebras of their
endomorphisms. -/
@[simps!]
def algConj (e : M₁ ≃ₗ[S] M₂) : Module.End S M₁ ≃ₐ[R] Module.End S M₂
    where
  __ := e.conjRingEquiv
  commutes' := fun _ ↦ by ext; change e.restrictScalars R _ = _; simp

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