Covers in subcanonical topologies

In this file we provide API related to covers in subcanonical topologies.

noncomputable def CategoryTheory.GrothendieckTopology.OneHypercover.glueMorphisms {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [J.Subcanonical] {S T : C} (E : J.OneHypercover S) (f : (i : E.I₀) → E.X i ⟶ T) (h : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), CategoryStruct.comp (E.p₁ k) (f i) = CategoryStruct.comp (E.p₂ k) (f j)) : S ⟶ T

Glue a family of morphisms along a 1-hypercover for a subcanonical topology.

@[simp]

theorem CategoryTheory.GrothendieckTopology.OneHypercover.f_glueMorphisms {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [J.Subcanonical] {S T : C} (E : J.OneHypercover S) (f : (i : E.I₀) → E.X i ⟶ T) (h : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), CategoryStruct.comp (E.p₁ k) (f i) = CategoryStruct.comp (E.p₂ k) (f j)) (i : E.I₀) : CategoryStruct.comp (E.f i) (E.glueMorphisms f h) = f i

@[simp]

theorem CategoryTheory.GrothendieckTopology.OneHypercover.f_glueMorphisms_assoc {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [J.Subcanonical] {S T : C} (E : J.OneHypercover S) (f : (i : E.I₀) → E.X i ⟶ T) (h : ∀ ⦃i j : E.I₀⦄ (k : E.I₁ i j), CategoryStruct.comp (E.p₁ k) (f i) = CategoryStruct.comp (E.p₂ k) (f j)) (i : E.I₀) {Z : C} (h✝ : T ⟶ Z) : CategoryStruct.comp (E.f i) (CategoryStruct.comp (E.glueMorphisms f h) h✝) = CategoryStruct.comp (f i) h✝

theorem CategoryTheory.Precoverage.ZeroHypercover.hom_ext {C : Type u} [Category.{v, u} C] {J : Precoverage C} [J.toGrothendieck.Subcanonical] {X Y : C} (𝒰 : J.ZeroHypercover X) {f g : X ⟶ Y} (h : ∀ (i : 𝒰.I₀), CategoryStruct.comp (𝒰.f i) f = CategoryStruct.comp (𝒰.f i) g) : f = g

noncomputable def CategoryTheory.Precoverage.ZeroHypercover.glueMorphisms {C : Type u} [Category.{v, u} C] {J : Precoverage C} [J.toGrothendieck.Subcanonical] {S T : C} (𝒰 : J.ZeroHypercover S) [𝒰.HasPullbacks] (f : (i : 𝒰.I₀) → 𝒰.X i ⟶ T) (hf : ∀ (i j : 𝒰.I₀), CategoryStruct.comp (Limits.pullback.fst (𝒰.f i) (𝒰.f j)) (f i) = CategoryStruct.comp (Limits.pullback.snd (𝒰.f i) (𝒰.f j)) (f j)) : S ⟶ T

Glue morphisms along a 0-hypercover.

@[simp]

theorem CategoryTheory.Precoverage.ZeroHypercover.f_glueMorphisms {C : Type u} [Category.{v, u} C] {J : Precoverage C} [J.toGrothendieck.Subcanonical] {S T : C} (𝒰 : J.ZeroHypercover S) [𝒰.HasPullbacks] (f : (i : 𝒰.I₀) → 𝒰.X i ⟶ T) (hf : ∀ (i j : 𝒰.I₀), CategoryStruct.comp (Limits.pullback.fst (𝒰.f i) (𝒰.f j)) (f i) = CategoryStruct.comp (Limits.pullback.snd (𝒰.f i) (𝒰.f j)) (f j)) (i : 𝒰.I₀) : CategoryStruct.comp (𝒰.f i) (𝒰.glueMorphisms f hf) = f i

@[simp]

theorem CategoryTheory.Precoverage.ZeroHypercover.f_glueMorphisms_assoc {C : Type u} [Category.{v, u} C] {J : Precoverage C} [J.toGrothendieck.Subcanonical] {S T : C} (𝒰 : J.ZeroHypercover S) [𝒰.HasPullbacks] (f : (i : 𝒰.I₀) → 𝒰.X i ⟶ T) (hf : ∀ (i j : 𝒰.I₀), CategoryStruct.comp (Limits.pullback.fst (𝒰.f i) (𝒰.f j)) (f i) = CategoryStruct.comp (Limits.pullback.snd (𝒰.f i) (𝒰.f j)) (f j)) (i : 𝒰.I₀) {Z : C} (h : T ⟶ Z) : CategoryStruct.comp (𝒰.f i) (CategoryStruct.comp (𝒰.glueMorphisms f hf) h) = CategoryStruct.comp (f i) h

instance CategoryTheory.Precoverage.ZeroHypercover.instIsLocalAtTargetIsomorphisms {C : Type u} [Category.{v, u} C] {J : Precoverage C} [J.toGrothendieck.Subcanonical] [Limits.HasPullbacks C] [J.IsStableUnderBaseChange] : (MorphismProperty.isomorphisms C).IsLocalAtTarget J

If J is a subcanonical precoverage, isomorphisms are local on the target for J.

theorem CategoryTheory.Precoverage.ZeroHypercover.isPullback_of_forall_isPullback {C : Type u} [Category.{v, u} C] {J : Precoverage C} [J.toGrothendieck.Subcanonical] [Limits.HasPullbacks C] [J.IsStableUnderBaseChange] {P X Y Z : C} (fst : P ⟶ X) (snd : P ⟶ Y) (f : X ⟶ Z) (g : Y ⟶ Z) (𝒰 : J.ZeroHypercover X) (H : ∀ (i : 𝒰.I₀), IsPullback (Limits.pullback.snd fst (𝒰.f i)) (CategoryStruct.comp (Limits.pullback.fst fst (𝒰.f i)) snd) (CategoryStruct.comp (𝒰.f i) f) g) : IsPullback fst snd f g

To show that

P ---> X
|      |
v      v
Y ---> Z

is a pullback square, it suffices to check that

P ×[X] Uᵢ ---> Uᵢ
   |           |
   v           v
   Y --------> Z

is a pullback square for all Uᵢ in a cover of X for some subcanonical topology.