unitsEndEquivAut — Mathlib

English

Isomorphisms induce isomorphisms between automorphism groups.

Русский

Изоморфизмы порождают изоморфизм между группами автоморфизмов.

LaTeX

$$$\text{autMulEquivOfIso}({X,Y}: C)(h: X \cong Y): Aut(X) \simeq Aut(Y)$$$

Lean4

/-- Units in the monoid of endomorphisms of an object
are (multiplicatively) equivalent to automorphisms of that object.
-/
def unitsEndEquivAut : (End X)ˣ ≃* Aut X where
  toFun f := ⟨f.1, f.2, f.4, f.3⟩
  invFun f := ⟨f.1, f.2, f.4, f.3⟩
  map_mul' f g := by cases f; cases g; rfl

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