/
BinaryProducts.lean
180 lines (141 loc) · 7.92 KB
/
BinaryProducts.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
/-
Copyright (c) 2020 Bhavik Mehta. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Bhavik Mehta
-/
import Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
import Mathlib.CategoryTheory.Limits.Preserves.Basic
#align_import category_theory.limits.preserves.shapes.binary_products from "leanprover-community/mathlib"@"024a4231815538ac739f52d08dd20a55da0d6b23"
/-!
# Preserving binary products
Constructions to relate the notions of preserving binary products and reflecting binary products
to concrete binary fans.
In particular, we show that `ProdComparison G X Y` is an isomorphism iff `G` preserves
the product of `X` and `Y`.
-/
noncomputable section
universe v₁ v₂ u₁ u₂
open CategoryTheory CategoryTheory.Category CategoryTheory.Limits
variable {C : Type u₁} [Category.{v₁} C]
variable {D : Type u₂} [Category.{v₂} D]
variable (G : C ⥤ D)
namespace CategoryTheory.Limits
section
variable {P X Y Z : C} (f : P ⟶ X) (g : P ⟶ Y)
/--
The map of a binary fan is a limit iff the fork consisting of the mapped morphisms is a limit. This
essentially lets us commute `BinaryFan.mk` with `Functor.mapCone`.
-/
def isLimitMapConeBinaryFanEquiv :
IsLimit (G.mapCone (BinaryFan.mk f g)) ≃ IsLimit (BinaryFan.mk (G.map f) (G.map g)) :=
(IsLimit.postcomposeHomEquiv (diagramIsoPair _) _).symm.trans
(IsLimit.equivIsoLimit
(Cones.ext (Iso.refl _)
(by rintro (_ | _) <;> simp)))
#align category_theory.limits.is_limit_map_cone_binary_fan_equiv CategoryTheory.Limits.isLimitMapConeBinaryFanEquiv
/-- The property of preserving products expressed in terms of binary fans. -/
def mapIsLimitOfPreservesOfIsLimit [PreservesLimit (pair X Y) G] (l : IsLimit (BinaryFan.mk f g)) :
IsLimit (BinaryFan.mk (G.map f) (G.map g)) :=
isLimitMapConeBinaryFanEquiv G f g (PreservesLimit.preserves l)
#align category_theory.limits.map_is_limit_of_preserves_of_is_limit CategoryTheory.Limits.mapIsLimitOfPreservesOfIsLimit
/-- The property of reflecting products expressed in terms of binary fans. -/
def isLimitOfReflectsOfMapIsLimit [ReflectsLimit (pair X Y) G]
(l : IsLimit (BinaryFan.mk (G.map f) (G.map g))) : IsLimit (BinaryFan.mk f g) :=
ReflectsLimit.reflects ((isLimitMapConeBinaryFanEquiv G f g).symm l)
#align category_theory.limits.is_limit_of_reflects_of_map_is_limit CategoryTheory.Limits.isLimitOfReflectsOfMapIsLimit
variable (X Y) [HasBinaryProduct X Y]
/-- If `G` preserves binary products and `C` has them, then the binary fan constructed of the mapped
morphisms of the binary product cone is a limit.
-/
def isLimitOfHasBinaryProductOfPreservesLimit [PreservesLimit (pair X Y) G] :
IsLimit (BinaryFan.mk (G.map (Limits.prod.fst : X ⨯ Y ⟶ X)) (G.map Limits.prod.snd)) :=
mapIsLimitOfPreservesOfIsLimit G _ _ (prodIsProd X Y)
#align category_theory.limits.is_limit_of_has_binary_product_of_preserves_limit CategoryTheory.Limits.isLimitOfHasBinaryProductOfPreservesLimit
variable [HasBinaryProduct (G.obj X) (G.obj Y)]
/-- If the product comparison map for `G` at `(X,Y)` is an isomorphism, then `G` preserves the
pair of `(X,Y)`.
-/
def PreservesLimitPair.ofIsoProdComparison [i : IsIso (prodComparison G X Y)] :
PreservesLimit (pair X Y) G := by
apply preservesLimitOfPreservesLimitCone (prodIsProd X Y)
apply (isLimitMapConeBinaryFanEquiv _ _ _).symm _
refine @IsLimit.ofPointIso _ _ _ _ _ _ _ (limit.isLimit (pair (G.obj X) (G.obj Y))) ?_
apply i
#align category_theory.limits.preserves_limit_pair.of_iso_prod_comparison CategoryTheory.Limits.PreservesLimitPair.ofIsoProdComparison
variable [PreservesLimit (pair X Y) G]
/-- If `G` preserves the product of `(X,Y)`, then the product comparison map for `G` at `(X,Y)` is
an isomorphism.
-/
def PreservesLimitPair.iso : G.obj (X ⨯ Y) ≅ G.obj X ⨯ G.obj Y :=
IsLimit.conePointUniqueUpToIso (isLimitOfHasBinaryProductOfPreservesLimit G X Y) (limit.isLimit _)
#align category_theory.limits.preserves_limit_pair.iso CategoryTheory.Limits.PreservesLimitPair.iso
@[simp]
theorem PreservesLimitPair.iso_hom : (PreservesLimitPair.iso G X Y).hom = prodComparison G X Y :=
rfl
#align category_theory.limits.preserves_limit_pair.iso_hom CategoryTheory.Limits.PreservesLimitPair.iso_hom
instance : IsIso (prodComparison G X Y) := by
rw [← PreservesLimitPair.iso_hom]
infer_instance
end
section
variable {P X Y Z : C} (f : X ⟶ P) (g : Y ⟶ P)
/-- The map of a binary cofan is a colimit iff
the cofork consisting of the mapped morphisms is a colimit.
This essentially lets us commute `BinaryCofan.mk` with `Functor.mapCocone`.
-/
def isColimitMapCoconeBinaryCofanEquiv :
IsColimit (Functor.mapCocone G (BinaryCofan.mk f g))
≃ IsColimit (BinaryCofan.mk (G.map f) (G.map g)) :=
(IsColimit.precomposeHomEquiv (diagramIsoPair _).symm _).symm.trans
(IsColimit.equivIsoColimit
(Cocones.ext (Iso.refl _)
(by rintro (_ | _) <;> simp)))
#align category_theory.limits.is_colimit_map_cocone_binary_cofan_equiv CategoryTheory.Limits.isColimitMapCoconeBinaryCofanEquiv
/-- The property of preserving coproducts expressed in terms of binary cofans. -/
def mapIsColimitOfPreservesOfIsColimit [PreservesColimit (pair X Y) G]
(l : IsColimit (BinaryCofan.mk f g)) : IsColimit (BinaryCofan.mk (G.map f) (G.map g)) :=
isColimitMapCoconeBinaryCofanEquiv G f g (PreservesColimit.preserves l)
#align category_theory.limits.map_is_colimit_of_preserves_of_is_colimit CategoryTheory.Limits.mapIsColimitOfPreservesOfIsColimit
/-- The property of reflecting coproducts expressed in terms of binary cofans. -/
def isColimitOfReflectsOfMapIsColimit [ReflectsColimit (pair X Y) G]
(l : IsColimit (BinaryCofan.mk (G.map f) (G.map g))) : IsColimit (BinaryCofan.mk f g) :=
ReflectsColimit.reflects ((isColimitMapCoconeBinaryCofanEquiv G f g).symm l)
#align category_theory.limits.is_colimit_of_reflects_of_map_is_colimit CategoryTheory.Limits.isColimitOfReflectsOfMapIsColimit
variable (X Y) [HasBinaryCoproduct X Y]
/--
If `G` preserves binary coproducts and `C` has them, then the binary cofan constructed of the mapped
morphisms of the binary product cocone is a colimit.
-/
def isColimitOfHasBinaryCoproductOfPreservesColimit [PreservesColimit (pair X Y) G] :
IsColimit (BinaryCofan.mk (G.map (Limits.coprod.inl : X ⟶ X ⨿ Y)) (G.map Limits.coprod.inr)) :=
mapIsColimitOfPreservesOfIsColimit G _ _ (coprodIsCoprod X Y)
#align category_theory.limits.is_colimit_of_has_binary_coproduct_of_preserves_colimit CategoryTheory.Limits.isColimitOfHasBinaryCoproductOfPreservesColimit
variable [HasBinaryCoproduct (G.obj X) (G.obj Y)]
/-- If the coproduct comparison map for `G` at `(X,Y)` is an isomorphism, then `G` preserves the
pair of `(X,Y)`.
-/
def PreservesColimitPair.ofIsoCoprodComparison [i : IsIso (coprodComparison G X Y)] :
PreservesColimit (pair X Y) G := by
apply preservesColimitOfPreservesColimitCocone (coprodIsCoprod X Y)
apply (isColimitMapCoconeBinaryCofanEquiv _ _ _).symm _
refine @IsColimit.ofPointIso _ _ _ _ _ _ _ (colimit.isColimit (pair (G.obj X) (G.obj Y))) ?_
apply i
#align category_theory.limits.preserves_colimit_pair.of_iso_coprod_comparison CategoryTheory.Limits.PreservesColimitPair.ofIsoCoprodComparison
variable [PreservesColimit (pair X Y) G]
/--
If `G` preserves the coproduct of `(X,Y)`, then the coproduct comparison map for `G` at `(X,Y)` is
an isomorphism.
-/
def PreservesColimitPair.iso : G.obj X ⨿ G.obj Y ≅ G.obj (X ⨿ Y) :=
IsColimit.coconePointUniqueUpToIso (colimit.isColimit _)
(isColimitOfHasBinaryCoproductOfPreservesColimit G X Y)
#align category_theory.limits.preserves_colimit_pair.iso CategoryTheory.Limits.PreservesColimitPair.iso
@[simp]
theorem PreservesColimitPair.iso_hom :
(PreservesColimitPair.iso G X Y).hom = coprodComparison G X Y := rfl
#align category_theory.limits.preserves_colimit_pair.iso_hom CategoryTheory.Limits.PreservesColimitPair.iso_hom
instance : IsIso (coprodComparison G X Y) := by
rw [← PreservesColimitPair.iso_hom]
infer_instance
end
end CategoryTheory.Limits