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.{v_1, u_1} C] : Type (max u_1 v_1)

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 {C : Type u_1} {inst✝ : Category.{v_1, u_1} C} {x y : Precoverage C} (coverings : x.coverings = y.coverings) : x = y

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

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

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

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

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

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

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

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

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

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

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

theorem CategoryTheory.Precoverage.hasPairwisePullbacks_of_mem {C : Type u} [Category.{v, u} C] (J : Precoverage C) [J.HasPullbacks] {X : C} {R : Presieve X} (hR : R ∈ J.coverings X) : R.HasPairwisePullbacks

def CategoryTheory.Precoverage.comap {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, 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.

@[simp]

theorem CategoryTheory.Precoverage.mem_comap_iff {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, 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.{v_1, 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

theorem CategoryTheory.Precoverage.comap_comp {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, u_1} D] {E : Type u_2} [Category.{v_2, u_2} E] (F : Functor C D) (G : Functor D E) (J : Precoverage E) : comap (F.comp G) J = comap F (comap G J)

instance CategoryTheory.Precoverage.instHasIsosComap {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{v_1, 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.{v_1, 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.{v_1, 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.{v_1, u_1} D] {F : Functor C D} {J : Precoverage D} [CreatesLimitsOfShape Limits.WalkingCospan F] [J.HasPullbacks] : (comap F J).HasPullbacks

class CategoryTheory.Functor.PreservesPairwisePullbacks {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) {X : C} (R : Presieve X) : Prop

A functor F preserves pairwise pullbacks of a presieve R if for every pair of morphisms f and g in R, the pullback of f and g is preserved by F.

• preservesLimit ⦃Y Z : C⦄ ⦃f : Y ⟶ X⦄ ⦃g : Z ⟶ X⦄ : R f → R g → Limits.PreservesLimit (Limits.cospan f g) F

theorem CategoryTheory.Functor.preservesLimit_cospan_of_mem_presieve {C : Type u_1} {D : Type u_2} {inst✝ : Category.{v_1, u_1} C} {inst✝¹ : Category.{v_2, u_2} D} {F : Functor C D} {X : C} (R : Presieve X) [self : F.PreservesPairwisePullbacks R] ⦃Y Z : C⦄ ⦃f : Y ⟶ X⦄ ⦃g : Z ⟶ X⦄ : R f → R g → Limits.PreservesLimit (Limits.cospan f g) F

Alias of CategoryTheory.Functor.PreservesPairwisePullbacks.preservesLimit.

instance CategoryTheory.instPreservesPairwisePullbacksOfPreservesLimitsOfShapeWalkingCospan {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) [Limits.PreservesLimitsOfShape Limits.WalkingCospan F] {X : C} (R : Presieve X) : F.PreservesPairwisePullbacks R

theorem CategoryTheory.Presieve.HasPairwisePullbacks.map_of_preservesPairwisePullbacks {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (F : Functor C D) {X : C} (R : Presieve X) [F.PreservesPairwisePullbacks R] [R.HasPairwisePullbacks] : (map F R).HasPairwisePullbacks

class CategoryTheory.Precoverage.PullbacksPreservedBy {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (J : Precoverage C) (F : Functor C D) : Prop

Pullbacks are preserved by a functor F : C ⥤ D for the precoverage J on C if F preserves all pairwise pullbacks of presieves in J.

• preservesPairwisePullbacks_of_mem ⦃X : C⦄ ⦃R : Presieve X⦄ : R ∈ J.coverings X → F.PreservesPairwisePullbacks R

theorem CategoryTheory.Precoverage.preservesPairwisePullbacks_of_mem {C : Type u_1} {D : Type u_2} {inst✝ : Category.{v_1, u_1} C} {inst✝¹ : Category.{v_2, u_2} D} {J : Precoverage C} {F : Functor C D} [self : J.PullbacksPreservedBy F] ⦃X : C⦄ ⦃R : Presieve X⦄ : R ∈ J.coverings X → F.PreservesPairwisePullbacks R

Alias of CategoryTheory.Precoverage.PullbacksPreservedBy.preservesPairwisePullbacks_of_mem.

instance CategoryTheory.Precoverage.instPullbacksPreservedByOfPreservesLimitsOfShapeWalkingCospan {C : Type u_1} {D : Type u_2} [Category.{v_1, u_1} C] [Category.{v_2, u_2} D] (J : Precoverage C) (F : Functor C D) [Limits.PreservesLimitsOfShape Limits.WalkingCospan F] : J.PullbacksPreservedBy F