Locality conditions on morphism properties #

In this file we define locality conditions on morphism properties in a category. Let K be a precoverage in a category C and P be a morphism property on C that respects isomorphisms.

We say that

P is local at the target if for every f : X ⟶ Y, P holds for f if and only if it holds for the restrictions of f to Uᵢ for a K-cover {Uᵢ} of Y.
P is local at the source if for every f : X ⟶ Y, P holds for f if and only if it holds for the restrictions of f to Uᵢ for a K-cover {Uᵢ} of X.

Implementation details #

The covers appearing in the definitions have index type in the morphism universe of C.

TODOs #

Define source and target local closure of a morphism property.

source

class CategoryTheory.MorphismProperty.IsLocalAtTarget {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) (K : Precoverage C) [K.HasPullbacks] extends P.Respects (CategoryTheory.MorphismProperty.isomorphisms C) :

Prop

A property of morphisms P in C is local at the target with respect to the precoverage K if it respects ismorphisms, and: P holds for f : X ⟶ Y if and only if it holds for the restrictions of f to Uᵢ for a 0-hypercover {Uᵢ} of Y in the precoverage K.

precomp {X Y Z : C} (i : X ⟶ Y) (hi : isomorphisms C i) (f : Y ⟶ Z) (hf : P f) : P (CategoryStruct.comp i f)
postcomp {X Y Z : C} (i : Y ⟶ Z) (hi : isomorphisms C i) (f : X ⟶ Y) (hf : P f) : P (CategoryStruct.comp f i)
pullbackSnd {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover Y) (i : 𝒰.I₀) (hf : P f) : P (Limits.pullback.snd f (𝒰.f i))
If P holds for f : X ⟶ Y, it also holds for f restricted to Uᵢ for any K-cover 𝒰 of Y.
of_zeroHypercover {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover Y) (h : ∀ (i : 𝒰.I₀), P (Limits.pullback.snd f (𝒰.f i))) : P f
If P holds for f restricted to Uᵢ for all i, it also holds for f : X ⟶ Y for any K-cover 𝒰 of Y.

Instances

source

theorem CategoryTheory.MorphismProperty.IsLocalAtTarget.mk_of_iff {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} {K : Precoverage C} [K.HasPullbacks] [P.RespectsIso] (H : ∀ {X Y : C} (f : X ⟶ Y) (𝒰 : K.ZeroHypercover Y), P f ↔ ∀ (i : 𝒰.I₀), P (Limits.pullback.snd f (𝒰.f i))) :

P.IsLocalAtTarget K

source

theorem CategoryTheory.MorphismProperty.IsLocalAtTarget.mk_of_isStableUnderBaseChange {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} {K : Precoverage C} [K.HasPullbacks] [P.IsStableUnderBaseChange] (H : ∀ {X Y : C} (f : X ⟶ Y) (𝒰 : K.ZeroHypercover Y), (∀ (i : 𝒰.I₀), P (Limits.pullback.snd f (𝒰.f i))) → P f) :

P.IsLocalAtTarget K

source

theorem CategoryTheory.MorphismProperty.IsLocalAtTarget.of_le {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} {K L : Precoverage C} [K.HasPullbacks] [L.HasPullbacks] [P.IsLocalAtTarget L] (hle : K ≤ L) :

P.IsLocalAtTarget K

source

instance CategoryTheory.MorphismProperty.IsLocalAtTarget.top {C : Type u} [Category.{v, u} C] {K : Precoverage C} [K.HasPullbacks] :

⊤.IsLocalAtTarget K

source

theorem CategoryTheory.MorphismProperty.IsLocalAtTarget.of_isPullback {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} {K : Precoverage C} [K.HasPullbacks] [P.IsLocalAtTarget K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover Y) {X' : C} (i : 𝒰.I₀) {fst : X' ⟶ X} {snd : X' ⟶ 𝒰.X i} (h : IsPullback fst snd f (𝒰.f i)) (hf : P f) :

P snd

source

theorem CategoryTheory.MorphismProperty.IsLocalAtTarget.iff_of_zeroHypercover {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} {K : Precoverage C} [K.HasPullbacks] [P.IsLocalAtTarget K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover Y) :

P f ↔ ∀ (i : 𝒰.I₀), P (Limits.pullback.snd f (𝒰.f i))

source

instance CategoryTheory.MorphismProperty.IsLocalAtTarget.inf {C : Type u} [Category.{v, u} C] {K : Precoverage C} [K.HasPullbacks] (P Q : MorphismProperty C) [P.IsLocalAtTarget K] [Q.IsLocalAtTarget K] :

(P ⊓ Q).IsLocalAtTarget K

source

theorem CategoryTheory.MorphismProperty.of_zeroHypercover_target {C : Type u} {inst✝ : Category.{v, u} C} {P : MorphismProperty C} {K : Precoverage C} {inst✝¹ : K.HasPullbacks} [self : P.IsLocalAtTarget K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover Y) (h : ∀ (i : 𝒰.I₀), P (Limits.pullback.snd f (𝒰.f i))) :

P f

Alias of CategoryTheory.MorphismProperty.IsLocalAtTarget.of_zeroHypercover.

If P holds for f restricted to Uᵢ for all i, it also holds for f : X ⟶ Y for any K-cover 𝒰 of Y.

source

theorem CategoryTheory.MorphismProperty.iff_of_zeroHypercover_target {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} {K : Precoverage C} [K.HasPullbacks] [P.IsLocalAtTarget K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover Y) :

P f ↔ ∀ (i : 𝒰.I₀), P (Limits.pullback.snd f (𝒰.f i))

Alias of CategoryTheory.MorphismProperty.IsLocalAtTarget.iff_of_zeroHypercover.

source

class CategoryTheory.MorphismProperty.IsLocalAtSource {C : Type u} [Category.{v, u} C] (P : MorphismProperty C) (K : Precoverage C) extends P.Respects (CategoryTheory.MorphismProperty.isomorphisms C) :

Prop

A property of morphisms P in C is local at the source with respect to the precoverage K if it respects ismorphisms, and: P holds for f : X ⟶ Y if and only if it holds for the restrictions of f to Uᵢ for a 0-hypercover {Uᵢ} of X in the precoverage K.

precomp {X Y Z : C} (i : X ⟶ Y) (hi : isomorphisms C i) (f : Y ⟶ Z) (hf : P f) : P (CategoryStruct.comp i f)
postcomp {X Y Z : C} (i : Y ⟶ Z) (hi : isomorphisms C i) (f : X ⟶ Y) (hf : P f) : P (CategoryStruct.comp f i)
comp {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover X) (i : 𝒰.I₀) (hf : P f) : P (CategoryStruct.comp (𝒰.f i) f)
If P holds for f : X ⟶ Y, it also holds for 𝒰.f i ≫ f for any K-cover 𝒰 of X.
of_zeroHypercover {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover X) : (∀ (i : 𝒰.I₀), P (CategoryStruct.comp (𝒰.f i) f)) → P f
If P holds for 𝒰.f i ≫ f for all i, it holds for f : X ⟶ Y for any K-cover 𝒰 of X.