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.

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 isomorphisms, 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.

For a version of of_zeroHypercover that takes a v-small 0-hypercover in an arbitrary universe, use CategoryTheory.MorphismProperty.of_zeroHypercover_target.

• 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.

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

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

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

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

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

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))

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

theorem CategoryTheory.MorphismProperty.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) [𝒰.Small] (h : ∀ (i : 𝒰.I₀), P (Limits.pullback.snd f (𝒰.f i))) : P f

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.

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 isomorphisms, 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.

For a version of of_zeroHypercover that takes a v-small 0-hypercover in an arbitrary universe, use CategoryTheory.MorphismProperty.of_zeroHypercover_source.

• 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.

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

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

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

theorem CategoryTheory.MorphismProperty.IsLocalAtSource.iff_of_zeroHypercover {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} {K : Precoverage C} [P.IsLocalAtSource K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover X) : P f ↔ ∀ (i : 𝒰.I₀), P (CategoryStruct.comp (𝒰.f i) f)

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

theorem CategoryTheory.MorphismProperty.of_zeroHypercover_source {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} {K : Precoverage C} [P.IsLocalAtSource K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover X) [𝒰.Small] (h : ∀ (i : 𝒰.I₀), P (CategoryStruct.comp (𝒰.f i) f)) : P f

theorem CategoryTheory.MorphismProperty.iff_of_zeroHypercover_source {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} {K : Precoverage C} [P.IsLocalAtSource K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover X) : P f ↔ ∀ (i : 𝒰.I₀), P (CategoryStruct.comp (𝒰.f i) f)

Alias of CategoryTheory.MorphismProperty.IsLocalAtSource.iff_of_zeroHypercover.

theorem CategoryTheory.eq_of_zeroHypercover_target {C : Type u} [Category.{v, u} C] [Limits.HasEqualizers C] [Limits.HasPullbacks C] {X Y S : C} {f g : X ⟶ Y} {s : X ⟶ S} {t : Y ⟶ S} (hf : CategoryStruct.comp f t = s) (hg : CategoryStruct.comp g t = s) {J : Precoverage C} (𝒰 : J.ZeroHypercover S) [J.IsStableUnderBaseChange] [(MorphismProperty.isomorphisms C).IsLocalAtTarget J] (H : ∀ (i : 𝒰.I₀), Limits.pullback.map s (𝒰.f i) t (𝒰.f i) f (CategoryStruct.id (𝒰.X i)) (CategoryStruct.id S) ⋯ ⋯ = Limits.pullback.map s (𝒰.f i) t (𝒰.f i) g (CategoryStruct.id (𝒰.X i)) (CategoryStruct.id S) ⋯ ⋯) : f = g

Let J be a precoverage for which isomorphisms are local at the target. Let f, g : X ⟶ Y be two morphisms over S and 𝒰 a J-cover of S. If for all i, the maps X ×[S] Uᵢ ⟶ Y ×[S] Uᵢ are equal, then f and g are equal.