Defining precoverages via pre-0-hypercovers

A precoverage is a condition on all presieves. In some applications, it is practical to instead define a condition on all pre-0-hypercovers. Such a condition for every object is a pre-0-hypercover family if these conditions are invariant under deduplication.

structure CategoryTheory.PreZeroHypercoverFamily (C : Type u) [Category.{v, u} C] : Type (max (u + 1) (v + 1))

A pre-0-hypercover family on C is a property on the category of pre-0-hypercovers for every X : C that is invariant under deduplication. The data of a pre-0-hypercover family is the same as the data of a precoverage (see: Precoverage.equivPreZeroHypercoverFamily).

• property ⦃X : C⦄ : ObjectProperty (PreZeroHypercover X)

  The condition on pre-0-hypercovers for every object.

• iff_shrink {X : C} {E : PreZeroHypercover X} : self.property E ↔ self.property E.shrink

theorem CategoryTheory.PreZeroHypercoverFamily.ext {C : Type u} {inst✝ : Category.{v, u} C} {x y : PreZeroHypercoverFamily C} (property : x.property = y.property) : x = y

theorem CategoryTheory.PreZeroHypercoverFamily.ext_iff {C : Type u} {inst✝ : Category.{v, u} C} {x y : PreZeroHypercoverFamily C} : x = y ↔ x.property = y.property

instance CategoryTheory.instCoeFunPreZeroHypercoverFamilyForallForallPreZeroHypercoverProp {C : Type u} [Category.{v, u} C] : CoeFun (PreZeroHypercoverFamily C) fun (x : PreZeroHypercoverFamily C) => ⦃X : C⦄ → PreZeroHypercover X → Prop

Equations

• CategoryTheory.instCoeFunPreZeroHypercoverFamilyForallForallPreZeroHypercoverProp = { coe := fun (P : CategoryTheory.PreZeroHypercoverFamily C) => P.property }

inductive CategoryTheory.PreZeroHypercoverFamily.presieve {C : Type u} [Category.{v, u} C] (P : PreZeroHypercoverFamily C) {X : C} : Presieve X → Prop

The induced condition on presieves in C, given by a pre-0-hypercover family.

• mk {C : Type u} [Category.{v, u} C] {P : PreZeroHypercoverFamily C} {X : C} (E : PreZeroHypercover X) : P.property E → P.presieve E.presieve₀

def CategoryTheory.PreZeroHypercoverFamily.precoverage {C : Type u} [Category.{v, u} C] (P : PreZeroHypercoverFamily C) : Precoverage C

The associated precoverage to a pre-0-hypercover family.

Equations

• P.precoverage = { coverings := fun (x : C) (R : CategoryTheory.Presieve x) => P.presieve R }

theorem CategoryTheory.PreZeroHypercoverFamily.mem_precoverage_iff {C : Type u} [Category.{v, u} C] {P : PreZeroHypercoverFamily C} {X : C} {R : Presieve X} : R ∈ P.precoverage.coverings X ↔ ∃ (E : PreZeroHypercover X), P.property E ∧ R = E.presieve₀

@[simp]

theorem CategoryTheory.PreZeroHypercover.presieve₀_mem_precoverage_iff {C : Type u} [Category.{v, u} C] {P : PreZeroHypercoverFamily C} {X : C} {E : PreZeroHypercover X} : E.presieve₀ ∈ P.precoverage.coverings X ↔ P.property E

def CategoryTheory.Precoverage.preZeroHypercoverFamily {C : Type u} [Category.{v, u} C] (K : Precoverage C) : PreZeroHypercoverFamily C

The associated pre-0-hypercover family to a precoverage.

Equations

• K.preZeroHypercoverFamily = { property := fun (X : C) (E : CategoryTheory.PreZeroHypercover X) => E.presieve₀ ∈ K.coverings X, iff_shrink := ⋯ }

@[simp]

theorem CategoryTheory.Precoverage.preZeroHypercoverFamily_property {C : Type u} [Category.{v, u} C] (K : Precoverage C) (X : C) (E : PreZeroHypercover X) : K.preZeroHypercoverFamily.property E = (E.presieve₀ ∈ K.coverings X)

def CategoryTheory.Precoverage.equivPreZeroHypercoverFamily (C : Type u) [Category.{v, u} C] : Precoverage C ≃ PreZeroHypercoverFamily C

Giving a precoverage on a category is the same as giving a predicate on every pre-0-hypercover that is stable under deduplication.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Precoverage.HasIsos.of_preZeroHypercoverFamily {C : Type u} [Category.{v, u} C] {P : PreZeroHypercoverFamily C} (h : ∀ ⦃X Y : C⦄ (f : X ⟶ Y) [IsIso f], P.property (PreZeroHypercover.singleton f)) : P.precoverage.HasIsos

theorem CategoryTheory.Precoverage.IsStableUnderBaseChange.of_preZeroHypercoverFamily_of_isClosedUnderIsomorphisms {C : Type u} [Category.{v, u} C] {P : PreZeroHypercoverFamily C} (h₁ : ∀ {X : C}, P.property.IsClosedUnderIsomorphisms) (h₂ : ∀ {X Y : C} (f : X ⟶ Y) (E : PreZeroHypercover Y) [inst : ∀ (i : E.I₀), Limits.HasPullback f (E.f i)], P.property E → P.property (PreZeroHypercover.pullback₁ f E)) : P.precoverage.IsStableUnderBaseChange

theorem CategoryTheory.Precoverage.IsStableUnderComposition.of_preZeroHypercoverFamily {C : Type u} [Category.{v, u} C] {P : PreZeroHypercoverFamily C} (h : ∀ {X : C} (E : PreZeroHypercover X) (F : (i : E.I₀) → PreZeroHypercover (E.X i)), P.property E → (∀ (i : E.I₀), P.property (F i)) → P.property (E.bind F)) : P.precoverage.IsStableUnderComposition