English
Lifting the universe level of morphisms and objects preserves connectedness: if J is connected, then ULiftHom(ULift(J)) is connected.
Русский
Поднятие уровня вселенной морфизмов и объектов сохраняет связность: если J связно, то ULiftHom(ULift(J)) тоже связно.
LaTeX
$$$[\\operatorname{IsConnected}(J)] \\Rightarrow \\operatorname{IsConnected}(\\operatorname{ULiftHom}(\\operatorname{ULift}(J))).$$$
Lean4
/-- Lifting the universe level of morphisms and objects preserves connectedness. -/
instance [hc : IsConnected J] : IsConnected (ULiftHom.{v₂} (ULift.{u₂} J)) :=
by
apply IsConnected.of_induct
· rintro p hj₀ h ⟨j⟩
let p' : Set J := {j : J | p ⟨j⟩}
have hj₀' : Classical.choice hc.is_nonempty ∈ p' :=
by
simp only [p']
exact hj₀
apply induct_on_objects p' hj₀' fun f => h ((ULiftHomULiftCategory.equiv J).functor.map f)
