Precoverages

A precoverage K on a category C is a set of presieves associated to every object X : C, called "covering presieves". There are no conditions on this set. Common extensions of a precoverage are:

• CategoryTheory.Coverage: A coverage is a precoverage that satisfies a pullback compatibility condition, saying that whenever S is a covering presieve on X and f : Y ⟶ X is a morphism, then there exists some covering sieve T on Y such that T factors through S along f.
• CategoryTheory.Pretopology: If C has pullbacks, a pretopology on C is a precoverage that has isomorphisms and is stable under pullback and refinement.

These two are defined in later files. For precoverages, we define stability conditions:

• CategoryTheory.Precoverage.HasIsos: Singleton presieves by isomorphisms are covering.
• CategoryTheory.Precoverage.IsStableUnderBaseChange: The pullback of a covering presieve is again covering.
• CategoryTheory.Precoverage.IsStableUnderComposition: Refining a covering presieve by covering presieves yields a covering presieve.

structure CategoryTheory.Precoverage (C : Type u_1) [Category.{u_2, u_1} C] : Type (max u_1 u_2)

A precoverage is a collection of covering presieves on every object X : C. See CategoryTheory.Coverage and CategoryTheory.Pretopology for common extensions of this.

• coverings (X : C) : Set (Presieve X)

  The collection of covering presieves for an object X.

theorem CategoryTheory.Precoverage.ext_iff {C : Type u_1} {inst✝ : Category.{u_2, u_1} C} {x y : Precoverage C} : x = y ↔ x.coverings = y.coverings

theorem CategoryTheory.Precoverage.ext {C : Type u_1} {inst✝ : Category.{u_2, u_1} C} {x y : Precoverage C} (coverings : x.coverings = y.coverings) : x = y

instance CategoryTheory.Precoverage.instCoeFunForallSetPresieve {C : Type u} [Category.{v, u} C] : CoeFun (Precoverage C) fun (x : Precoverage C) => (X : C) → Set (Presieve X)

Equations

• CategoryTheory.Precoverage.instCoeFunForallSetPresieve = { coe := CategoryTheory.Precoverage.coverings }

instance CategoryTheory.Precoverage.instPartialOrder {C : Type u} [Category.{v, u} C] : PartialOrder (Precoverage C)

Equations

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

instance CategoryTheory.Precoverage.instMin {C : Type u} [Category.{v, u} C] : Min (Precoverage C)

Equations

• CategoryTheory.Precoverage.instMin = { min := fun (A B : CategoryTheory.Precoverage C) => { coverings := A.coverings ⊓ B.coverings } }

instance CategoryTheory.Precoverage.instMax {C : Type u} [Category.{v, u} C] : Max (Precoverage C)

Equations

• CategoryTheory.Precoverage.instMax = { max := fun (A B : CategoryTheory.Precoverage C) => { coverings := A.coverings ⊔ B.coverings } }

instance CategoryTheory.Precoverage.instSupSet {C : Type u} [Category.{v, u} C] : SupSet (Precoverage C)

Equations

• CategoryTheory.Precoverage.instSupSet = { sSup := fun (A : Set (CategoryTheory.Precoverage C)) => { coverings := ⨆ K ∈ A, K.coverings } }

instance CategoryTheory.Precoverage.instInfSet {C : Type u} [Category.{v, u} C] : InfSet (Precoverage C)

Equations

• CategoryTheory.Precoverage.instInfSet = { sInf := fun (A : Set (CategoryTheory.Precoverage C)) => { coverings := ⨅ K ∈ A, K.coverings } }

instance CategoryTheory.Precoverage.instTop {C : Type u} [Category.{v, u} C] : Top (Precoverage C)

Equations

• CategoryTheory.Precoverage.instTop = { top := { coverings := fun (x : C) => Set.univ } }

instance CategoryTheory.Precoverage.instBot {C : Type u} [Category.{v, u} C] : Bot (Precoverage C)

Equations

• CategoryTheory.Precoverage.instBot = { bot := { coverings := fun (x : C) => ∅ } }

instance CategoryTheory.Precoverage.instCompleteLattice {C : Type u} [Category.{v, u} C] : CompleteLattice (Precoverage C)

Equations

• CategoryTheory.Precoverage.instCompleteLattice = Function.Injective.completeLattice CategoryTheory.Precoverage.coverings ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

class CategoryTheory.Precoverage.HasIsos {C : Type u} [Category.{v, u} C] (J : Precoverage C) : Prop

A precoverage has isomorphisms if singleton presieves by isomorphisms are covering.

