Lean4
/-- `cocone F` is a colimit cocone, i.e. `F` is pro-represented by `incl F`. -/
noncomputable def isColimit : IsColimit (cocone F) :=
by
refine evaluationJointlyReflectsColimits _ (fun X ↦ ?_)
refine Types.FilteredColimit.isColimitOf _ _ ?_ ?_
· intro (x : F.obj X)
obtain ⟨Y, i, y, h1, _, _⟩ := fiber_in_connected_component F X x
obtain ⟨Z, f, z, hgal, hfz⟩ := exists_hom_from_galois_of_fiber F Y y
refine ⟨⟨Z, z, hgal⟩, f ≫ i, ?_⟩
simp only [mapCocone_ι_app, evaluation_obj_map, cocone_app, map_comp, ← h1, FintypeCat.comp_apply, hfz]
· intro ⟨A, a, _⟩ ⟨B, b, _⟩ (u : (A : C) ⟶ X) (v : (B : C) ⟶ X) (h : F.map u a = F.map v b)
obtain ⟨⟨Z, z, _⟩, ⟨f, hf⟩, ⟨g, hg⟩, _⟩ :=
IsFilteredOrEmpty.cocone_objs (C := (PointedGaloisObject F)ᵒᵖ) ⟨{ obj := A, pt := a }⟩ ⟨{ obj := B, pt := b }⟩
refine ⟨⟨{ obj := Z, pt := z }⟩, ⟨f, hf⟩, ⟨g, hg⟩, ?_⟩
apply evaluation_injective_of_isConnected F Z X z
change F.map (f ≫ u) z = F.map (g ≫ v) z
rw [map_comp, FintypeCat.comp_apply, hf, map_comp, FintypeCat.comp_apply, hg, h]
