refl_conj — Mathlib

English

For α: X ≅ Y and β: Y ≅ Z, and f ∈ Aut X, conjAut respects composition: α.trans β conjugates to β.conjAut (α.conjAut f).

Русский

Для изоморфизмов α: X ≅ Y, β: Y ≅ Z и автоморфизма f ∈ Aut X отображение conjAut сохраняет композицию: conjAut (α.trans β) f = β.conjAut (α.conjAut f).

LaTeX

$$$\\alpha:\\,X\\cong Y,\\ \\beta:\\,Y\\cong Z,\\ f:\\,Aut(X):\\n\\alpha.\\mathrm{conjAut}(f) = \\beta.\\mathrm{conjAut}(\\alpha.\\mathrm{conjAut}(f))$$$

Lean4

@[simp]
theorem refl_conj (f : End X) : (Iso.refl X).conj f = f := by
  rw [conj_apply, Iso.refl_inv, Iso.refl_hom, Category.id_comp, Category.comp_id]

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