Theorems · Theorem · category theory

factorsThrough_of_pullbackCondition

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor C TopCat) (X : Type w')
  [inst_1 : TopologicalSpace X] {Z B : C} {π : Z ⟶ B} [inst_2 : CategoryTheory.Limits.HasPullback π π]
  [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan π π) G] {a : C(↑(G.obj Z), X)},
  ⇑a ∘ ⇑(CategoryTheory.ConcreteCategory.hom (G.map (CategoryTheory.Limits.pullback.fst π π))) =
      ⇑a ∘ ⇑(CategoryTheory.ConcreteCategory.hom (G.map (CategoryTheory.Limits.pullback.snd π π))) →
    Function.FactorsThrough ⇑a ⇑(CategoryTheory.ConcreteCategory.hom (G.map π))

An auxiliary lemma to that allows us to use IsQuotientMap.lift in the proof of equalizerCondition_yonedaPresheaf.

Defined in

Mathlib.Condensed.TopComparison

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryTopologicalSpaceCategoryTheory.Limits.HasPullbackCategoryTheory.Limits.PreservesLimit