Theorems · Theorem · category theory

CategoryTheory.MorphismProperty.isContinuous_comap_forget

∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.MorphismProperty C} {S : C}
  [P.IsStableUnderComposition] (K : CategoryTheory.Precoverage C) [K.HasIsos] [K.IsStableUnderBaseChange]
  [K.IsStableUnderComposition] [K.HasPullbacks] [CategoryTheory.Limits.HasFiniteWidePullbacks C]
  [P.HasOfPostcompProperty P] [P.IsStableUnderBaseChange] [P.ContainsIdentities],
  K ≤ P.precoverage →
    (CategoryTheory.MorphismProperty.Over.forget P ⊤ S).IsContinuous
      (CategoryTheory.Precoverage.comap
          ((CategoryTheory.MorphismProperty.Over.forget P ⊤ S).comp (CategoryTheory.Over.forget S)) K).toGrothendieck
      (K.toGrothendieck.over S)

Defined in

Mathlib.CategoryTheory.MorphismProperty.CommaSites

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MorphismProperty.IsStableUnderCompositionCategoryTheory.Precoverage.HasIsosCategoryTheory.Precoverage.IsStableUnderBaseChangeCategoryTheory.Precoverage.IsStableUnderCompositionCategoryTheory.Precoverage.HasPullbacksCategoryTheory.Limits.HasFiniteWidePullbacksCategoryTheory.MorphismProperty.HasOfPostcompPropertyCategoryTheory.MorphismProperty.IsStableUnderBaseChangeCategoryTheory.MorphismProperty.ContainsIdentities