Locality conditions on object properties

In this file we define locality conditions on object properties in a category. Let K be a precoverage in a category C and P be an object property that is closed under isomorphisms.

We say that

• P is local if for every X : C, P holds for X if and only if it holds for 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.

class CategoryTheory.ObjectProperty.IsLocal {C : Type u} [Category.{v, u} C] (P : ObjectProperty C) (K : Precoverage C) extends P.IsClosedUnderIsomorphisms : Prop

An object property is local if it holds for X if and only if it holds for all Uᵢ where {Uᵢ} is a K-cover of X.

• of_iso {X Y : C} : ∀ (x : X ≅ Y), P X → P Y
• component {X : C} {R : Presieve X} (hR : R ∈ K.coverings X) {Y : C} (f : Y ⟶ X) (hf : R f) : P X → P Y
• of_presieve {X : C} {R : Presieve X} (hR : R ∈ K.coverings X) (H : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → P Y) : P X

theorem CategoryTheory.ObjectProperty.iff_of_presieve {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {K : Precoverage C} [P.IsLocal K] {X : C} {R : Presieve X} (hR : R ∈ K.coverings X) : P X ↔ ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, R f → P Y

theorem CategoryTheory.ObjectProperty.IsLocal.mk_of_zeroHypercover {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {K : Precoverage C} [P.IsClosedUnderIsomorphisms] (H : ∀ ⦃X : C⦄ (𝒰 : K.ZeroHypercover X), P X ↔ ∀ (i : 𝒰.I₀), P (𝒰.X i)) : P.IsLocal K

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

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

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

theorem CategoryTheory.ObjectProperty.of_zeroHypercover {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {K : Precoverage C} [P.IsLocal K] {X : C} (𝒰 : K.ZeroHypercover X) (h : ∀ (i : 𝒰.I₀), P (𝒰.X i)) : P X

theorem CategoryTheory.ObjectProperty.iff_of_zeroHypercover {C : Type u} [Category.{v, u} C] {P : ObjectProperty C} {K : Precoverage C} [P.IsLocal K] {X : C} (𝒰 : K.ZeroHypercover X) : P X ↔ ∀ (i : 𝒰.I₀), P (𝒰.X i)