From 7003654ec5bbfa699bcf1f06387ac666d2112bf3 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Tue, 7 Mar 2023 09:14:52 +0000 Subject: [PATCH] feat: port CategoryTheory.Limits.Shapes.DisjointCoproduct (#2689) Co-authored-by: Moritz Firsching --- Mathlib.lean | 1 + .../Limits/Shapes/DisjointCoproduct.lean | 140 ++++++++++++++++++ 2 files changed, 141 insertions(+) create mode 100644 Mathlib/CategoryTheory/Limits/Shapes/DisjointCoproduct.lean diff --git a/Mathlib.lean b/Mathlib.lean index ebb1b42f774d4..896eea82f1ee9 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -302,6 +302,7 @@ import Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal import Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts +import Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct import Mathlib.CategoryTheory.Limits.Shapes.Equalizers import Mathlib.CategoryTheory.Limits.Shapes.Pullbacks import Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer diff --git a/Mathlib/CategoryTheory/Limits/Shapes/DisjointCoproduct.lean b/Mathlib/CategoryTheory/Limits/Shapes/DisjointCoproduct.lean new file mode 100644 index 0000000000000..f30edaa3d6edd --- /dev/null +++ b/Mathlib/CategoryTheory/Limits/Shapes/DisjointCoproduct.lean @@ -0,0 +1,140 @@ +/- +Copyright (c) 2021 Bhavik Mehta. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Bhavik Mehta + +! This file was ported from Lean 3 source module category_theory.limits.shapes.disjoint_coproduct +! leanprover-community/mathlib commit c9c9fa15fec7ca18e9ec97306fb8764bfe988a7e +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts +import Mathlib.CategoryTheory.Limits.Shapes.Pullbacks + +/-! +# Disjoint coproducts + +Defines disjoint coproducts: coproducts where the intersection is initial and the coprojections +are monic. +Shows that a category with disjoint coproducts is `InitialMonoClass`. + +## TODO + +* Adapt this to the infinitary (small) version: This is one of the conditions in Giraud's theorem + characterising sheaf topoi. +* Construct examples (and counterexamples?), eg Type, Vec. +* Define extensive categories, and show every extensive category has disjoint coproducts. +* Define coherent categories and use this to define positive coherent categories. +-/ + + +universe v u u₂ + +namespace CategoryTheory + +namespace Limits + +open Category + +variable {C : Type u} [Category.{v} C] + +/-- Given any pullback diagram of the form + +Z ⟶ X₁ +↓ ↓ +X₂ ⟶ X + +where `X₁ ⟶ X ← X₂` is a coproduct diagram, then `Z` is initial, and both `X₁ ⟶ X` and `X₂ ⟶ X` +are mono. +-/ +class CoproductDisjoint (X₁ X₂ : C) where + isInitialOfIsPullbackOfIsCoproduct : + ∀ {X Z} {pX₁ : X₁ ⟶ X} {pX₂ : X₂ ⟶ X} {f : Z ⟶ X₁} {g : Z ⟶ X₂} + (_cX : IsColimit (BinaryCofan.mk pX₁ pX₂)) {comm : f ≫ pX₁ = g ≫ pX₂}, + IsLimit (PullbackCone.mk _ _ comm) → IsInitial Z + mono_inl : ∀ (X) (X₁ : X₁ ⟶ X) (X₂ : X₂ ⟶ X) (_cX : IsColimit (BinaryCofan.mk X₁ X₂)), Mono X₁ + mono_inr : ∀ (X) (X₁ : X₁ ⟶ X) (X₂ : X₂ ⟶ X) (_cX : IsColimit (BinaryCofan.mk X₁ X₂)), Mono X₂ +#align category_theory.limits.coproduct_disjoint CategoryTheory.Limits.CoproductDisjoint + +/-- If the coproduct of `X₁` and `X₂` is disjoint, then given any pullback square + +Z ⟶ X₁ +↓ ↓ +X₂ ⟶ X + +where `X₁ ⟶ X ← X₂` is a coproduct, then `Z` is initial. +-/ +def isInitialOfIsPullbackOfIsCoproduct {Z X₁ X₂ X : C} [CoproductDisjoint X₁ X₂] {pX₁ : X₁ ⟶ X} + {pX₂ : X₂ ⟶ X} (cX : IsColimit (BinaryCofan.mk pX₁ pX₂)) {f : Z ⟶ X₁} {g : Z ⟶ X₂} + {comm : f ≫ pX₁ = g ≫ pX₂} (cZ : IsLimit (PullbackCone.mk _ _ comm)) : IsInitial Z := + CoproductDisjoint.isInitialOfIsPullbackOfIsCoproduct cX cZ +#align category_theory.limits.is_initial_of_is_pullback_of_is_coproduct CategoryTheory.Limits.isInitialOfIsPullbackOfIsCoproduct + +/-- If the coproduct of `X₁` and `X₂` is disjoint, then given any pullback square + +Z ⟶ X₁ +↓ ↓ +X₂ ⟶ X₁ ⨿ X₂ + +`Z` is initial. +-/ +noncomputable def isInitialOfIsPullbackOfCoproduct {Z X₁ X₂ : C} [HasBinaryCoproduct X₁ X₂] + [CoproductDisjoint X₁ X₂] {f : Z ⟶ X₁} {g : Z ⟶ X₂} + {comm : f ≫ (coprod.inl : X₁ ⟶ _ ⨿ X₂) = g ≫ coprod.inr} + (cZ : IsLimit (PullbackCone.mk _ _ comm)) : IsInitial Z := + CoproductDisjoint.isInitialOfIsPullbackOfIsCoproduct (coprodIsCoprod _ _) cZ +#align category_theory.limits.is_initial_of_is_pullback_of_coproduct CategoryTheory.Limits.isInitialOfIsPullbackOfCoproduct + +/-- If the coproduct of `X₁` and `X₂` is disjoint, then provided `X₁ ⟶ X ← X₂` is a coproduct the +pullback is an initial object: + + X₁ + ↓ +X₂ ⟶ X +-/ +noncomputable def isInitialOfPullbackOfIsCoproduct {X X₁ X₂ : C} [CoproductDisjoint X₁ X₂] + {pX₁ : X₁ ⟶ X} {pX₂ : X₂ ⟶ X} [HasPullback pX₁ pX₂] (cX : IsColimit (BinaryCofan.mk pX₁ pX₂)) : + IsInitial (pullback pX₁ pX₂) := + CoproductDisjoint.isInitialOfIsPullbackOfIsCoproduct cX (pullbackIsPullback _ _) +#align category_theory.limits.is_initial_of_pullback_of_is_coproduct CategoryTheory.Limits.isInitialOfPullbackOfIsCoproduct + +/-- If the coproduct of `X₁` and `X₂` is disjoint, the pullback of `X₁ ⟶ X₁ ⨿ X₂` and `X₂ ⟶ X₁ ⨿ X₂` +is initial. +-/ +noncomputable def isInitialOfPullbackOfCoproduct {X₁ X₂ : C} [HasBinaryCoproduct X₁ X₂] + [CoproductDisjoint X₁ X₂] [HasPullback (coprod.inl : X₁ ⟶ _ ⨿ X₂) coprod.inr] : + IsInitial (pullback (coprod.inl : X₁ ⟶ _ ⨿ X₂) coprod.inr) := + isInitialOfIsPullbackOfCoproduct (pullbackIsPullback _ _) +#align category_theory.limits.is_initial_of_pullback_of_coproduct CategoryTheory.Limits.isInitialOfPullbackOfCoproduct + +instance {X₁ X₂ : C} [HasBinaryCoproduct X₁ X₂] [CoproductDisjoint X₁ X₂] : + Mono (coprod.inl : X₁ ⟶ X₁ ⨿ X₂) := + CoproductDisjoint.mono_inl _ _ _ (coprodIsCoprod _ _) + +instance {X₁ X₂ : C} [HasBinaryCoproduct X₁ X₂] [CoproductDisjoint X₁ X₂] : + Mono (coprod.inr : X₂ ⟶ X₁ ⨿ X₂) := + CoproductDisjoint.mono_inr _ _ _ (coprodIsCoprod _ _) + +/-- `C` has disjoint coproducts if every coproduct is disjoint. -/ +class CoproductsDisjoint (C : Type u) [Category.{v} C] where + CoproductDisjoint : ∀ X Y : C, CoproductDisjoint X Y +#align category_theory.limits.coproducts_disjoint CategoryTheory.Limits.CoproductsDisjoint + +attribute [instance] CoproductsDisjoint.CoproductDisjoint + +/-- If `C` has disjoint coproducts, any morphism out of initial is mono. Note it isn't true in +general that `C` has strict initial objects, for instance consider the category of types and +partial functions. -/ +theorem initialMonoClass_of_disjoint_coproducts [CoproductsDisjoint C] : InitialMonoClass C := + { isInitial_mono_from := @fun _I X hI => + CoproductDisjoint.mono_inl X (IsInitial.to hI X) (CategoryTheory.CategoryStruct.id X) + { desc := fun s : BinaryCofan _ _ => s.inr + fac := fun _s j => + Discrete.casesOn j fun j => WalkingPair.casesOn j (hI.hom_ext _ _) (id_comp _) + uniq := fun (_s : BinaryCofan _ _) _m w => + (id_comp _).symm.trans (w ⟨WalkingPair.right⟩) } } +#align category_theory.limits.initial_mono_class_of_disjoint_coproducts CategoryTheory.Limits.initialMonoClass_of_disjoint_coproducts + +end Limits + +end CategoryTheory