Local closure of morphism properties

We define the source local closure of a morphism property P w.r.t. a precoverage K as the weakest property containing P that is K-local on the source.

inductive CategoryTheory.MorphismProperty.sourceLocalClosure {C : Type u} [Category.{v, u} C] (K : Precoverage C) (P : MorphismProperty C) : MorphismProperty C

The source-local closure of P along a precoverage K is the weakest property containing P that is local on the source.

• of {C : Type u} [Category.{v, u} C] {K : Precoverage C} {P : MorphismProperty C} {X Y : C} (f : X ⟶ Y) : P f → sourceLocalClosure K P f

  Force P ≤ sourceLocalClosure K P.

• of_iso {C : Type u} [Category.{v, u} C] {K : Precoverage C} {P : MorphismProperty C} {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') (e : Arrow.mk f ≅ Arrow.mk g) : sourceLocalClosure K P f → sourceLocalClosure K P g

  Force RespectsIso.

• comp {C : Type u} [Category.{v, u} C] {K : Precoverage C} {P : MorphismProperty C} {X Y : C} (f : X ⟶ Y) (hf : sourceLocalClosure K P f) (R : Presieve X) (hR : R ∈ K.coverings X) {U : C} (g : U ⟶ X) : R g → sourceLocalClosure K P (CategoryStruct.comp g f)
• of_presieve {C : Type u} [Category.{v, u} C] {K : Precoverage C} {P : MorphismProperty C} {X Y : C} (f : X ⟶ Y) (R : Presieve X) (hR : R ∈ K.coverings X) (h : ∀ (U : C) (g : U ⟶ X), R g → sourceLocalClosure K P (CategoryStruct.comp g f)) : sourceLocalClosure K P f

instance CategoryTheory.MorphismProperty.sourceLocalClosure.instIsLocalAtSource {C : Type u} [Category.{v, u} C] {K : Precoverage C} {P : MorphismProperty C} : (sourceLocalClosure K P).IsLocalAtSource K

theorem CategoryTheory.MorphismProperty.sourceLocalClosure.le {C : Type u} [Category.{v, u} C] {K : Precoverage C} {P : MorphismProperty C} : P ≤ sourceLocalClosure K P

theorem CategoryTheory.MorphismProperty.sourceLocalClosure.le_of_isLocalAtSource {C : Type u} [Category.{v, u} C] {K : Precoverage C} {P Q : MorphismProperty C} (h : P ≤ Q) [Q.IsLocalAtSource K] : sourceLocalClosure K P ≤ Q

instance CategoryTheory.MorphismProperty.sourceLocalClosure.instContainsIdentities {C : Type u} [Category.{v, u} C] {K : Precoverage C} {P : MorphismProperty C} [P.ContainsIdentities] : (sourceLocalClosure K P).ContainsIdentities

instance CategoryTheory.MorphismProperty.sourceLocalClosure.instIsStableUnderBaseChangeOfIsStableUnderBaseChangeOfHasPullbacks {C : Type u} [Category.{v, u} C] {K : Precoverage C} {P : MorphismProperty C} [P.IsStableUnderBaseChange] [K.IsStableUnderBaseChange] [Limits.HasPullbacks C] : (sourceLocalClosure K P).IsStableUnderBaseChange

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