English
For every j in ConnectedComponents J, the component j.Component is connected; any two objects in that component can be joined by a zigzag of morphisms inside the component.
Русский
Для каждого j из ConnectedComponents J компонент j.Component связна: любые два объекта внутри компонента можно соединить зигзагом морфизмов внутри компонента.
LaTeX
$$$ \\forall j \\in \\mathrm{ConnectedComponents}(J),\\; \\mathrm{IsConnected}(j.\\mathrm{Component}). $$$
Lean4
/-- Each connected component of the category is connected. -/
instance (j : ConnectedComponents J) : IsConnected j.Component := by
-- Show it's connected by constructing a zigzag (in `j.Component`) between any two objects
apply isConnected_of_zigzag
rintro ⟨j₁, hj₁⟩
⟨j₂, rfl⟩
-- We know that the underlying objects j₁ j₂ have some zigzag between them in `J`
have h₁₂ : Zigzag j₁ j₂ := Quotient.exact' hj₁
rcases List.exists_isChain_cons_of_relationReflTransGen h₁₂ with
⟨l, hl₁, hl₂⟩
-- Everything which has a zigzag to j₂ can be lifted to the same component as `j₂`.
let f : ∀ x, Zigzag x j₂ → (ConnectedComponents.mk j₂).Component := fun x h =>
⟨x, Quotient.sound' h⟩
-- Everything in our chosen zigzag from `j₁` to `j₂` has a zigzag to `j₂`.
have hf : ∀ a : J, a ∈ l → Zigzag a j₂ := by
intro i hi
apply hl₁.backwards_cons_induction (fun t => Zigzag t j₂) _ hl₂ _ _ _ (List.mem_of_mem_tail hi)
· intro j k
apply Relation.ReflTransGen.head
· apply Relation.ReflTransGen.refl
refine ⟨l.pmap f hf, ?_, by grind⟩
refine @List.isChain_cons_pmap_of_isChain_cons _ _ Zag _ _ f (fun x y _ _ h => ?_) _ _ h₁₂ hl₁ _
exact zag_of_zag_obj (ConnectedComponents.ι _) h
