Skip to content

Commit 8a946ee

Browse files
joelrioujoelriou
committed
feat: port CategoryTheory.Limits.Constructions.ZeroObjects (#2823)
1 parent b8574d7 commit 8a946ee

File tree

2 files changed

+234
-0
lines changed

2 files changed

+234
-0
lines changed

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -325,6 +325,7 @@ import Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProduct
325325
import Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
326326
import Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
327327
import Mathlib.CategoryTheory.Limits.Constructions.Pullbacks
328+
import Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects
328329
import Mathlib.CategoryTheory.Limits.Creates
329330
import Mathlib.CategoryTheory.Limits.EssentiallySmall
330331
import Mathlib.CategoryTheory.Limits.ExactFunctor

‎Mathlib/CategoryTheory/Limits/Constructions/ZeroObjects.lean‎

Lines changed: 233 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,233 @@
1+
/-
2+
Copyright (c) 2022 Scott Morrison. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Scott Morrison
5+
6+
! This file was ported from Lean 3 source module category_theory.limits.constructions.zero_objects
7+
! leanprover-community/mathlib commit 52a270e2ea4e342c2587c106f8be904524214a4b
8+
! Please do not edit these lines, except to modify the commit id
9+
! if you have ported upstream changes.
10+
-/
11+
import Mathlib.CategoryTheory.Limits.Shapes.Pullbacks
12+
import Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
13+
import Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
14+
15+
/-!
16+
# Limits involving zero objects
17+
18+
Binary products and coproducts with a zero object always exist,
19+
and pullbacks/pushouts over a zero object are products/coproducts.
20+
-/
21+
22+
23+
noncomputable section
24+
25+
open CategoryTheory
26+
27+
variable {C : Type _} [Category C]
28+
29+
namespace CategoryTheory.Limits
30+
31+
variable [HasZeroObject C] [HasZeroMorphisms C]
32+
33+
open ZeroObject
34+
35+
/-- The limit cone for the product with a zero object. -/
36+
def binaryFanZeroLeft (X : C) : BinaryFan (0 : C) X :=
37+
BinaryFan.mk 0 (𝟙 X)
38+
#align category_theory.limits.binary_fan_zero_left CategoryTheory.Limits.binaryFanZeroLeft
39+
40+
/-- The limit cone for the product with a zero object is limiting. -/
41+
def binaryFanZeroLeftIsLimit (X : C) : IsLimit (binaryFanZeroLeft X) :=
42+
BinaryFan.isLimitMk (fun s => BinaryFan.snd s) (by aesop_cat) (by aesop_cat)
43+
(fun s m _ h₂ => by simpa using h₂)
44+
#align category_theory.limits.binary_fan_zero_left_is_limit CategoryTheory.Limits.binaryFanZeroLeftIsLimit
45+
46+
instance hasBinaryProduct_zero_left (X : C) : HasBinaryProduct (0 : C) X :=
47+
HasLimit.mk ⟨_, binaryFanZeroLeftIsLimit X⟩
48+
#align category_theory.limits.has_binary_product_zero_left CategoryTheory.Limits.hasBinaryProduct_zero_left
49+
50+
/-- A zero object is a left unit for categorical product. -/
51+
def zeroProdIso (X : C) : (0 : C) ⨯ X ≅ X :=
52+
limit.isoLimitCone ⟨_, binaryFanZeroLeftIsLimit X⟩
53+
#align category_theory.limits.zero_prod_iso CategoryTheory.Limits.zeroProdIso
54+
55+
@[simp]
56+
theorem zeroProdIso_hom (X : C) : (zeroProdIso X).hom = prod.snd :=
57+
rfl
58+
#align category_theory.limits.zero_prod_iso_hom CategoryTheory.Limits.zeroProdIso_hom
59+
60+
@[simp]
61+
theorem zeroProdIso_inv_snd (X : C) : (zeroProdIso X).inv ≫ prod.snd = 𝟙 X := by
62+
dsimp [zeroProdIso, binaryFanZeroLeft]
63+
simp
64+
#align category_theory.limits.zero_prod_iso_inv_snd CategoryTheory.Limits.zeroProdIso_inv_snd
65+
66+
/-- The limit cone for the product with a zero object. -/
67+
def binaryFanZeroRight (X : C) : BinaryFan X (0 : C) :=
68+
BinaryFan.mk (𝟙 X) 0
69+
#align category_theory.limits.binary_fan_zero_right CategoryTheory.Limits.binaryFanZeroRight
70+
71+
/-- The limit cone for the product with a zero object is limiting. -/
72+
def binaryFanZeroRightIsLimit (X : C) : IsLimit (binaryFanZeroRight X) :=
73+
BinaryFan.isLimitMk (fun s => BinaryFan.fst s) (by aesop_cat) (by aesop_cat)
74+
(fun s m h₁ => by simpa using h₁)
75+
#align category_theory.limits.binary_fan_zero_right_is_limit CategoryTheory.Limits.binaryFanZeroRightIsLimit
76+
77+
instance hasBinaryProduct_zero_right (X : C) : HasBinaryProduct X (0 : C) :=
78+
HasLimit.mk ⟨_, binaryFanZeroRightIsLimit X⟩
79+
#align category_theory.limits.has_binary_product_zero_right CategoryTheory.Limits.hasBinaryProduct_zero_right
80+
81+
/-- A zero object is a right unit for categorical product. -/
82+
def prodZeroIso (X : C) : X ⨯ (0 : C) ≅ X :=
83+
limit.isoLimitCone ⟨_, binaryFanZeroRightIsLimit X⟩
84+
#align category_theory.limits.prod_zero_iso CategoryTheory.Limits.prodZeroIso
85+
86+
@[simp]
87+
theorem prodZeroIso_hom (X : C) : (prodZeroIso X).hom = prod.fst :=
88+
rfl
89+
#align category_theory.limits.prod_zero_iso_hom CategoryTheory.Limits.prodZeroIso_hom
90+
91+
@[simp]
92+
theorem prodZeroIso_iso_inv_snd (X : C) : (prodZeroIso X).inv ≫ prod.fst = 𝟙 X := by
93+
dsimp [prodZeroIso, binaryFanZeroRight]
94+
simp
95+
#align category_theory.limits.prod_zero_iso_iso_inv_snd CategoryTheory.Limits.prodZeroIso_iso_inv_snd
96+
97+
/-- The colimit cocone for the coproduct with a zero object. -/
98+
def binaryCofanZeroLeft (X : C) : BinaryCofan (0 : C) X :=
99+
BinaryCofan.mk 0 (𝟙 X)
100+
#align category_theory.limits.binary_cofan_zero_left CategoryTheory.Limits.binaryCofanZeroLeft
101+
102+
/-- The colimit cocone for the coproduct with a zero object is colimiting. -/
103+
def binaryCofanZeroLeftIsColimit (X : C) : IsColimit (binaryCofanZeroLeft X) :=
104+
BinaryCofan.isColimitMk (fun s => BinaryCofan.inr s) (by aesop_cat) (by aesop_cat)
105+
(fun s m _ h₂ => by simpa using h₂)
106+
#align category_theory.limits.binary_cofan_zero_left_is_colimit CategoryTheory.Limits.binaryCofanZeroLeftIsColimit
107+
108+
instance hasBinaryCoproduct_zero_left (X : C) : HasBinaryCoproduct (0 : C) X :=
109+
HasColimit.mk ⟨_, binaryCofanZeroLeftIsColimit X⟩
110+
#align category_theory.limits.has_binary_coproduct_zero_left CategoryTheory.Limits.hasBinaryCoproduct_zero_left
111+
112+
/-- A zero object is a left unit for categorical coproduct. -/
113+
def zeroCoprodIso (X : C) : (0 : C) ⨿ X ≅ X :=
114+
colimit.isoColimitCocone ⟨_, binaryCofanZeroLeftIsColimit X⟩
115+
#align category_theory.limits.zero_coprod_iso CategoryTheory.Limits.zeroCoprodIso
116+
117+
@[simp]
118+
theorem inr_zeroCoprodIso_hom (X : C) : coprod.inr ≫ (zeroCoprodIso X).hom = 𝟙 X := by
119+
dsimp [zeroCoprodIso, binaryCofanZeroLeft]
120+
simp
121+
#align category_theory.limits.inr_zero_coprod_iso_hom CategoryTheory.Limits.inr_zeroCoprodIso_hom
122+
123+
@[simp]
124+
theorem zeroCoprodIso_inv (X : C) : (zeroCoprodIso X).inv = coprod.inr :=
125+
rfl
126+
#align category_theory.limits.zero_coprod_iso_inv CategoryTheory.Limits.zeroCoprodIso_inv
127+
128+
/-- The colimit cocone for the coproduct with a zero object. -/
129+
def binaryCofanZeroRight (X : C) : BinaryCofan X (0 : C) :=
130+
BinaryCofan.mk (𝟙 X) 0
131+
#align category_theory.limits.binary_cofan_zero_right CategoryTheory.Limits.binaryCofanZeroRight
132+
133+
/-- The colimit cocone for the coproduct with a zero object is colimiting. -/
134+
def binaryCofanZeroRightIsColimit (X : C) : IsColimit (binaryCofanZeroRight X) :=
135+
BinaryCofan.isColimitMk (fun s => BinaryCofan.inl s) (by aesop_cat) (by aesop_cat)
136+
(fun s m h₁ _ => by simpa using h₁)
137+
#align category_theory.limits.binary_cofan_zero_right_is_colimit CategoryTheory.Limits.binaryCofanZeroRightIsColimit
138+
139+
instance hasBinaryCoproduct_zero_right (X : C) : HasBinaryCoproduct X (0 : C) :=
140+
HasColimit.mk ⟨_, binaryCofanZeroRightIsColimit X⟩
141+
#align category_theory.limits.has_binary_coproduct_zero_right CategoryTheory.Limits.hasBinaryCoproduct_zero_right
142+
143+
/-- A zero object is a right unit for categorical coproduct. -/
144+
def coprodZeroIso (X : C) : X ⨿ (0 : C) ≅ X :=
145+
colimit.isoColimitCocone ⟨_, binaryCofanZeroRightIsColimit X⟩
146+
#align category_theory.limits.coprod_zero_iso CategoryTheory.Limits.coprodZeroIso
147+
148+
@[simp]
149+
theorem inr_coprod_zeroiso_hom (X : C) : coprod.inl ≫ (coprodZeroIso X).hom = 𝟙 X := by
150+
dsimp [coprodZeroIso, binaryCofanZeroRight]
151+
simp
152+
#align category_theory.limits.inr_coprod_zeroiso_hom CategoryTheory.Limits.inr_coprod_zeroiso_hom
153+
154+
@[simp]
155+
theorem coprodZeroIso_inv (X : C) : (coprodZeroIso X).inv = coprod.inl :=
156+
rfl
157+
#align category_theory.limits.coprod_zero_iso_inv CategoryTheory.Limits.coprodZeroIso_inv
158+
159+
instance hasPullback_over_zero (X Y : C) [HasBinaryProduct X Y] :
160+
HasPullback (0 : X ⟶ 0) (0 : Y ⟶ 0) :=
161+
HasLimit.mk
162+
⟨_, isPullbackOfIsTerminalIsProduct _ _ _ _ HasZeroObject.zeroIsTerminal (prodIsProd X Y)⟩
163+
#align category_theory.limits.has_pullback_over_zero CategoryTheory.Limits.hasPullback_over_zero
164+
165+
/-- The pullback over the zeron object is the product. -/
166+
def pullbackZeroZeroIso (X Y : C) [HasBinaryProduct X Y] :
167+
pullback (0 : X ⟶ 0) (0 : Y ⟶ 0) ≅ X ⨯ Y :=
168+
limit.isoLimitCone
169+
⟨_, isPullbackOfIsTerminalIsProduct _ _ _ _ HasZeroObject.zeroIsTerminal (prodIsProd X Y)⟩
170+
#align category_theory.limits.pullback_zero_zero_iso CategoryTheory.Limits.pullbackZeroZeroIso
171+
172+
@[simp]
173+
theorem pullbackZeroZeroIso_inv_fst (X Y : C) [HasBinaryProduct X Y] :
174+
(pullbackZeroZeroIso X Y).inv ≫ pullback.fst = prod.fst := by
175+
dsimp [pullbackZeroZeroIso]
176+
simp
177+
#align category_theory.limits.pullback_zero_zero_iso_inv_fst CategoryTheory.Limits.pullbackZeroZeroIso_inv_fst
178+
179+
@[simp]
180+
theorem pullbackZeroZeroIso_inv_snd (X Y : C) [HasBinaryProduct X Y] :
181+
(pullbackZeroZeroIso X Y).inv ≫ pullback.snd = prod.snd := by
182+
dsimp [pullbackZeroZeroIso]
183+
simp
184+
#align category_theory.limits.pullback_zero_zero_iso_inv_snd CategoryTheory.Limits.pullbackZeroZeroIso_inv_snd
185+
186+
@[simp]
187+
theorem pullbackZeroZeroIso_hom_fst (X Y : C) [HasBinaryProduct X Y] :
188+
(pullbackZeroZeroIso X Y).hom ≫ prod.fst = pullback.fst := by simp [← Iso.eq_inv_comp]
189+
#align category_theory.limits.pullback_zero_zero_iso_hom_fst CategoryTheory.Limits.pullbackZeroZeroIso_hom_fst
190+
191+
@[simp]
192+
theorem pullbackZeroZeroIso_hom_snd (X Y : C) [HasBinaryProduct X Y] :
193+
(pullbackZeroZeroIso X Y).hom ≫ prod.snd = pullback.snd := by simp [← Iso.eq_inv_comp]
194+
#align category_theory.limits.pullback_zero_zero_iso_hom_snd CategoryTheory.Limits.pullbackZeroZeroIso_hom_snd
195+
196+
instance hasPushout_over_zero (X Y : C) [HasBinaryCoproduct X Y] :
197+
HasPushout (0 : 0 ⟶ X) (0 : 0 ⟶ Y) :=
198+
HasColimit.mk
199+
⟨_, isPushoutOfIsInitialIsCoproduct _ _ _ _ HasZeroObject.zeroIsInitial (coprodIsCoprod X Y)⟩
200+
#align category_theory.limits.has_pushout_over_zero CategoryTheory.Limits.hasPushout_over_zero
201+
202+
/-- The pushout over the zero object is the coproduct. -/
203+
def pushoutZeroZeroIso (X Y : C) [HasBinaryCoproduct X Y] :
204+
pushout (0 : 0 ⟶ X) (0 : 0 ⟶ Y) ≅ X ⨿ Y :=
205+
colimit.isoColimitCocone
206+
⟨_, isPushoutOfIsInitialIsCoproduct _ _ _ _ HasZeroObject.zeroIsInitial (coprodIsCoprod X Y)⟩
207+
#align category_theory.limits.pushout_zero_zero_iso CategoryTheory.Limits.pushoutZeroZeroIso
208+
209+
@[simp]
210+
theorem inl_pushoutZeroZeroIso_hom (X Y : C) [HasBinaryCoproduct X Y] :
211+
pushout.inl ≫ (pushoutZeroZeroIso X Y).hom = coprod.inl := by
212+
dsimp [pushoutZeroZeroIso]
213+
simp
214+
#align category_theory.limits.inl_pushout_zero_zero_iso_hom CategoryTheory.Limits.inl_pushoutZeroZeroIso_hom
215+
216+
@[simp]
217+
theorem inr_pushoutZeroZeroIso_hom (X Y : C) [HasBinaryCoproduct X Y] :
218+
pushout.inr ≫ (pushoutZeroZeroIso X Y).hom = coprod.inr := by
219+
dsimp [pushoutZeroZeroIso]
220+
simp
221+
#align category_theory.limits.inr_pushout_zero_zero_iso_hom CategoryTheory.Limits.inr_pushoutZeroZeroIso_hom
222+
223+
@[simp]
224+
theorem inl_pushoutZeroZeroIso_inv (X Y : C) [HasBinaryCoproduct X Y] :
225+
coprod.inl ≫ (pushoutZeroZeroIso X Y).inv = pushout.inl := by simp [Iso.comp_inv_eq]
226+
#align category_theory.limits.inl_pushout_zero_zero_iso_inv CategoryTheory.Limits.inl_pushoutZeroZeroIso_inv
227+
228+
@[simp]
229+
theorem inr_pushoutZeroZeroIso_inv (X Y : C) [HasBinaryCoproduct X Y] :
230+
coprod.inr ≫ (pushoutZeroZeroIso X Y).inv = pushout.inr := by simp [Iso.comp_inv_eq]
231+
#align category_theory.limits.inr_pushout_zero_zero_iso_inv CategoryTheory.Limits.inr_pushoutZeroZeroIso_inv
232+
233+
end CategoryTheory.Limits

0 commit comments

Comments
 (0)