isProductOfDisjoint — Mathlib

English

If U and V are disjoint (U ∩ V = ∅), then F(U ⊔ V) is the product of F(U) and F(V) in the ambient category; i.e., the pullback (binary) cone is a product cone.

Русский

Если U и V не пересекаются, то F(U ⊔ V) является произведением F(U) и F(V) в данной категории.

LaTeX

$$If U ∩ V = ⊥, then IsLimit (BinaryFan.mk (F.1.map (homOfLE le_sup_left).op) (F.1.map (homOfLE le_sup_right).op))$$

Lean4

/-- If `U, V` are disjoint, then `F(U ⊔ V) = F(U) × F(V)`. -/
def isProductOfDisjoint (h : U ⊓ V = ⊥) :
    IsLimit
      (BinaryFan.mk (F.1.map (homOfLE le_sup_left : _ ⟶ U ⊔ V).op) (F.1.map (homOfLE le_sup_right : _ ⟶ U ⊔ V).op)) :=
  isProductOfIsTerminalIsPullback _ _ _ _ (F.isTerminalOfEqEmpty h) (isLimitPullbackCone F U V)

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