|
| 1 | +/- |
| 2 | +Copyright (c) 2020 Bhavik Mehta. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Bhavik Mehta |
| 5 | +-/ |
| 6 | +import Mathlib.CategoryTheory.Sites.IsSheafFor |
| 7 | +import Mathlib.CategoryTheory.Limits.Shapes.Types |
| 8 | + |
| 9 | +#align_import category_theory.sites.sheaf_of_types from "leanprover-community/mathlib"@"70fd9563a21e7b963887c9360bd29b2393e6225a" |
| 10 | + |
| 11 | +/-! |
| 12 | +# The equalizer diagram sheaf condition for a presieve |
| 13 | +
|
| 14 | +In `Mathlib/CategoryTheory/Sites/IsSheafFor` it is defined what it means for a presheaf to be a |
| 15 | +sheaf *for* a particular presieve. In this file we provide equivalent conditions in terms of |
| 16 | +equalizer diagrams. |
| 17 | +
|
| 18 | +* In `Equalizer.Presieve.sheaf_condition`, the sheaf condition at a presieve is shown to be |
| 19 | + equivalent to that of https://stacks.math.columbia.edu/tag/00VM (and combined with |
| 20 | + `isSheaf_pretopology`, this shows the notions of `IsSheaf` are exactly equivalent.) |
| 21 | +
|
| 22 | +* In `Equalizer.Sieve.equalizer_sheaf_condition`, the sheaf condition at a sieve is shown to be |
| 23 | + equivalent to that of Equation (3) p. 122 in Maclane-Moerdijk [MM92]. |
| 24 | +
|
| 25 | +## References |
| 26 | +
|
| 27 | +* [MM92]: *Sheaves in geometry and logic*, Saunders MacLane, and Ieke Moerdijk: |
| 28 | + Chapter III, Section 4. |
| 29 | +* https://stacks.math.columbia.edu/tag/00VL (sheaves on a pretopology or site) |
| 30 | +
|
| 31 | +-/ |
| 32 | + |
| 33 | + |
| 34 | +universe w v u |
| 35 | + |
| 36 | +namespace CategoryTheory |
| 37 | + |
| 38 | +open Opposite CategoryTheory Category Limits Sieve |
| 39 | + |
| 40 | +namespace Equalizer |
| 41 | + |
| 42 | +variable {C : Type u} [Category.{v} C] (P : Cᵒᵖ ⥤ Type max v u) {X : C} (R : Presieve X) |
| 43 | + (S : Sieve X) |
| 44 | + |
| 45 | +noncomputable section |
| 46 | + |
| 47 | +/-- |
| 48 | +The middle object of the fork diagram given in Equation (3) of [MM92], as well as the fork diagram |
| 49 | +of <https://stacks.math.columbia.edu/tag/00VM>. |
| 50 | +-/ |
| 51 | +def FirstObj : Type max v u := |
| 52 | + ∏ fun f : ΣY, { f : Y ⟶ X // R f } => P.obj (op f.1) |
| 53 | +#align category_theory.equalizer.first_obj CategoryTheory.Equalizer.FirstObj |
| 54 | + |
| 55 | +variable {P R} |
| 56 | + |
| 57 | +-- porting note: added to ease automation |
| 58 | +@[ext] |
| 59 | +lemma FirstObj.ext (z₁ z₂ : FirstObj P R) (h : ∀ (Y : C) (f : Y ⟶ X) |
| 60 | + (hf : R f), (Pi.π _ ⟨Y, f, hf⟩ : FirstObj P R ⟶ _) z₁ = |
| 61 | + (Pi.π _ ⟨Y, f, hf⟩ : FirstObj P R ⟶ _) z₂) : z₁ = z₂ := by |
| 62 | + apply Limits.Types.limit_ext |
| 63 | + rintro ⟨⟨Y, f, hf⟩⟩ |
| 64 | + exact h Y f hf |
| 65 | + |
| 66 | +variable (P R) |
| 67 | + |
| 68 | +/-- Show that `FirstObj` is isomorphic to `FamilyOfElements`. -/ |
| 69 | +@[simps] |
| 70 | +def firstObjEqFamily : FirstObj P R ≅ R.FamilyOfElements P where |
| 71 | + hom t Y f hf := Pi.π (fun f : ΣY, { f : Y ⟶ X // R f } => P.obj (op f.1)) ⟨_, _, hf⟩ t |
| 72 | + inv := Pi.lift fun f x => x _ f.2.2 |
| 73 | +#align category_theory.equalizer.first_obj_eq_family CategoryTheory.Equalizer.firstObjEqFamily |
| 74 | + |
| 75 | +instance : Inhabited (FirstObj P (⊥ : Presieve X)) := |
| 76 | + (firstObjEqFamily P _).toEquiv.inhabited |
| 77 | + |
| 78 | +-- porting note: was not needed in mathlib |
| 79 | +instance : Inhabited (FirstObj P ((⊥ : Sieve X) : Presieve X)) := |
| 80 | + (inferInstance : Inhabited (FirstObj P (⊥ : Presieve X))) |
| 81 | + |
| 82 | +/-- |
| 83 | +The left morphism of the fork diagram given in Equation (3) of [MM92], as well as the fork diagram |
| 84 | +of <https://stacks.math.columbia.edu/tag/00VM>. |
| 85 | +-/ |
| 86 | +def forkMap : P.obj (op X) ⟶ FirstObj P R := |
| 87 | + Pi.lift fun f => P.map f.2.1.op |
| 88 | +#align category_theory.equalizer.fork_map CategoryTheory.Equalizer.forkMap |
| 89 | + |
| 90 | +/-! |
| 91 | +This section establishes the equivalence between the sheaf condition of Equation (3) [MM92] and |
| 92 | +the definition of `IsSheafFor`. |
| 93 | +-/ |
| 94 | + |
| 95 | + |
| 96 | +namespace Sieve |
| 97 | + |
| 98 | +/-- The rightmost object of the fork diagram of Equation (3) [MM92], which contains the data used |
| 99 | +to check a family is compatible. |
| 100 | +-/ |
| 101 | +def SecondObj : Type max v u := |
| 102 | + ∏ fun f : Σ(Y Z : _) (_ : Z ⟶ Y), { f' : Y ⟶ X // S f' } => P.obj (op f.2.1) |
| 103 | +#align category_theory.equalizer.sieve.second_obj CategoryTheory.Equalizer.Sieve.SecondObj |
| 104 | + |
| 105 | +variable {P S} |
| 106 | + |
| 107 | +-- porting note: added to ease automation |
| 108 | +@[ext] |
| 109 | +lemma SecondObj.ext (z₁ z₂ : SecondObj P S) (h : ∀ (Y Z : C) (g : Z ⟶ Y) (f : Y ⟶ X) |
| 110 | + (hf : S.arrows f), (Pi.π _ ⟨Y, Z, g, f, hf⟩ : SecondObj P S ⟶ _) z₁ = |
| 111 | + (Pi.π _ ⟨Y, Z, g, f, hf⟩ : SecondObj P S ⟶ _) z₂) : z₁ = z₂ := by |
| 112 | + apply Limits.Types.limit_ext |
| 113 | + rintro ⟨⟨Y, Z, g, f, hf⟩⟩ |
| 114 | + apply h |
| 115 | + |
| 116 | +variable (P S) |
| 117 | + |
| 118 | +/-- The map `p` of Equations (3,4) [MM92]. -/ |
| 119 | +def firstMap : FirstObj P (S : Presieve X) ⟶ SecondObj P S := |
| 120 | + Pi.lift fun fg => |
| 121 | + Pi.π _ (⟨_, _, S.downward_closed fg.2.2.2.2 fg.2.2.1⟩ : ΣY, { f : Y ⟶ X // S f }) |
| 122 | +#align category_theory.equalizer.sieve.first_map CategoryTheory.Equalizer.Sieve.firstMap |
| 123 | + |
| 124 | +instance : Inhabited (SecondObj P (⊥ : Sieve X)) := |
| 125 | + ⟨firstMap _ _ default⟩ |
| 126 | + |
| 127 | +/-- The map `a` of Equations (3,4) [MM92]. -/ |
| 128 | +def secondMap : FirstObj P (S : Presieve X) ⟶ SecondObj P S := |
| 129 | + Pi.lift fun fg => Pi.π _ ⟨_, fg.2.2.2⟩ ≫ P.map fg.2.2.1.op |
| 130 | +#align category_theory.equalizer.sieve.second_map CategoryTheory.Equalizer.Sieve.secondMap |
| 131 | + |
| 132 | +theorem w : forkMap P (S : Presieve X) ≫ firstMap P S = forkMap P S ≫ secondMap P S := by |
| 133 | + ext |
| 134 | + simp [firstMap, secondMap, forkMap] |
| 135 | +#align category_theory.equalizer.sieve.w CategoryTheory.Equalizer.Sieve.w |
| 136 | + |
| 137 | +/-- |
| 138 | +The family of elements given by `x : FirstObj P S` is compatible iff `firstMap` and `secondMap` |
| 139 | +map it to the same point. |
| 140 | +-/ |
| 141 | +theorem compatible_iff (x : FirstObj P S) : |
| 142 | + ((firstObjEqFamily P S).hom x).Compatible ↔ firstMap P S x = secondMap P S x := by |
| 143 | + rw [Presieve.compatible_iff_sieveCompatible] |
| 144 | + constructor |
| 145 | + · intro t |
| 146 | + apply SecondObj.ext |
| 147 | + intros Y Z g f hf |
| 148 | + simpa [firstMap, secondMap] using t _ g hf |
| 149 | + · intro t Y Z f g hf |
| 150 | + rw [Types.limit_ext_iff'] at t |
| 151 | + simpa [firstMap, secondMap] using t ⟨⟨Y, Z, g, f, hf⟩⟩ |
| 152 | +#align category_theory.equalizer.sieve.compatible_iff CategoryTheory.Equalizer.Sieve.compatible_iff |
| 153 | + |
| 154 | +/-- `P` is a sheaf for `S`, iff the fork given by `w` is an equalizer. -/ |
| 155 | +theorem equalizer_sheaf_condition : |
| 156 | + Presieve.IsSheafFor P (S : Presieve X) ↔ Nonempty (IsLimit (Fork.ofι _ (w P S))) := by |
| 157 | + rw [Types.type_equalizer_iff_unique, |
| 158 | + ← Equiv.forall_congr_left (firstObjEqFamily P (S : Presieve X)).toEquiv.symm] |
| 159 | + simp_rw [← compatible_iff] |
| 160 | + simp only [inv_hom_id_apply, Iso.toEquiv_symm_fun] |
| 161 | + apply ball_congr |
| 162 | + intro x _ |
| 163 | + apply exists_unique_congr |
| 164 | + intro t |
| 165 | + rw [← Iso.toEquiv_symm_fun] |
| 166 | + rw [Equiv.eq_symm_apply] |
| 167 | + constructor |
| 168 | + · intro q |
| 169 | + funext Y f hf |
| 170 | + simpa [firstObjEqFamily, forkMap] using q _ _ |
| 171 | + · intro q Y f hf |
| 172 | + rw [← q] |
| 173 | + simp [firstObjEqFamily, forkMap] |
| 174 | +#align category_theory.equalizer.sieve.equalizer_sheaf_condition CategoryTheory.Equalizer.Sieve.equalizer_sheaf_condition |
| 175 | + |
| 176 | +end Sieve |
| 177 | + |
| 178 | +/-! |
| 179 | +This section establishes the equivalence between the sheaf condition of |
| 180 | +https://stacks.math.columbia.edu/tag/00VM and the definition of `isSheafFor`. |
| 181 | +-/ |
| 182 | + |
| 183 | + |
| 184 | +namespace Presieve |
| 185 | + |
| 186 | +variable [R.hasPullbacks] |
| 187 | + |
| 188 | +/-- The rightmost object of the fork diagram of https://stacks.math.columbia.edu/tag/00VM, which |
| 189 | +contains the data used to check a family of elements for a presieve is compatible. |
| 190 | +-/ |
| 191 | +@[simp] def SecondObj : Type max v u := |
| 192 | + ∏ fun fg : (ΣY, { f : Y ⟶ X // R f }) × ΣZ, { g : Z ⟶ X // R g } => |
| 193 | + haveI := Presieve.hasPullbacks.has_pullbacks fg.1.2.2 fg.2.2.2 |
| 194 | + P.obj (op (pullback fg.1.2.1 fg.2.2.1)) |
| 195 | +#align category_theory.equalizer.presieve.second_obj CategoryTheory.Equalizer.Presieve.SecondObj |
| 196 | + |
| 197 | +/-- The map `pr₀*` of <https://stacks.math.columbia.edu/tag/00VL>. -/ |
| 198 | +def firstMap : FirstObj P R ⟶ SecondObj P R := |
| 199 | + Pi.lift fun fg => |
| 200 | + haveI := Presieve.hasPullbacks.has_pullbacks fg.1.2.2 fg.2.2.2 |
| 201 | + Pi.π _ _ ≫ P.map pullback.fst.op |
| 202 | +#align category_theory.equalizer.presieve.first_map CategoryTheory.Equalizer.Presieve.firstMap |
| 203 | + |
| 204 | +instance [HasPullbacks C] : Inhabited (SecondObj P (⊥ : Presieve X)) := |
| 205 | + ⟨firstMap _ _ default⟩ |
| 206 | + |
| 207 | +/-- The map `pr₁*` of <https://stacks.math.columbia.edu/tag/00VL>. -/ |
| 208 | +def secondMap : FirstObj P R ⟶ SecondObj P R := |
| 209 | + Pi.lift fun fg => |
| 210 | + haveI := Presieve.hasPullbacks.has_pullbacks fg.1.2.2 fg.2.2.2 |
| 211 | + Pi.π _ _ ≫ P.map pullback.snd.op |
| 212 | +#align category_theory.equalizer.presieve.second_map CategoryTheory.Equalizer.Presieve.secondMap |
| 213 | + |
| 214 | +theorem w : forkMap P R ≫ firstMap P R = forkMap P R ≫ secondMap P R := by |
| 215 | + dsimp |
| 216 | + ext fg |
| 217 | + simp only [firstMap, secondMap, forkMap] |
| 218 | + simp only [limit.lift_π, limit.lift_π_assoc, assoc, Fan.mk_π_app] |
| 219 | + haveI := Presieve.hasPullbacks.has_pullbacks fg.1.2.2 fg.2.2.2 |
| 220 | + rw [← P.map_comp, ← op_comp, pullback.condition] |
| 221 | + simp |
| 222 | +#align category_theory.equalizer.presieve.w CategoryTheory.Equalizer.Presieve.w |
| 223 | + |
| 224 | +/-- |
| 225 | +The family of elements given by `x : FirstObj P S` is compatible iff `firstMap` and `secondMap` |
| 226 | +map it to the same point. |
| 227 | +-/ |
| 228 | +theorem compatible_iff (x : FirstObj P R) : |
| 229 | + ((firstObjEqFamily P R).hom x).Compatible ↔ firstMap P R x = secondMap P R x := by |
| 230 | + rw [Presieve.pullbackCompatible_iff] |
| 231 | + constructor |
| 232 | + · intro t |
| 233 | + apply Limits.Types.limit_ext |
| 234 | + rintro ⟨⟨Y, f, hf⟩, Z, g, hg⟩ |
| 235 | + simpa [firstMap, secondMap] using t hf hg |
| 236 | + · intro t Y Z f g hf hg |
| 237 | + rw [Types.limit_ext_iff'] at t |
| 238 | + simpa [firstMap, secondMap] using t ⟨⟨⟨Y, f, hf⟩, Z, g, hg⟩⟩ |
| 239 | +#align category_theory.equalizer.presieve.compatible_iff CategoryTheory.Equalizer.Presieve.compatible_iff |
| 240 | + |
| 241 | +/-- `P` is a sheaf for `R`, iff the fork given by `w` is an equalizer. |
| 242 | +See <https://stacks.math.columbia.edu/tag/00VM>. |
| 243 | +-/ |
| 244 | +theorem sheaf_condition : R.IsSheafFor P ↔ Nonempty (IsLimit (Fork.ofι _ (w P R))) := by |
| 245 | + rw [Types.type_equalizer_iff_unique] |
| 246 | + erw [← Equiv.forall_congr_left (firstObjEqFamily P R).toEquiv.symm] |
| 247 | + simp_rw [← compatible_iff, ← Iso.toEquiv_fun, Equiv.apply_symm_apply] |
| 248 | + apply ball_congr |
| 249 | + intro x _ |
| 250 | + apply exists_unique_congr |
| 251 | + intro t |
| 252 | + rw [Equiv.eq_symm_apply] |
| 253 | + constructor |
| 254 | + · intro q |
| 255 | + funext Y f hf |
| 256 | + simpa [forkMap] using q _ _ |
| 257 | + · intro q Y f hf |
| 258 | + rw [← q] |
| 259 | + simp [forkMap] |
| 260 | +#align category_theory.equalizer.presieve.sheaf_condition CategoryTheory.Equalizer.Presieve.sheaf_condition |
| 261 | + |
| 262 | +end Presieve |
| 263 | + |
| 264 | +end |
| 265 | + |
| 266 | +end Equalizer |
0 commit comments