English
If J and K are equivalent, then preconnectedness is transferred to K.
Русский
Если J и K эквивалентны, предсвязность переносится на K.
LaTeX
$$$\\forall (e:\\, J \\simeq K),\\; IsPreconnected(J) \\Rightarrow IsPreconnected(K).$$$
Lean4
/-- If `J` and `K` are equivalent, then if `J` is preconnected then `K` is as well. -/
theorem isPreconnected_of_equivalent {K : Type u₂} [Category.{v₂} K] [IsPreconnected J] (e : J ≌ K) : IsPreconnected K
where
iso_constant F
k :=
⟨calc
F ≅ e.inverse ⋙ e.functor ⋙ F := (e.invFunIdAssoc F).symm
_ ≅ e.inverse ⋙ (Functor.const J).obj ((e.functor ⋙ F).obj (e.inverse.obj k)) :=
(isoWhiskerLeft e.inverse (isoConstant (e.functor ⋙ F) (e.inverse.obj k)))
_ ≅ e.inverse ⋙ (Functor.const J).obj (F.obj k) :=
(isoWhiskerLeft _ ((F ⋙ Functor.const J).mapIso (e.counitIso.app k)))
_ ≅ (Functor.const K).obj (F.obj k) := NatIso.ofComponents fun _ => Iso.refl _⟩
