isPreconnected_op — Mathlib

English

If J is preconnected, then the opposite category Jᵒᵖ is preconnected as well.

Русский

Если J предсвязан, то и противоположная категория Jᵒᵖ предсвязана.

LaTeX

$$$[\\mathrm{IsPreconnected}(J)] \\Rightarrow \\mathrm{IsPreconnected}(J^{\\mathrm{op}})$$$

Lean4

/-- If `J` is preconnected, then `Jᵒᵖ` is preconnected as well. -/
instance isPreconnected_op [IsPreconnected J] : IsPreconnected Jᵒᵖ where
  iso_constant := fun {α} F X =>
    ⟨NatIso.ofComponents fun Y =>
        eqToIso
          (Discrete.ext
            (Discrete.eq_of_hom
              ((Nonempty.some (IsPreconnected.iso_constant (F.rightOp ⋙ (Discrete.opposite α).functor) (unop X))).app
                  (unop Y)).hom))⟩

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