English
Up to isomorphism, an element of the fiber lies in a unique connected component.
Русский
С учетом изоморфизмов элемент фибера принадлежит уникальной связной компоненте.
LaTeX
$$$\exists f:\, A \cong B,\ F.map f.hom a = b$$$
Lean4
/-- Up to isomorphism an element of the fiber of `X` only lies in one connected component. -/
theorem connected_component_unique {X A B : C} [IsConnected A] [IsConnected B] (a : F.obj A) (b : F.obj B) (i : A ⟶ X)
(j : B ⟶ X) (h : F.map i a = F.map j b) [Mono i] [Mono j] : ∃ (f : A ≅ B), F.map f.hom a = b := by
/- We consider the fiber product of A and B over X. This is a non-empty (because of `h`)
subobject of `A` and `B` and hence isomorphic to `A` and `B` by connectedness. -/
let Y : C := pullback i j
let u : Y ⟶ A := pullback.fst i j
let v : Y ⟶ B := pullback.snd i j
let G := F ⋙ FintypeCat.incl
let e : F.obj Y ≃ { p : F.obj A × F.obj B // F.map i p.1 = F.map j p.2 } := fiberPullbackEquiv F i j
let y : F.obj Y := e.symm ⟨(a, b), h⟩
have hn : IsInitial Y → False := not_initial_of_inhabited F y
have : IsIso u := IsConnected.noTrivialComponent Y u hn
have : IsIso v := IsConnected.noTrivialComponent Y v hn
use (asIso u).symm ≪≫ asIso v
have hu : G.map u y = a :=
by
simp only [u, G, y, e, ← PreservesPullback.iso_hom_fst G, fiberPullbackEquiv, Iso.toEquiv_comp,
Equiv.symm_trans_apply, Iso.toEquiv_symm_fun, types_comp_apply, inv_hom_id_apply]
erw [Types.pullbackIsoPullback_inv_fst_apply (F.map i) (F.map j)]
have hv : G.map v y = b :=
by
simp only [v, G, y, e, ← PreservesPullback.iso_hom_snd G, fiberPullbackEquiv, Iso.toEquiv_comp,
Equiv.symm_trans_apply, Iso.toEquiv_symm_fun, types_comp_apply, inv_hom_id_apply]
erw [Types.pullbackIsoPullback_inv_snd_apply (F.map i) (F.map j)]
rw [← hu, ← hv]
change (F.map u ≫ F.map _) y = F.map v y
simp only [← F.map_comp, Iso.trans_hom, Iso.symm_hom, asIso_inv, asIso_hom, IsIso.hom_inv_id_assoc]
