Documentation

Mathlib.CategoryTheory.Sites.Hypercover.Subcanonical

Covers in subcanonical topologies #

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

source
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.

Equations
Instances For
    source
    @[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
    source
    @[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✝
    source
    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
    source
    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.

    Equations
    Instances For
      source
      @[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
      source
      @[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
      source
      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.

      source
      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.