Theorems · Theorem · category theory

TopCat.binaryCofan_isColimit_iff

∀ {X Y : TopCat} (c : CategoryTheory.Limits.BinaryCofan X Y),
  Nonempty (CategoryTheory.Limits.IsColimit c) ↔
    Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom c.inl) ∧
      Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom c.inr) ∧
        IsCompl (Set.range ⇑(CategoryTheory.ConcreteCategory.hom c.inl))
          (Set.range ⇑(CategoryTheory.ConcreteCategory.hom c.inr))

Defined in

Mathlib.Topology.Category.TopCat.Limits.Products

Cited by

1 results in Mathlib

Foundations

Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound