From d70b029618a44e71c2e168bc0d758f0fad6df0b3 Mon Sep 17 00:00:00 2001 From: Andrew Yang Date: Sat, 28 Oct 2023 11:22:32 +0000 Subject: [PATCH] feat: Remove `Extensive` in favour of `FinitaryExtensive`. (#7731) Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com> --- Mathlib/CategoryTheory/Extensive.lean | 200 ++++++++++++++++-- Mathlib/CategoryTheory/Limits/VanKampen.lean | 102 +++++++++ .../Sites/RegularExtensive.lean | 44 +--- 3 files changed, 296 insertions(+), 50 deletions(-) diff --git a/Mathlib/CategoryTheory/Extensive.lean b/Mathlib/CategoryTheory/Extensive.lean index 910c171544aaa..8df95e366bd1b 100644 --- a/Mathlib/CategoryTheory/Extensive.lean +++ b/Mathlib/CategoryTheory/Extensive.lean @@ -8,6 +8,7 @@ import Mathlib.CategoryTheory.Limits.Shapes.StrictInitial import Mathlib.CategoryTheory.Limits.Shapes.Types import Mathlib.Topology.Category.TopCat.Limits.Pullbacks import Mathlib.CategoryTheory.Limits.FunctorCategory +import Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts import Mathlib.CategoryTheory.Limits.VanKampen #align_import category_theory.extensive from "leanprover-community/mathlib"@"178a32653e369dce2da68dc6b2694e385d484ef1" @@ -31,7 +32,9 @@ import Mathlib.CategoryTheory.Limits.VanKampen - `CategoryTheory.FinitaryExtensive_TopCat`: The category `Top` is extensive. - `CategoryTheory.FinitaryExtensive_functor`: The category `C ⥤ D` is extensive if `D` - has all pullbacks and is extensive + has all pullbacks and is extensive. +- `CategoryTheory.FinitaryExtensive.isVanKampen_finiteCoproducts`: Finite coproducts in a + finitary extensive category are van Kampen. ## TODO Show that the following are finitary extensive: @@ -58,17 +61,26 @@ section Extensive variable {X Y : C} -/-- A category is (finitary) extensive if it has finite coproducts, -and binary coproducts are van Kampen. +/-- A category is (finitary) pre-extensive if it has finite coproducts, +and binary coproducts are van Kampen. -/ +class FinitaryPreExtensive (C : Type u) [Category.{v} C] : Prop where + [hasFiniteCoproducts : HasFiniteCoproducts C] + [hasPullbackInl : ∀ {X Y Z : C} (f : Z ⟶ X ⨿ Y), HasPullback coprod.inl f] + /-- In a finitary extensive category, all coproducts are van Kampen-/ + universal' : ∀ {X Y : C} (c : BinaryCofan X Y), IsColimit c → IsUniversalColimit c -TODO: Show that this is iff all finite coproducts are van Kampen. -/ +attribute [instance] FinitaryPreExtensive.hasFiniteCoproducts FinitaryPreExtensive.hasPullbackInl + +/-- A category is (finitary) extensive if it has finite coproducts, +and binary coproducts are van Kampen. -/ class FinitaryExtensive (C : Type u) [Category.{v} C] : Prop where [hasFiniteCoproducts : HasFiniteCoproducts C] + [hasPullbackInl : ∀ {X Y Z : C} (f : Z ⟶ X ⨿ Y), HasPullback coprod.inl f] /-- In a finitary extensive category, all coproducts are van Kampen-/ van_kampen' : ∀ {X Y : C} (c : BinaryCofan X Y), IsColimit c → IsVanKampenColimit c #align category_theory.finitary_extensive CategoryTheory.FinitaryExtensive -attribute [instance] FinitaryExtensive.hasFiniteCoproducts +attribute [instance] FinitaryExtensive.hasFiniteCoproducts FinitaryExtensive.hasPullbackInl theorem FinitaryExtensive.vanKampen [FinitaryExtensive C] {F : Discrete WalkingPair ⥤ C} (c : Cocone F) (hc : IsColimit c) : IsVanKampenColimit c := by @@ -83,6 +95,33 @@ theorem FinitaryExtensive.vanKampen [FinitaryExtensive C] {F : Discrete WalkingP exact FinitaryExtensive.van_kampen' c hc #align category_theory.finitary_extensive.van_kampen CategoryTheory.FinitaryExtensive.vanKampen +namespace FinitaryPreExtensive + +variable [FinitaryPreExtensive C] {X Y Z : C} (f : Z ⟶ X ⨿ Y) + +instance hasPullbackInl' : + HasPullback f coprod.inl := + hasPullback_symmetry _ _ + +instance hasPullbackInr' : + HasPullback f coprod.inr := by + have : IsPullback (𝟙 _) (f ≫ (coprod.braiding X Y).hom) f (coprod.braiding Y X).hom := + IsPullback.of_horiz_isIso ⟨by simp⟩ + have := (IsPullback.of_hasPullback (f ≫ (coprod.braiding X Y).hom) coprod.inl).paste_horiz this + simp only [coprod.braiding_hom, Category.comp_id, colimit.ι_desc, BinaryCofan.mk_pt, + BinaryCofan.ι_app_left, BinaryCofan.mk_inl] at this + exact ⟨⟨⟨_, this.isLimit⟩⟩⟩ + +instance hasPullbackInr : + HasPullback coprod.inr f := + hasPullback_symmetry _ _ + +end FinitaryPreExtensive + +instance (priority := 100) FinitaryExtensive.toFinitaryPreExtensive [FinitaryExtensive C] : + FinitaryPreExtensive C := + ⟨fun c hc ↦ (FinitaryExtensive.van_kampen' c hc).isUniversal⟩ + theorem FinitaryExtensive.mono_inr_of_isColimit [FinitaryExtensive C] {c : BinaryCofan X Y} (hc : IsColimit c) : Mono c.inr := BinaryCofan.mono_inr_of_isVanKampen (FinitaryExtensive.vanKampen c hc) @@ -105,18 +144,19 @@ theorem FinitaryExtensive.isPullback_initial_to_binaryCofan [FinitaryExtensive C BinaryCofan.isPullback_initial_to_of_isVanKampen (FinitaryExtensive.vanKampen c hc) #align category_theory.finitary_extensive.is_pullback_initial_to_binary_cofan CategoryTheory.FinitaryExtensive.isPullback_initial_to_binaryCofan -instance (priority := 100) hasStrictInitialObjects_of_finitaryExtensive [FinitaryExtensive C] : - HasStrictInitialObjects C := - hasStrictInitial_of_isUniversal (FinitaryExtensive.vanKampen _ +instance (priority := 100) hasStrictInitialObjects_of_finitaryPreExtensive + [FinitaryPreExtensive C] : HasStrictInitialObjects C := + hasStrictInitial_of_isUniversal (FinitaryPreExtensive.universal' _ ((BinaryCofan.isColimit_iff_isIso_inr initialIsInitial _).mpr (by dsimp - infer_instance)).some).isUniversal -#align category_theory.has_strict_initial_objects_of_finitary_extensive CategoryTheory.hasStrictInitialObjects_of_finitaryExtensive + infer_instance)).some) +#align category_theory.has_strict_initial_objects_of_finitary_extensive CategoryTheory.hasStrictInitialObjects_of_finitaryPreExtensive theorem finitaryExtensive_iff_of_isTerminal (C : Type u) [Category.{v} C] [HasFiniteCoproducts C] + [hasPullbackInl : ∀ {X Y Z : C} (f : Z ⟶ X ⨿ Y), HasPullback coprod.inl f] (T : C) (HT : IsTerminal T) (c₀ : BinaryCofan T T) (hc₀ : IsColimit c₀) : FinitaryExtensive C ↔ IsVanKampenColimit c₀ := by - refine' ⟨fun H => H.2 c₀ hc₀, fun H => _⟩ + refine' ⟨fun H => H.van_kampen' c₀ hc₀, fun H => _⟩ constructor simp_rw [BinaryCofan.isVanKampen_iff] at H ⊢ intro X Y c hc X' Y' c' αX αY f hX hY @@ -348,7 +388,8 @@ instance finitaryExtensive_functor [HasPullbacks C] [FinitaryExtensive C] : FinitaryExtensive.vanKampen _ <| PreservesColimit.preserves hc⟩ theorem finitaryExtensive_of_preserves_and_reflects (F : C ⥤ D) [FinitaryExtensive D] - [HasFiniteCoproducts C] [PreservesLimitsOfShape WalkingCospan F] + [HasFiniteCoproducts C] [∀ {X Y Z : C} (f : Z ⟶ X ⨿ Y), HasPullback coprod.inl f] + [PreservesLimitsOfShape WalkingCospan F] [ReflectsLimitsOfShape WalkingCospan F] [PreservesColimitsOfShape (Discrete WalkingPair) F] [ReflectsColimitsOfShape (Discrete WalkingPair) F] : FinitaryExtensive C := ⟨fun _ hc => (FinitaryExtensive.vanKampen _ (isColimitOfPreserves F hc)).of_mapCocone F⟩ @@ -366,6 +407,141 @@ theorem finitaryExtensive_of_preserves_and_reflects_isomorphism (F : C ⥤ D) [F end Functor +section FiniteCoproducts + +theorem FinitaryPreExtensive.isUniversal_finiteCoproducts_Fin [FinitaryPreExtensive C] {n : ℕ} + {F : Discrete (Fin n) ⥤ C} {c : Cocone F} (hc : IsColimit c) : IsUniversalColimit c := by + let f : Fin n → C := F.obj ∘ Discrete.mk + have : F = Discrete.functor f := + Functor.hext (fun _ ↦ rfl) (by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp) + clear_value f + subst this + induction' n with n IH + · exact (isVanKampenColimit_of_isEmpty _ hc).isUniversal + · apply IsUniversalColimit.of_iso _ + ((extendCofanIsColimit f (coproductIsCoproduct _) (coprodIsCoprod _ _)).uniqueUpToIso hc) + apply @isUniversalColimit_extendCofan _ _ _ _ _ _ _ _ ?_ + · apply IH + exact coproductIsCoproduct _ + · apply FinitaryPreExtensive.universal' + exact coprodIsCoprod _ _ + · dsimp + infer_instance + +theorem FinitaryPreExtensive.isUniversal_finiteCoproducts [FinitaryPreExtensive C] {ι : Type*} + [Finite ι] {F : Discrete ι ⥤ C} {c : Cocone F} (hc : IsColimit c) : IsUniversalColimit c := by + obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin ι + apply (IsUniversalColimit.whiskerEquivalence_iff (Discrete.equivalence e).symm).mp + apply FinitaryPreExtensive.isUniversal_finiteCoproducts_Fin + exact (IsColimit.whiskerEquivalenceEquiv (Discrete.equivalence e).symm) hc + +theorem FinitaryExtensive.isVanKampen_finiteCoproducts_Fin [FinitaryExtensive C] {n : ℕ} + {F : Discrete (Fin n) ⥤ C} {c : Cocone F} (hc : IsColimit c) : IsVanKampenColimit c := by + let f : Fin n → C := F.obj ∘ Discrete.mk + have : F = Discrete.functor f := + Functor.hext (fun _ ↦ rfl) (by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp) + clear_value f + subst this + induction' n with n IH + · exact isVanKampenColimit_of_isEmpty _ hc + · apply IsVanKampenColimit.of_iso _ + ((extendCofanIsColimit f (coproductIsCoproduct _) (coprodIsCoprod _ _)).uniqueUpToIso hc) + apply @isVanKampenColimit_extendCofan _ _ _ _ _ _ _ _ ?_ + · apply IH + exact coproductIsCoproduct _ + · apply FinitaryExtensive.van_kampen' + exact coprodIsCoprod _ _ + · dsimp + infer_instance + +theorem FinitaryExtensive.isVanKampen_finiteCoproducts [FinitaryExtensive C] {ι : Type*} + [Finite ι] {F : Discrete ι ⥤ C} {c : Cocone F} (hc : IsColimit c) : IsVanKampenColimit c := by + obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin ι + apply (IsVanKampenColimit.whiskerEquivalence_iff (Discrete.equivalence e).symm).mp + apply FinitaryExtensive.isVanKampen_finiteCoproducts_Fin + exact (IsColimit.whiskerEquivalenceEquiv (Discrete.equivalence e).symm) hc + +lemma FinitaryPreExtensive.hasPullbacks_of_is_coproduct [FinitaryPreExtensive C] {ι : Type*} + [Finite ι] {F : Discrete ι ⥤ C} {c : Cocone F} (hc : IsColimit c) (i : Discrete ι) {X : C} + (g : X ⟶ _) : HasPullback g (c.ι.app i) := by + classical + let f : ι → C := F.obj ∘ Discrete.mk + have : F = Discrete.functor f := + Functor.hext (fun i ↦ rfl) (by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp) + clear_value f + subst this + change Cofan f at c + obtain ⟨i⟩ := i + let e : ∐ f ≅ f i ⨿ (∐ fun j : ({i}ᶜ : Set ι) ↦ f j) := + { hom := Sigma.desc (fun j ↦ if h : j = i then eqToHom (congr_arg f h) ≫ coprod.inl else + Sigma.ι (fun j : ({i}ᶜ : Set ι) ↦ f j) ⟨j, h⟩ ≫ coprod.inr) + inv := coprod.desc (Sigma.ι f i) (Sigma.desc <| fun j ↦ Sigma.ι f j) + hom_inv_id := by aesop_cat + inv_hom_id := by + ext j + · simp + · simp only [coprod.desc_comp, colimit.ι_desc, Cofan.mk_pt, Cofan.mk_ι_app, + eqToHom_refl, Category.id_comp, dite_true, BinaryCofan.mk_pt, BinaryCofan.ι_app_right, + BinaryCofan.mk_inr, colimit.ι_desc_assoc, Discrete.functor_obj, Category.comp_id] + exact dif_neg j.prop } + let e' : c.pt ≅ f i ⨿ (∐ fun j : ({i}ᶜ : Set ι) ↦ f j) := + hc.coconePointUniqueUpToIso (getColimitCocone _).2 ≪≫ e + have : coprod.inl ≫ e'.inv = c.ι.app ⟨i⟩ + · simp only [Iso.trans_inv, coprod.desc_comp, colimit.ι_desc, BinaryCofan.mk_pt, + BinaryCofan.ι_app_left, BinaryCofan.mk_inl] + exact colimit.comp_coconePointUniqueUpToIso_inv _ _ + clear_value e' + rw [← this] + have : IsPullback (𝟙 _) (g ≫ e'.hom) g e'.inv := IsPullback.of_horiz_isIso ⟨by simp⟩ + exact ⟨⟨⟨_, ((IsPullback.of_hasPullback (g ≫ e'.hom) coprod.inl).paste_horiz this).isLimit⟩⟩⟩ + +lemma FinitaryExtensive.mono_ι [FinitaryExtensive C] {ι : Type*} [Finite ι] {F : Discrete ι ⥤ C} + {c : Cocone F} (hc : IsColimit c) (i : Discrete ι) : + Mono (c.ι.app i) := + mono_of_cofan_isVanKampen (isVanKampen_finiteCoproducts hc) _ + +instance [FinitaryExtensive C] {ι : Type*} [Finite ι] (X : ι → C) (i : ι) : + Mono (Sigma.ι X i) := + FinitaryExtensive.mono_ι (coproductIsCoproduct _) ⟨i⟩ + +lemma FinitaryExtensive.isPullback_initial_to [FinitaryExtensive C] + {ι : Type*} [Finite ι] {F : Discrete ι ⥤ C} + {c : Cocone F} (hc : IsColimit c) (i j : Discrete ι) (e : i ≠ j) : + IsPullback (initial.to _) (initial.to _) (c.ι.app i) (c.ι.app j) := + isPullback_initial_to_of_cofan_isVanKampen (isVanKampen_finiteCoproducts hc) i j e + +lemma FinitaryExtensive.isPullback_initial_to_sigma_ι [FinitaryExtensive C] {ι : Type*} [Finite ι] + (X : ι → C) (i j : ι) (e : i ≠ j) : + IsPullback (initial.to _) (initial.to _) (Sigma.ι X i) (Sigma.ι X j) := + FinitaryExtensive.isPullback_initial_to (coproductIsCoproduct _) ⟨i⟩ ⟨j⟩ + (ne_of_apply_ne Discrete.as e) + +instance FinitaryPreExtensive.hasPullbacks_of_inclusions [FinitaryPreExtensive C] {X Z : C} + {α : Type*} (f : X ⟶ Z) {Y : (a : α) → C} (i : (a : α) → Y a ⟶ Z) [Finite α] + [hi : IsIso (Sigma.desc i)] (a : α) : HasPullback f (i a) := by + apply FinitaryPreExtensive.hasPullbacks_of_is_coproduct (c := Cofan.mk Z i) + exact @IsColimit.ofPointIso (t := Cofan.mk Z i) (P := _) hi + +lemma FinitaryPreExtensive.sigma_desc_iso [FinitaryPreExtensive C] {α : Type} [Finite α] {X : C} + {Z : α → C} (π : (a : α) → Z a ⟶ X) {Y : C} (f : Y ⟶ X) (hπ : IsIso (Sigma.desc π)) : + IsIso (Sigma.desc ((fun _ ↦ pullback.fst) : (a : α) → pullback f (π a) ⟶ _)) := by + suffices IsColimit (Cofan.mk _ ((fun _ ↦ pullback.fst) : (a : α) → pullback f (π a) ⟶ _)) by + change IsIso (this.coconePointUniqueUpToIso (getColimitCocone _).2).inv + infer_instance + let : IsColimit (Cofan.mk X π) + · refine @IsColimit.ofPointIso (t := Cofan.mk X π) (P := coproductIsCoproduct Z) ?_ + convert hπ + simp [coproductIsCoproduct] + refine (FinitaryPreExtensive.isUniversal_finiteCoproducts this + (Cofan.mk _ ((fun _ ↦ pullback.fst) : (a : α) → pullback f (π a) ⟶ _)) + (Discrete.natTrans <| fun i ↦ pullback.snd) f ?_ + (NatTrans.equifibered_of_discrete _) ?_).some + · ext + simp [pullback.condition] + · exact fun j ↦ IsPullback.of_hasPullback f (π j.as) + +end FiniteCoproducts + end Extensive end CategoryTheory diff --git a/Mathlib/CategoryTheory/Limits/VanKampen.lean b/Mathlib/CategoryTheory/Limits/VanKampen.lean index 0ade69108a5ac..b7bdabb61e031 100644 --- a/Mathlib/CategoryTheory/Limits/VanKampen.lean +++ b/Mathlib/CategoryTheory/Limits/VanKampen.lean @@ -133,6 +133,18 @@ theorem IsInitial.isVanKampenColimit [HasStrictInitialObjects C] {X : C} (h : Is section Functor +theorem IsUniversalColimit.of_iso {F : J ⥤ C} {c c' : Cocone F} (hc : IsUniversalColimit c) + (e : c ≅ c') : IsUniversalColimit c' := by + intro F' c'' α f h hα H + have : c'.ι ≫ (Functor.const J).map e.inv.hom = c.ι := by + ext j + exact e.inv.2 j + apply hc c'' α (f ≫ e.inv.1) (by rw [Functor.map_comp, ← reassoc_of% h, this]) hα + intro j + rw [← Category.comp_id (α.app j)] + have : IsIso e.inv.hom := Functor.map_isIso (Cocones.forget _) e.inv + exact (H j).paste_vert (IsPullback.of_vert_isIso ⟨by simp⟩) + theorem IsVanKampenColimit.of_iso {F : J ⥤ C} {c c' : Cocone F} (H : IsVanKampenColimit c) (e : c ≅ c') : IsVanKampenColimit c' := by intro F' c'' α f h hα @@ -162,6 +174,18 @@ theorem IsVanKampenColimit.precompose_isIso {F G : J ⥤ C} (α : F ⟶ G) [IsIs rw [← IsPullback.paste_vert_iff this _, Category.comp_id] exact (congr_app e j).symm +theorem IsUniversalColimit.precompose_isIso {F G : J ⥤ C} (α : F ⟶ G) [IsIso α] + {c : Cocone G} (hc : IsUniversalColimit c) : + IsUniversalColimit ((Cocones.precompose α).obj c) := by + intros F' c' α' f e hα H + apply (hc c' (α' ≫ α) f ((Category.assoc _ _ _).trans e) + (hα.comp (NatTrans.equifibered_of_isIso _))) + intro j + simp only [Functor.const_obj_obj, NatTrans.comp_app, + Cocones.precompose_obj_pt, Cocones.precompose_obj_ι] + rw [← Category.comp_id f] + exact (H j).paste_vert (IsPullback.of_vert_isIso ⟨Category.comp_id _⟩) + theorem IsVanKampenColimit.precompose_isIso_iff {F G : J ⥤ C} (α : F ⟶ G) [IsIso α] {c : Cocone G} : IsVanKampenColimit ((Cocones.precompose α).obj c) ↔ IsVanKampenColimit c := ⟨fun hc ↦ IsVanKampenColimit.of_iso (IsVanKampenColimit.precompose_isIso (inv α) hc) @@ -189,6 +213,28 @@ theorem IsVanKampenColimit.mapCocone_iff (G : C ⥤ D) {F : J ⥤ C} {c : Cocone refine hc.of_iso (Cocones.ext (G.asEquivalence.unitIso.app c.pt) ?_) simp [Functor.asEquivalence]⟩ +theorem IsUniversalColimit.whiskerEquivalence {K : Type*} [Category K] (e : J ≌ K) + {F : K ⥤ C} {c : Cocone F} (hc : IsUniversalColimit c) : + IsUniversalColimit (c.whisker e.functor) := by + intro F' c' α f e' hα H + convert hc (c'.whisker e.inverse) (whiskerLeft e.inverse α ≫ (e.invFunIdAssoc F).hom) f ?_ + ((hα.whiskerLeft _).comp (NatTrans.equifibered_of_isIso _)) ?_ using 1 + · exact (IsColimit.whiskerEquivalenceEquiv e.symm).nonempty_congr + · convert congr_arg (whiskerLeft e.inverse) e' + ext + simp + · intro k + rw [← Category.comp_id f] + refine (H (e.inverse.obj k)).paste_vert ?_ + have : IsIso (𝟙 (Cocone.whisker e.functor c).pt) := inferInstance + exact IsPullback.of_vert_isIso ⟨by simp⟩ + +theorem IsUniversalColimit.whiskerEquivalence_iff {K : Type*} [Category K] (e : J ≌ K) + {F : K ⥤ C} {c : Cocone F} : + IsUniversalColimit (c.whisker e.functor) ↔ IsUniversalColimit c := + ⟨fun hc ↦ ((hc.whiskerEquivalence e.symm).precompose_isIso (e.invFunIdAssoc F).inv).of_iso + (Cocones.ext (Iso.refl _) (by simp)), IsUniversalColimit.whiskerEquivalence e⟩ + theorem IsVanKampenColimit.whiskerEquivalence {K : Type*} [Category K] (e : J ≌ K) {F : K ⥤ C} {c : Cocone F} (hc : IsVanKampenColimit c) : IsVanKampenColimit (c.whisker e.functor) := by @@ -659,6 +705,62 @@ theorem isVanKampenColimit_extendCofan {n : ℕ} (f : Fin (n + 1) → C) BinaryCofan.ι_app_right, BinaryCofan.mk_inr, colimit.ι_desc, Discrete.natTrans_app] using t₁'.paste_horiz (t₂' ⟨WalkingPair.right⟩) +theorem isPullback_of_cofan_isVanKampen [HasInitial C] {ι : Type*} {X : ι → C} + {c : Cofan X} (hc : IsVanKampenColimit c) (i j : ι) [DecidableEq ι] : + IsPullback (P := (if j = i then X i else ⊥_ C)) + (if h : j = i then eqToHom (if_pos h) else eqToHom (if_neg h) ≫ initial.to (X i)) + (if h : j = i then eqToHom ((if_pos h).trans (congr_arg X h.symm)) + else eqToHom (if_neg h) ≫ initial.to (X j)) + (Cofan.inj c i) (Cofan.inj c j) := by + refine (hc (Cofan.mk (X i) (f := fun k ↦ if k = i then X i else ⊥_ C) + (fun k ↦ if h : k = i then (eqToHom $ if_pos h) else (eqToHom $ if_neg h) ≫ initial.to _)) + (Discrete.natTrans (fun k ↦ if h : k.1 = i then (eqToHom $ (if_pos h).trans + (congr_arg X h.symm)) else (eqToHom $ if_neg h) ≫ initial.to _)) + (c.inj i) ?_ (NatTrans.equifibered_of_discrete _)).mp ⟨?_⟩ ⟨j⟩ + · ext ⟨k⟩ + simp only [Discrete.functor_obj, Functor.const_obj_obj, NatTrans.comp_app, + Discrete.natTrans_app, Cofan.mk_pt, Cofan.mk_ι_app, Functor.const_map_app] + split + · subst ‹k = i›; rfl + · simp + · refine mkCofanColimit _ (fun t ↦ (eqToHom (if_pos rfl).symm) ≫ t.inj i) ?_ ?_ + · intro t j + simp only [Cofan.mk_pt, cofan_mk_inj] + split + · subst ‹j = i›; simp + · rw [Category.assoc, ← IsIso.eq_inv_comp] + exact initialIsInitial.hom_ext _ _ + · intro t m hm + simp [← hm i] + +theorem isPullback_initial_to_of_cofan_isVanKampen [HasInitial C] {ι : Type*} {F : Discrete ι ⥤ C} + {c : Cocone F} (hc : IsVanKampenColimit c) (i j : Discrete ι) (hi : i ≠ j) : + IsPullback (initial.to _) (initial.to _) (c.ι.app i) (c.ι.app j) := by + classical + let f : ι → C := F.obj ∘ Discrete.mk + have : F = Discrete.functor f := + Functor.hext (fun i ↦ rfl) (by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp) + clear_value f + subst this + convert isPullback_of_cofan_isVanKampen hc i.as j.as + exact (if_neg (mt (Discrete.ext _ _) hi.symm)).symm + +theorem mono_of_cofan_isVanKampen [HasInitial C] {ι : Type*} {F : Discrete ι ⥤ C} + {c : Cocone F} (hc : IsVanKampenColimit c) (i : Discrete ι) : Mono (c.ι.app i) := by + classical + let f : ι → C := F.obj ∘ Discrete.mk + have : F = Discrete.functor f := + Functor.hext (fun i ↦ rfl) (by rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩; simp) + clear_value f + subst this + refine' PullbackCone.mono_of_isLimitMkIdId _ (IsPullback.isLimit _) + nth_rw 1 [← Category.id_comp (c.ι.app i)] + convert IsPullback.paste_vert _ (isPullback_of_cofan_isVanKampen hc i.as i.as) + swap + · exact (eqToHom (if_pos rfl).symm) + · simp + · exact IsPullback.of_vert_isIso ⟨by simp⟩ + end FiniteCoproducts end CategoryTheory diff --git a/Mathlib/CategoryTheory/Sites/RegularExtensive.lean b/Mathlib/CategoryTheory/Sites/RegularExtensive.lean index 4518e82aeb6f1..7a4ca586fddc1 100644 --- a/Mathlib/CategoryTheory/Sites/RegularExtensive.lean +++ b/Mathlib/CategoryTheory/Sites/RegularExtensive.lean @@ -5,6 +5,7 @@ Authors: Dagur Asgeirsson, Filippo A. E. Nuccio, Riccardo Brasca -/ import Mathlib.CategoryTheory.Preadditive.Projective import Mathlib.CategoryTheory.Sites.Coherent +import Mathlib.CategoryTheory.Extensive import Mathlib.CategoryTheory.Sites.EqualizerSheafCondition import Mathlib.Tactic.ApplyFun /-! @@ -19,8 +20,8 @@ covering sieves of this coverage are generated by presieves consisting of a sing epimorphism. The second one is called the *extensive* coverage and for that to exist, the category `C` must -satisfy a condition called `Extensive C`. This means `C` has finite coproducts and that those -are preserved by pullbacks. The covering sieves of this coverage are generated by presieves +satisfy a condition called `FinitaryPreExtensive C`. This means `C` has finite coproducts and that +those are preserved by pullbacks. The covering sieves of this coverage are generated by presieves consisting finitely many arrows that together induce an isomorphism from the coproduct to the target. @@ -67,39 +68,6 @@ class Preregular : Prop where exists_fac : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Z ⟶ Y) [EffectiveEpi g], (∃ (W : C) (h : W ⟶ X) (_ : EffectiveEpi h) (i : W ⟶ Z), i ≫ g = h ≫ f) -/-- -Describes the property of having pullbacks of morphsims into a finite coproduct, where one -of the morphisms is an inclusion map into the coproduct (up to isomorphism). --/ -class HasPullbacksOfInclusions : Prop where - /-- For any morphism `f : X ⟶ Z`, where `Z` is the coproduct of `i : (a : α) → Y a ⟶ Z` with - `α` finite, the pullback of `f` and `i a` exists for every `a : α`. -/ - has_pullback : ∀ {X Z : C} {α : Type w} (f : X ⟶ Z) {Y : (a : α) → C} - (i : (a : α) → Y a ⟶ Z) [Fintype α] [HasCoproduct Y] [IsIso (Sigma.desc i)] (a : α), - HasPullback f (i a) - -instance [HasPullbacksOfInclusions C] {X Z : C} {α : Type w} (f : X ⟶ Z) {Y : (a : α) → C} - (i : (a : α) → Y a ⟶ Z) [Fintype α] [HasCoproduct Y] [IsIso (Sigma.desc i)] (a : α) : - HasPullback f (i a) := HasPullbacksOfInclusions.has_pullback f i a - -/-- -If `C` has pullbacks then it has the pullbacks relevant to `HasPullbacksOfInclusions`. --/ -instance (priority := 10) [HasPullbacks C] : - HasPullbacksOfInclusions C := ⟨fun _ _ _ => inferInstance⟩ - -/-- -A category is *extensive* if it has all finite coproducts and those coproducts are preserved -by pullbacks (we only require the relevant pullbacks to exist, via `HasPullbacksOfInclusions`). - -TODO: relate this to the class `FinitaryExtensive` --/ -class Extensive extends HasFiniteCoproducts C, HasPullbacksOfInclusions C : Prop where - /-- Pulling back an isomorphism from a coproduct yields an isomorphism. -/ - sigma_desc_iso : ∀ {α : Type} [Fintype α] {X : C} {Z : α → C} (π : (a : α) → Z a ⟶ X) - {Y : C} (f : Y ⟶ X) (_ : IsIso (Sigma.desc π)), - IsIso (Sigma.desc ((fun _ ↦ pullback.fst) : (a : α) → pullback f (π a) ⟶ _)) - /-- The regular coverage on a regular category `C`. -/ @@ -122,7 +90,7 @@ def regularCoverage [Preregular C] : Coverage C where /-- The extensive coverage on an extensive category `C` -/ -def extensiveCoverage [Extensive C] : Coverage C where +def extensiveCoverage [FinitaryPreExtensive C] : Coverage C where covering B := { S | ∃ (α : Type) (_ : Fintype α) (X : α → C) (π : (a : α) → (X a ⟶ B)), S = Presieve.ofArrows X π ∧ IsIso (Sigma.desc π) } pullback := by @@ -131,7 +99,7 @@ def extensiveCoverage [Extensive C] : Coverage C where let π' : (a : α) → Z' a ⟶ Y := fun a ↦ pullback.fst refine ⟨@Presieve.ofArrows C _ _ α Z' π', ⟨?_, ?_⟩⟩ · constructor - exact ⟨hα, Z', π', ⟨by simp only, Extensive.sigma_desc_iso (fun x => π x) f h_iso⟩⟩ + exact ⟨hα, Z', π', ⟨by simp only, FinitaryPreExtensive.sigma_desc_iso (fun x => π x) f h_iso⟩⟩ · intro W g hg rcases hg with ⟨a⟩ refine ⟨Z a, pullback.snd, π a, ?_, by rw [CategoryTheory.Limits.pullback.condition]⟩ @@ -140,7 +108,7 @@ def extensiveCoverage [Extensive C] : Coverage C where /-- The union of the extensive and regular coverages generates the coherent topology on `C`. -/ -lemma extensive_regular_generate_coherent [Preregular C] [Extensive C] [Precoherent C] : +lemma extensive_regular_generate_coherent [Preregular C] [FinitaryPreExtensive C] [Precoherent C] : ((extensiveCoverage C) ⊔ (regularCoverage C)).toGrothendieck = (coherentTopology C) := by ext B S