[Merged by Bors] - feat(CategoryTheory/Sites): morphisms and homotopies of 1-hypercovers

Mathlib/CategoryTheory/Sites/Grothendieck.lean

@@ -160,6 +160,12 @@ theorem bind_covering {S : Sieve X} {R : ∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S f
     (hR : ∀ ⦃Y⦄ ⦃f : Y ⟶ X⦄ (H : S f), R H ∈ J Y) : Sieve.bind S R ∈ J X :=
   J.transitive hS _ fun _ f hf => superset_covering J (Sieve.le_pullback_bind S R f hf) (hR hf)
 
+lemma bindOfArrows {ι : Type*} {X : C} {Z : ι → C} {f : ∀ i, Z i ⟶ X} {R : ∀ i, Presieve (Z i)}
+    (h : Sieve.ofArrows Z f ∈ J X) (hR : ∀ i, Sieve.generate (R i) ∈ J _) :
+    Sieve.generate (Presieve.bindOfArrows Z f R) ∈ J X := by
+  refine J.superset_covering (Presieve.bind_ofArrows_le_bindOfArrows _ _ _) ?_
+  exact J.bind_covering h fun _ _ _ ↦ J.pullback_stable _ (hR _)
+
 /-- The sieve `S` on `X` `J`-covers an arrow `f` to `X` if `S.pullback f ∈ J Y`.
 This definition is an alternate way of presenting a Grothendieck topology.
 -/

Mathlib/CategoryTheory/Sites/OneHypercover.lean

@@ -22,7 +22,7 @@ identifies to the multiequalizer of suitable maps
 
 -/
 
-universe w v u
+universe w' w v u
 
 namespace CategoryTheory
 
@@ -139,6 +139,221 @@ def multifork (F : Cᵒᵖ ⥤ A) :
     dsimp
     simp only [← F.map_comp, ← op_comp, E.w])
 
