fiber_in_connected_component — Mathlib

English

For X and x ∈ F.obj X there exist Y, i: Y ⟶ X, y ∈ F.obj Y with F.map i y = x and Y connected and Mono i.

Русский

Для X и x ∈ F.obj X существует Y, i: Y ⟶ X, y ∈ F.obj Y такие что F.map i y = x и Y связен, э

LaTeX

$$$\exists Y\; (i\;:\, Y \to X)\; (y:\, F.obj Y),\ F.map i y = x \land IsConnected Y \land Mono i$$$

Lean4

/-- Every element in the fiber of `X` lies in some connected component of `X`. -/
theorem fiber_in_connected_component (X : C) (x : F.obj X) :
    ∃ (Y : C) (i : Y ⟶ X) (y : F.obj Y), F.map i y = x ∧ IsConnected Y ∧ Mono i :=
  by
  obtain ⟨ι, f, g, hl, hc, he⟩ := has_decomp_connected_components X
  let s : Cocone (Discrete.functor f ⋙ F) := F.mapCocone (Cofan.mk X g)
  let s' : IsColimit s := isColimitOfPreserves F hl
  obtain ⟨⟨j⟩, z, h⟩ := Concrete.isColimit_exists_rep _ s' x
  refine ⟨f j, g j, z, ⟨?_, hc j, MonoCoprod.mono_inj _ (Cofan.mk X g) hl j⟩⟩
  subst h
  rfl

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