autMulEquivOfIso — Mathlib

English

Isomorphisms of objects induce an isomorphism between their automorphism groups.

Русский

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

LaTeX

$$$\forall h: X \cong Y, Aut(X) \simeq Aut(Y)$$$

Lean4

/-- Isomorphisms induce isomorphisms of the automorphism group -/
def autMulEquivOfIso {X Y : C} (h : X ≅ Y) : Aut X ≃* Aut Y
    where
  toFun x := { hom := h.inv ≫ x.hom ≫ h.hom, inv := h.inv ≫ x.inv ≫ h.hom }
  invFun y := { hom := h.hom ≫ y.hom ≫ h.inv, inv := h.hom ≫ y.inv ≫ h.inv }
  left_inv _ := by cat_disch
  right_inv _ := by cat_disch
  map_mul' := by simp [Aut_mul_def]

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