Theorems · Theorem · category theory

CategoryTheory.MorphismProperty.sourceLocalClosure.sourceLocalClosure_iff_of_respectsLeft

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {K : CategoryTheory.Precoverage C}
  {P : CategoryTheory.MorphismProperty C} [P.RespectsIso] [P.RespectsLeft K.morphismProperty] [K.HasIsos]
  [K.IsStableUnderBaseChange] [K.IsStableUnderComposition] [K.HasPullbacks] {X Y : C} {f : X ⟶ Y},
  CategoryTheory.MorphismProperty.sourceLocalClosure K P f ↔
    ∃ R ∈ K.coverings X, ∀ (U : C) (g : U ⟶ X), R g → P (CategoryTheory.CategoryStruct.comp g f)

Defined in

Mathlib.CategoryTheory.MorphismProperty.LocalClosure

Cited by

0 results in Mathlib

Foundations

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

Assumes

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