• mem_coverings_of_isIso {S T : C} (f : S ⟶ T) [IsIso f] : Presieve.singleton f ∈ J.coverings T

class CategoryTheory.Precoverage.IsStableUnderBaseChange {C : Type u} [Category.{v, u} C] (J : Precoverage C) : Prop

A precoverage is stable under base change if pullbacks of covering presieves are covering presieves. Use Precoverage.mem_coverings_of_isPullback for less universe restrictions. Note: This is stronger than the analogous requirement for a Pretopology, because IsPullback does not imply equality with the (arbitrarily) chosen pullbacks in C.

• mem_coverings_of_isPullback {ι : Type (max u v)} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) (hR : Presieve.ofArrows X f ∈ J.coverings S) {Y : C} (g : Y ⟶ S) {P : ι → C} (p₁ : (i : ι) → P i ⟶ Y) (p₂ : (i : ι) → P i ⟶ X i) (h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)) : Presieve.ofArrows P p₁ ∈ J.coverings Y

class CategoryTheory.Precoverage.IsStableUnderComposition {C : Type u} [Category.{v, u} C] (J : Precoverage C) : Prop

A precoverage is stable under composition if the indexed composition of coverings is again a covering. Use Precoverage.comp_mem_coverings for less universe restrictions. Note: This is stronger than the analogous requirement for a Pretopology, because this is in general not equal to a Presieve.bind.

• comp_mem_coverings {ι : Type (max u v)} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) (hf : Presieve.ofArrows X f ∈ J.coverings S) {σ : ι → Type (max u v)} {Y : (i : ι) → σ i → C} (g : (i : ι) → (j : σ i) → Y i j ⟶ X i) (hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ J.coverings (X i)) : (Presieve.ofArrows (fun (p : (i : ι) × σ i) => Y p.fst p.snd) fun (x : (i : ι) × σ i) => CategoryStruct.comp (g x.fst x.snd) (f x.fst)) ∈ J.coverings S

class CategoryTheory.Precoverage.IsStableUnderSup {C : Type u} [Category.{v, u} C] (J : Precoverage C) : Prop

A precoverage is stable under ⊔ if whenever R and S are coverings, also R ⊔ S is a covering.

• sup_mem_coverings {X : C} {R S : Presieve X} (hR : R ∈ J.coverings X) (hS : S ∈ J.coverings X) : R ⊔ S ∈ J.coverings X

class CategoryTheory.Precoverage.HasPullbacks {C : Type u} [Category.{v, u} C] (J : Precoverage C) : Prop

A precoverage has pullbacks, if every covering presieve has pullbacks along arbitrary morphisms.

• hasPullbacks_of_mem {X Y : C} {R : Presieve Y} (f : X ⟶ Y) (hR : R ∈ J.coverings Y) : R.HasPullbacks f

theorem CategoryTheory.Precoverage.mem_coverings_of_isIso {C : Type u} {inst✝ : Category.{v, u} C} {J : Precoverage C} [self : J.HasIsos] {S T : C} (f : S ⟶ T) [IsIso f] : Presieve.singleton f ∈ J.coverings T

Alias of CategoryTheory.Precoverage.HasIsos.mem_coverings_of_isIso.

theorem CategoryTheory.Precoverage.sup_mem_coverings {C : Type u} {inst✝ : Category.{v, u} C} {J : Precoverage C} [self : J.IsStableUnderSup] {X : C} {R S : Presieve X} (hR : R ∈ J.coverings X) (hS : S ∈ J.coverings X) : R ⊔ S ∈ J.coverings X

Alias of CategoryTheory.Precoverage.IsStableUnderSup.sup_mem_coverings.

theorem CategoryTheory.Precoverage.hasPullbacks_of_mem {C : Type u} {inst✝ : Category.{v, u} C} {J : Precoverage C} [self : J.HasPullbacks] {X Y : C} {R : Presieve Y} (f : X ⟶ Y) (hR : R ∈ J.coverings Y) : R.HasPullbacks f

Alias of CategoryTheory.Precoverage.HasPullbacks.hasPullbacks_of_mem.

theorem CategoryTheory.Precoverage.mem_coverings_of_isPullback {C : Type u} [Category.{v, u} C] {J : Precoverage C} [J.IsStableUnderBaseChange] {ι : Type w} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) (hR : Presieve.ofArrows X f ∈ J.coverings S) {Y : C} (g : Y ⟶ S) {P : ι → C} (p₁ : (i : ι) → P i ⟶ Y) (p₂ : (i : ι) → P i ⟶ X i) (h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)) : Presieve.ofArrows P p₁ ∈ J.coverings Y