+section Category
+
+/-- A morphism of pre-`1`-hypercovers of `S` is a family of refinement morphisms commuting
+with the structure morphisms of `E` and `F`. -/
+@[ext]
+structure Hom (E F : PreOneHypercover S) where
+  /-- The map between indexing types of the coverings of `S` -/
+  s₀ (i : E.I₀) : F.I₀
+  /-- The map between indexing types of the coverings of the fibre products over `S`. -/
+  s₁ {i j : E.I₀} (k : E.I₁ i j) : F.I₁ (s₀ i) (s₀ j)
+  /-- The refinement morphisms between objects in the coverings of `S`. -/
+  h₀ (i : E.I₀) : E.X i ⟶ F.X (s₀ i)
+  /-- The refinement morphisms between objects in the coverings of the fibre products over `S`. -/
+  h₁ {i j : E.I₀} (k : E.I₁ i j) : E.Y k ⟶ F.Y (s₁ k)
+  w₀ (i : E.I₀) : h₀ i ≫ F.f (s₀ i) = E.f i := by aesop_cat
+  w₁₁ {i j : E.I₀} (k : E.I₁ i j) : h₁ k ≫ F.p₁ (s₁ k) = E.p₁ k ≫ h₀ i := by aesop_cat
+  w₁₂ {i j : E.I₀} (k : E.I₁ i j) : h₁ k ≫ F.p₂ (s₁ k) = E.p₂ k ≫ h₀ j := by aesop_cat
+
+attribute [reassoc (attr := simp)] Hom.w₀
+attribute [reassoc] Hom.w₁₁ Hom.w₁₂
+
+/-- The identity refinement of a pre-`1`-hypercover. -/
+@[simps]
+def Hom.id (E : PreOneHypercover S) : Hom E E where
+  s₀ := _root_.id
+  s₁ := _root_.id
+  h₀ _ := 𝟙 _
+  h₁ _ := 𝟙 _
+
+variable {E : PreOneHypercover.{w} S} {F : PreOneHypercover.{w'} S}
+  {G : PreOneHypercover S}
+
+/-- Composition of refinement morphisms of pre-`1`-hypercovers. -/
+@[simps]
+def Hom.comp (f : E.Hom F) (g : F.Hom G) : E.Hom G where
+  s₀ := g.s₀ ∘ f.s₀
+  s₁ := g.s₁ ∘ f.s₁
+  h₀ i := f.h₀ i ≫ g.h₀ _
+  h₁ i := f.h₁ i ≫ g.h₁ _
+  w₁₁ := by simp [w₁₁, w₁₁_assoc]
+  w₁₂ := by simp [w₁₂, w₁₂_assoc]
+
+/-- The induced index map `E.I₁' → F.I₁'` from a refinement morphism `E ⟶ F`. -/
+@[simp]
+def Hom.s₁' (f : E.Hom F) (k : E.I₁') : F.I₁' :=
+  ⟨⟨f.s₀ k.1.1, f.s₀ k.1.2⟩, f.s₁ k.2⟩
+
+@[simps! id_s₀ id_s₁ id_h₀ id_h₁ comp_s₀ comp_s₁ comp_h₀ comp_h₁]
+instance : Category (PreOneHypercover S) where
+  Hom := Hom
+  id E := Hom.id E
+  comp f g := f.comp g
+
+/-- A homotopy of refinements `E ⟶ F` is a family of morphisms `Xᵢ ⟶ Yₐ` where
+`Yₐ` is a component of the cover of `X_{f(i)} ×[S] X_{g(i)}`. -/
+structure Homotopy (f g : E.Hom F) where
+  /-- The index map sending `i : E.I₀` to `a` above `(f(i), g(i))`. -/
+  H (i : E.I₀) : F.I₁ (f.s₀ i) (g.s₀ i)
+  /-- The morphism `Xᵢ ⟶ Yₐ`. -/
+  a (i : E.I₀) : E.X i ⟶ F.Y (H i)
+  wl (i : E.I₀) : a i ≫ F.p₁ (H i) = f.h₀ i
+  wr (i : E.I₀) : a i ≫ F.p₂ (H i) = g.h₀ i
+
+attribute [reassoc (attr := simp)] Homotopy.wl Homotopy.wr
+
+/-- A refinement morphism `E ⟶ F` induces a morphism on associated multiequalizers. -/
+def Hom.mapMultiforkOfIsLimit (f : E.Hom F) (P : Cᵒᵖ ⥤ A) {c : Multifork (E.multicospanIndex P)}
+    (hc : IsLimit c) (d : Multifork (F.multicospanIndex P)) :
+    d.pt ⟶ c.pt :=
+  Multifork.IsLimit.lift hc (fun a ↦ d.ι (f.s₀ a) ≫ P.map (f.h₀ a).op) <| by
+    intro (k : E.I₁')
+    simp only [multicospanIndex_right, multicospanShape_fst, multicospanIndex_left,
+      multicospanIndex_fst, assoc, multicospanShape_snd, multicospanIndex_snd]
+    have heq := d.condition (f.s₁' k)
+    simp only [Hom.s₁', multicospanIndex_right, multicospanShape_fst, multicospanIndex_left,
+      multicospanIndex_fst, multicospanShape_snd, multicospanIndex_snd] at heq
+    rw [← Functor.map_comp, ← op_comp, ← Hom.w₁₁, ← Functor.map_comp, ← op_comp, ← Hom.w₁₂]
+    rw [op_comp, Functor.map_comp, reassoc_of% heq, op_comp, Functor.map_comp]
+
+@[reassoc (attr := simp)]
+lemma Hom.mapMultiforkOfIsLimit_ι {E F : PreOneHypercover.{w} S}
+    (f : E.Hom F) (P : Cᵒᵖ ⥤ A) {c : Multifork (E.multicospanIndex P)} (hc : IsLimit c)
+    (d : Multifork (F.multicospanIndex P)) (a : E.I₀) :
+    f.mapMultiforkOfIsLimit P hc d ≫ c.ι a = d.ι (f.s₀ a) ≫ P.map (f.h₀ a).op := by
+  simp [mapMultiforkOfIsLimit]
+
+/-- Homotopic refinements induce the same map on multiequalizers. -/
+lemma Homotopy.mapMultiforkOfIsLimit_eq {E F : PreOneHypercover.{w} S}
+    {f g : E.Hom F} (H : Homotopy f g)
+    (P : Cᵒᵖ ⥤ A) {c : Multifork (E.multicospanIndex P)} (hc : IsLimit c)
+    (d : Multifork (F.multicospanIndex P)) :
+    f.mapMultiforkOfIsLimit P hc d = g.mapMultiforkOfIsLimit P hc d := by
+  refine Multifork.IsLimit.hom_ext hc fun a ↦ ?_
+  have heq := d.condition ⟨⟨(f.s₀ a), (g.s₀ a)⟩, H.H a⟩
+  simp only [multicospanIndex_right, multicospanShape_fst, multicospanIndex_left,
+    multicospanIndex_fst, multicospanShape_snd, multicospanIndex_snd] at heq
+  simp [-Homotopy.wl, -Homotopy.wr, ← H.wl, ← H.wr, reassoc_of% heq]
+
+variable [Limits.HasPullbacks C] (f g : E.Hom F)
+
+/-- (Implementation): The covering object of `cylinder f g`. -/
+noncomputable
+abbrev cylinderX {i : E.I₀} (k : F.I₁ (f.s₀ i) (g.s₀ i)) : C :=
+  pullback (pullback.lift (f.h₀ i) (g.h₀ i) (by simp)) (F.toPullback k)
+
+/-- (Implementation): The structure morphisms of the covering objects of `cylinder f g`. -/
+noncomputable
+abbrev cylinderf {i : E.I₀} (k : F.I₁ (f.s₀ i) (g.s₀ i)) : cylinderX f g k ⟶ S :=
+  pullback.fst _ _ ≫ E.f _
+
+/-- Given two refinement morphisms `f, g : E ⟶ F`, this is a (pre-)`1`-hypercover `W` that
+admits a morphism `h : W ⟶ E` such that `h ≫ f` and `h ≫ g` are homotopic. Hence
+they become equal after quotienting out by homotopy.
+This is a `1`-hypercover, if `E` and `F` are (see `OneHpyercover.cylinder`). -/
+@[simps]
+noncomputable def cylinder (f g : E.Hom F) : PreOneHypercover.{max w w'} S where
+  I₀ := Σ (i : E.I₀), F.I₁ (f.s₀ i) (g.s₀ i)
+  X p := cylinderX f g p.2
+  f p := cylinderf f g p.2
+  I₁ p q := ULift.{max w w'} (E.I₁ p.1 q.1)
+  Y {p q} k :=
+    pullback
+      (pullback.map (cylinderf f g p.2)
+        (cylinderf f g q.2) _ _ (pullback.fst _ _) (pullback.fst _ _) (𝟙 S) (by simp)
+        (by simp))
+      (pullback.lift _ _ (E.w k.down))
+  p₁ {p q} k := pullback.fst _ _ ≫ pullback.fst _ _
+  p₂ {p q} k := pullback.fst _ _ ≫ pullback.snd _ _
+  w {_ _} k := by simp [pullback.condition]
+
+lemma toPullback_cylinder {i j : (cylinder f g).I₀} (k : (cylinder f g).I₁ i j) :
+    (cylinder f g).toPullback k = pullback.fst _ _ := by
+  apply pullback.hom_ext <;> simp [toPullback]
+
+lemma sieve₀_cylinder :
+    (cylinder f g).sieve₀ =
+      Sieve.generate
+        (Presieve.bindOfArrows _ E.f <| fun i ↦
+          (Sieve.pullback (pullback.lift (f.h₀ _) (g.h₀ _) (by simp))
+            (F.sieve₁' _ _)).arrows) := by
+  refine le_antisymm ?_ ?_
+  · rw [sieve₀, Sieve.generate_le_iff]
+    rintro - - ⟨i⟩
+    refine ⟨_, 𝟙 _, (cylinder f g).f _, ⟨_, _, ?_⟩, by simp⟩
+    simp only [Sieve.pullback_apply, pullback.condition]
+    exact Sieve.downward_closed _ (Sieve.ofArrows_mk _ _ _) _
+  · rw [Sieve.generate_le_iff, sieve₀]
+    rintro Z u ⟨i, v, ⟨W, o, o', ⟨j⟩, hoo'⟩⟩
+    exact ⟨_, pullback.lift v o hoo'.symm, (cylinder f g).f ⟨i, j⟩, Presieve.ofArrows.mk _,
+      by simp⟩
+
+lemma sieve₁'_cylinder (i j : Σ (i : E.I₀), F.I₁ (f.s₀ i) (g.s₀ i)) :
+    (cylinder f g).sieve₁' i j =
+      Sieve.pullback
+        (pullback.map _ _ _ _ (pullback.fst _ _) (pullback.fst _ _) (𝟙 S) (by simp) (by simp))
+        (E.sieve₁' i.1 j.1) := by
+  refine le_antisymm ?_ ?_
+  · rw [sieve₁', Sieve.ofArrows, Sieve.generate_le_iff]
+    rintro - - ⟨k⟩
+    refine ⟨E.Y k.down, pullback.snd _ _, E.toPullback k.down, Presieve.ofArrows.mk k.down, ?_⟩
+    simp only [cylinder_Y, cylinder_f, toPullback_cylinder, pullback.condition]
+  · rw [sieve₁', Sieve.ofArrows, ← Sieve.pullbackArrows_comm, Sieve.generate_le_iff]
+    rintro Z u ⟨W, v, ⟨k⟩⟩
+    rw [← pullbackSymmetry_inv_comp_fst]
+    apply (((cylinder f g).sieve₁' i j)).downward_closed
+    rw [sieve₁']
+    convert Sieve.ofArrows_mk _ _ (ULift.up k)
+    simp [toPullback_cylinder f g ⟨k⟩]
+
+/-- (Implementation): The refinement morphism `cylinder f g ⟶ E`. -/
+@[simps]
+noncomputable def cylinderHom : (cylinder f g).Hom E where
+  s₀ p := p.1
+  s₁ k := k.down
+  h₀ p := pullback.fst _ _
+  h₁ {p q} k := pullback.snd _ _
+  w₁₁ k := by
+    have : E.p₁ k.down = pullback.lift _ _ (E.w k.down) ≫ pullback.fst _ _ := by simp
+    nth_rw 2 [this]
+    rw [← pullback.condition_assoc]
+    simp
+  w₁₂ {p q} k := by
+    have : E.p₂ k.down = pullback.lift _ _ (E.w k.down) ≫ pullback.snd _ _ := by simp
+    nth_rw 2 [this]
+    rw [← pullback.condition_assoc]
+    simp
+  w₀ := by simp
+
+/-- (Implementation): The homotopy of the morphisms `cylinder f g ⟶ E ⟶ F`. -/
+noncomputable def cylinderHomotopy :
+    Homotopy ((cylinderHom f g).comp f) ((cylinderHom f g).comp g) where
+  H p := p.2
+  a p := pullback.snd _ _
+  wl p := by
+    have : F.p₁ p.snd = pullback.lift _ _ (F.w p.2) ≫ pullback.fst _ _ := by simp
+    nth_rw 1 [this]
+    rw [← pullback.condition_assoc]
+    simp
+  wr p := by
+    have : g.h₀ p.fst = pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) (by simp) ≫
+        pullback.snd (F.f _) (F.f _) := by simp
+    dsimp only [cylinder_X, Hom.comp_s₀, cylinder_I₀, Function.comp_apply, cylinderHom_s₀,
+      Hom.comp_h₀, cylinderHom_h₀]
+    nth_rw 3 [this]
+    rw [pullback.condition_assoc]
+    simp
+
+/-- Up to homotopy, the category of (pre-)`1`-hypercovers is cofiltered. -/
+lemma exists_nonempty_homotopy (f g : E.Hom F) :
+    ∃ (W : PreOneHypercover.{max w w'} S) (h : W.Hom E),
+      Nonempty (Homotopy (h.comp f) (h.comp g)) :=
+  ⟨cylinder f g, PreOneHypercover.cylinderHom f g, ⟨cylinderHomotopy f g⟩⟩
+
+end Category
+
 end PreOneHypercover
 
 namespace GrothendieckTopology
@@ -214,6 +429,39 @@ noncomputable def isLimitMultifork : IsLimit (E.multifork F.1) :=
 
 end
 
+section Category
+
+variable {S : C} {E : OneHypercover.{w} J S} {F : OneHypercover.{w'} J S}
+
+/-- A morphism of `1`-hypercovers is a morphism of the underlying pre-`1`-hypercovers. -/
+abbrev Hom (E : OneHypercover.{w} J S) (F : OneHypercover.{w'} J S) :=
+  E.toPreOneHypercover.Hom F.toPreOneHypercover
+
+variable [HasPullbacks C]
+
+/-- Given two refinement morphism `f, g : E ⟶ F`, this is a `1`-hypercover `W` that
+admits a morphism `h : W ⟶ E` such that `h ≫ f` and `h ≫ g` are homotopic. Hence
+they become equal after quotienting out by homotopy. -/
+@[simps! toPreOneHypercover]
+noncomputable def cylinder (f g : E.Hom F) : J.OneHypercover S :=
+  mk' (PreOneHypercover.cylinder f g)
+    (by
+      rw [PreOneHypercover.sieve₀_cylinder]
+      refine J.bindOfArrows E.mem₀ fun i ↦ ?_
+      rw [Sieve.generate_sieve]
+      exact J.pullback_stable _ (mem_sieve₁' F _ _))
+    (fun i j ↦ by
+      rw [PreOneHypercover.sieve₁'_cylinder]
+      exact J.pullback_stable _ (mem_sieve₁' E _ _))
+
+/-- Up to homotopy, the category of `1`-hypercovers is cofiltered. -/
+lemma exists_nonempty_homotopy (f g : E.Hom F) :
+    ∃ (W : OneHypercover.{max w w'} J S) (h : W.Hom E),
+      Nonempty (PreOneHypercover.Homotopy (h.comp f) (h.comp g)) :=
+  ⟨cylinder f g, PreOneHypercover.cylinderHom f g, ⟨PreOneHypercover.cylinderHomotopy f g⟩⟩
+
+end Category
+
 end OneHypercover
 
 namespace Cover

Mathlib/CategoryTheory/Sites/Sieves.lean

@@ -189,6 +189,13 @@ theorem ofArrows_surj {ι : Type*} {Y : ι → C} (f : ∀ i, Y i ⟶ X) {Z : C}
   obtain ⟨i⟩ := hg
   exact ⟨i, rfl, by simp only [eqToHom_refl, id_comp]⟩
 
+/-- A convenient constructor for a refinement of a presieve of the form `Presieve.ofArrows`.
+This contains a sieve obtained by `Sieve.bind` and `Sieve.ofArrows`, see
+`Presieve.bind_ofArrows_le_bindOfArrows`, but has better definitional properties. -/
+inductive bindOfArrows {ι : Type*} {X : C} (Y : ι → C)
+    (f : ∀ i, Y i ⟶ X) (R : ∀ i, Presieve (Y i)) : Presieve X
+  | mk (i : ι) {Z : C} (g : Z ⟶ Y i) (hg : R i g) : bindOfArrows Y f R (g ≫ f i)
+
 /-- Given a presieve on `F(X)`, we can define a presieve on `X` by taking the preimage via `F`. -/
 def functorPullback (R : Presieve (F.obj X)) : Presieve X := fun _ f => R (F.map f)
 
@@ -880,4 +887,14 @@ instance functorInclusion_top_isIso : IsIso (⊤ : Sieve X).functorInclusion :=
 
 end Sieve
 
+lemma Presieve.bind_ofArrows_le_bindOfArrows {ι : Type*} {X : C} (Z : ι → C)
+    (f : ∀ i, Z i ⟶ X) (R : ∀ i, Presieve (Z i)) :
+    Sieve.bind (Sieve.ofArrows Z f)
+      (fun _ _ hg ↦ Sieve.pullback
+        (Sieve.ofArrows.h hg) (.generate <| R (Sieve.ofArrows.i hg))) ≤
+    Sieve.generate (Presieve.bindOfArrows Z f R) := by
+  rintro T g ⟨W, v, v', hv', ⟨S, u, u', h, hu⟩, rfl⟩
+  rw [← Sieve.ofArrows.fac hv', ← reassoc_of% hu]
+  exact ⟨S, u, u' ≫ f _, ⟨_, _, h⟩, rfl⟩
+
 end CategoryTheory