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.

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

• 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 : Y ⟶ X} {R : Presieve X} {U : C} {g : U ⟶ X} (hR : R ∈ K.coverings X) (hg : R g) (hf : P f) [Limits.HasPullback f g] : P (Limits.pullback.snd f g)

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

• of_forall_pullbackSnd {X Y : C} {f : Y ⟶ X} {R : Presieve X} (hR : R ∈ K.coverings X) (h : ∀ {U : C} {g : U ⟶ X} [inst : Limits.HasPullback f g], R g → P (Limits.pullback.snd f g)) : P f

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

theorem CategoryTheory.MorphismProperty.IsLocalAtTarget.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⦄ ⦃R : Presieve Y⦄, R ∈ K.coverings Y → (P f ↔ ∀ {U : C} (g : U ⟶ Y) [inst : Limits.HasPullback f g], R g → P (Limits.pullback.snd f g))) : P.IsLocalAtTarget K

theorem CategoryTheory.MorphismProperty.IsLocalAtTarget.iff_of_forall_pullbackSnd {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} {K : Precoverage C} [P.IsLocalAtTarget K] {X Y : C} {R : Presieve Y} (hR : R ∈ K.coverings Y) {f : X ⟶ Y} : P f ↔ ∀ {U : C} (g : U ⟶ Y) [inst : Limits.HasPullback f g], R g → P (Limits.pullback.snd f g)

theorem CategoryTheory.MorphismProperty.IsLocalAtTarget.mk_of_iff_of_zeroHypercover {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_small {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} {K : Precoverage C} [K.HasPullbacks] [P.RespectsIso] [K.Small] (h₁ : ∀ {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover Y), P f → ∀ (i : 𝒰.I₀), P (Limits.pullback.snd f (𝒰.f i))) (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.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} [P.IsLocalAtTarget L] (hle : K ≤ L) : P.IsLocalAtTarget K

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

theorem CategoryTheory.MorphismProperty.IsLocalAtTarget.of_isPullback {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} {K : Precoverage C} [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.of_zeroHypercover {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} {K : Precoverage C} [P.IsLocalAtTarget K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover Y) [K.HasPullbacks] (h : ∀ (i : 𝒰.I₀), P (Limits.pullback.snd f (𝒰.f i))) : P f

theorem CategoryTheory.MorphismProperty.IsLocalAtTarget.iff_of_zeroHypercover {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} {K : Precoverage C} [P.IsLocalAtTarget K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover Y) [K.HasPullbacks] : 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} (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} [P.IsLocalAtTarget K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover Y) [K.HasPullbacks] (h : ∀ (i : 𝒰.I₀), P (Limits.pullback.snd f (𝒰.f i))) : P f

Alias of CategoryTheory.MorphismProperty.IsLocalAtTarget.of_zeroHypercover.

theorem CategoryTheory.MorphismProperty.iff_of_zeroHypercover_target {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} {K : Precoverage C} [P.IsLocalAtTarget K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover Y) [K.HasPullbacks] : 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.

• 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} {R : Presieve X} (hR : R ∈ K.coverings X) {U : C} (g : U ⟶ X) (hg : R g) (hf : P f) : P (CategoryStruct.comp g f)

  If P holds for f : X ⟶ Y, it also holds for 𝒰.f i ≫ f for any K-cover R of X.

• of_forall_comp {X Y : C} {f : X ⟶ Y} {R : Presieve X} (hR : R ∈ K.coverings X) : (∀ ⦃U : C⦄ ⦃g : U ⟶ X⦄, R g → P (CategoryStruct.comp g f)) → P f

  If P holds for 𝒰.f i ≫ f for all i, it holds for f : X ⟶ Y for any K-cover R 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} {R : Presieve X}, R ∈ K.coverings X → (P f ↔ ∀ ⦃U : C⦄ ⦃g : U ⟶ X⦄, R g → P (CategoryStruct.comp g f))) : P.IsLocalAtSource K

theorem CategoryTheory.MorphismProperty.IsLocalAtSource.mk_of_iff_of_zeroHypercover {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.mk_of_small {C : Type u} [Category.{v, u} C] {P : MorphismProperty C} {K : Precoverage C} [P.RespectsIso] [K.Small] (h₁ : ∀ {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover X), P f → ∀ (i : 𝒰.I₀), P (CategoryStruct.comp (𝒰.f i) f)) (h₂ : ∀ {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover X), (∀ (i : 𝒰.I₀), P (CategoryStruct.comp (𝒰.f i) f)) → P 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.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) (h : ∀ (i : 𝒰.I₀), P (CategoryStruct.comp (𝒰.f i) f)) : P f

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) (h : ∀ (i : 𝒰.I₀), P (CategoryStruct.comp (𝒰.f i) f)) : P f

Alias of CategoryTheory.MorphismProperty.IsLocalAtSource.of_zeroHypercover.

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.