autIsoFibers — Mathlib

English

There is a natural isomorphism between Aut A and F(A) for Galois objects A, functorially in A. In particular, Aut(A) ≅ F(A) as groups, compatibly with morphisms of Galois objects.

Русский

Для Galois-объектов A существует естественное изоморование автморфизмов Aut(A) и множества F(A), совместимое с морфизмами между объектами.

LaTeX

$$$\\mathrm{Aut}(A) \\cong F(A)\\quad\\text{naturally in }A$$$

Lean4

/-- Functorial isomorphism `Aut A ≅ F.obj A` for Galois objects `A`. -/
noncomputable def autIsoFibers : autGaloisSystem F ⋙ forget GrpCat ≅ incl F ⋙ F' :=
  NatIso.ofComponents (fun A ↦ ((evaluationEquivOfIsGalois F A A.pt).toIso))
    (fun {A B} f ↦ by
      ext (φ : Aut A.obj)
      dsimp
      erw [evaluationEquivOfIsGalois_apply, evaluationEquivOfIsGalois_apply]
      simp [-Hom.comp, ← f.comp])

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