Theorems · Theorem · category theory

CategoryTheory.MorphismProperty.locallyCoverDense_forget_of_le

∀ {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],
  K ≤ P.precoverage → (CategoryTheory.MorphismProperty.Over.forget P ⊤ S).LocallyCoverDense (K.toGrothendieck.over S)

Defined in

Mathlib.CategoryTheory.MorphismProperty.CommaSites

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MorphismProperty.IsStableUnderCompositionCategoryTheory.Precoverage.HasIsosCategoryTheory.Precoverage.IsStableUnderBaseChangeCategoryTheory.Precoverage.IsStableUnderCompositionCategoryTheory.Precoverage.HasPullbacks