English
Aut F forms a fundamental group with the automorphism functor on the FintypeCat, compatible with naturality, transitivity, and continuity.
Русский
Aut F образует фундаментальную группу вместе с автоморфизм-функтором на FintypeCat, совместимую с естественностью, транситивностью и непрерывностью.
LaTeX
$$$\text{IsFundamentalGroup}(F, Aut\,F)$$$
Lean4
/-- The category of pointed Galois objects is cofiltered. -/
instance : IsCofilteredOrEmpty (PointedGaloisObject F)
where
cone_objs := fun ⟨A, a, _⟩ ⟨B, b, _⟩ ↦
by
obtain ⟨Z, f, z, hgal, hfz⟩ :=
exists_hom_from_galois_of_fiber F (A ⨯ B) <| (fiberBinaryProductEquiv F A B).symm (a, b)
refine ⟨⟨Z, z, hgal⟩, ⟨f ≫ prod.fst, ?_⟩, ⟨f ≫ prod.snd, ?_⟩, trivial⟩
· simp only [F.map_comp, hfz, FintypeCat.comp_apply, fiberBinaryProductEquiv_symm_fst_apply]
· simp only [F.map_comp, hfz, FintypeCat.comp_apply, fiberBinaryProductEquiv_symm_snd_apply]
cone_maps := fun ⟨A, a, _⟩ ⟨B, b, _⟩ ⟨f, hf⟩ ⟨g, hg⟩ ↦
by
obtain ⟨Z, h, z, hgal, hhz⟩ := exists_hom_from_galois_of_fiber F A a
refine ⟨⟨Z, z, hgal⟩, ⟨h, hhz⟩, hom_ext ?_⟩
apply evaluation_injective_of_isConnected F Z B z
simp [hhz, hf, hg]