theorem CategoryTheory.Precoverage.comp_mem_coverings {C : Type u} [Category.{v, u} C] {J : Precoverage C} [J.IsStableUnderComposition] {ι : Type w} {S : C} {X : ι → C} (f : (i : ι) → X i ⟶ S) (hf : Presieve.ofArrows X f ∈ J.coverings S) {σ : ι → Type w'} {Y : (i : ι) → σ i → C} (g : (i : ι) → (j : σ i) → Y i j ⟶ X i) (hg : ∀ (i : ι), Presieve.ofArrows (Y i) (g i) ∈ J.coverings (X i)) : (Presieve.ofArrows (fun (p : (i : ι) × σ i) => Y p.fst p.snd) fun (x : (i : ι) × σ i) => CategoryStruct.comp (g x.fst x.snd) (f x.fst)) ∈ J.coverings S

instance CategoryTheory.Precoverage.instHasPullbacksOfHasPullbacks {C : Type u} [Category.{v, u} C] (J : Precoverage C) [Limits.HasPullbacks C] : J.HasPullbacks

theorem CategoryTheory.Precoverage.pullbackArrows_mem {C : Type u} [Category.{v, u} C] {J : Precoverage C} [J.IsStableUnderBaseChange] {X Y : C} (f : X ⟶ Y) {R : Presieve Y} (hR : R ∈ J.coverings Y) [R.HasPullbacks f] : Presieve.pullbackArrows f R ∈ J.coverings X

instance CategoryTheory.Precoverage.instHasIsosMin {C : Type u} [Category.{v, u} C] (J K : Precoverage C) [J.HasIsos] [K.HasIsos] : (J ⊓ K).HasIsos

instance CategoryTheory.Precoverage.instIsStableUnderBaseChangeMin {C : Type u} [Category.{v, u} C] (J K : Precoverage C) [J.IsStableUnderBaseChange] [K.IsStableUnderBaseChange] : (J ⊓ K).IsStableUnderBaseChange

instance CategoryTheory.Precoverage.instIsStableUnderCompositionMin {C : Type u} [Category.{v, u} C] (J K : Precoverage C) [J.IsStableUnderComposition] [K.IsStableUnderComposition] : (J ⊓ K).IsStableUnderComposition

instance CategoryTheory.Precoverage.instIsStableUnderSupMin {C : Type u} [Category.{v, u} C] (J K : Precoverage C) [J.IsStableUnderSup] [K.IsStableUnderSup] : (J ⊓ K).IsStableUnderSup

def CategoryTheory.Precoverage.comap {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] (F : Functor C D) (J : Precoverage D) : Precoverage C

If J is a precoverage on D, we obtain a precoverage on C by declaring a presieve on D to be covering if its image under F is.

Equations

• CategoryTheory.Precoverage.comap F J = { coverings := fun (Y : C) (R : CategoryTheory.Presieve Y) => CategoryTheory.Presieve.map F R ∈ J.coverings (F.obj Y) }

@[simp]

theorem CategoryTheory.Precoverage.mem_comap_iff {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] {F : Functor C D} {J : Precoverage D} {X : C} {R : Presieve X} : R ∈ (comap F J).coverings X ↔ Presieve.map F R ∈ J.coverings (F.obj X)

theorem CategoryTheory.Precoverage.comap_inf {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] {F : Functor C D} {J K : Precoverage D} : comap F (J ⊓ K) = comap F J ⊓ comap F K

@[simp]

theorem CategoryTheory.Precoverage.comap_id {C : Type u} [Category.{v, u} C] (K : Precoverage C) : comap (Functor.id C) K = K

instance CategoryTheory.Precoverage.instHasIsosComap {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] {F : Functor C D} {J : Precoverage D} [J.HasIsos] : (comap F J).HasIsos

instance CategoryTheory.Precoverage.instIsStableUnderCompositionComap {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] {F : Functor C D} {J : Precoverage D} [J.IsStableUnderComposition] : (comap F J).IsStableUnderComposition

instance CategoryTheory.Precoverage.instIsStableUnderBaseChangeComapOfPreservesLimitsOfShapeWalkingCospan {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] {F : Functor C D} {J : Precoverage D} [Limits.PreservesLimitsOfShape Limits.WalkingCospan F] [J.IsStableUnderBaseChange] : (comap F J).IsStableUnderBaseChange

instance CategoryTheory.Precoverage.instHasPullbacksComapOfCreatesLimitsOfShapeWalkingCospan {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] {F : Functor C D} {J : Precoverage D} [CreatesLimitsOfShape Limits.WalkingCospan F] [J.HasPullbacks] : (comap F J).HasPullbacks