Skip to content

Commit 6939380

Browse files
YaelDilliesYaelDillies
committed
feat: a binary fan in Over X is the same thing as a pullback cone to X (#23723)
From Toric Co-authored-by: Andrew Yang <the.erd.one@gmail.com> Co-authored-by: Michał Mrugała <kiolterino@gmail.com>
1 parent 9608176 commit 6939380

File tree

2 files changed

+207
-44
lines changed

2 files changed

+207
-44
lines changed

‎Mathlib/CategoryTheory/Limits/Constructions/Over/Products.lean‎

Lines changed: 197 additions & 44 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,14 @@ import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq
1111
Shows that products in the over category can be derived from wide pullbacks in the base category.
1212
The main result is `over_product_of_widePullback`, which says that if `C` has `J`-indexed wide
1313
pullbacks, then `Over B` has `J`-indexed products.
14+
15+
Note that the binary case is done separately to ensure defeqs with the pullback in the base
16+
category.
17+
18+
## TODO
19+
20+
* Generalise from arbitrary products to arbitrary limits. This is done in Toric.
21+
* Dualise to get the `Under X` results.
1422
-/
1523

1624

@@ -20,9 +28,196 @@ open CategoryTheory CategoryTheory.Limits
2028

2129
variable {J : Type w}
2230
variable {C : Type u} [Category.{v} C]
23-
variable {X : C}
31+
variable {X Y Z : C}
32+
33+
/-!
34+
### Binary products
35+
36+
In this section we construct binary products in `Over X` and binary coproducts in `Under X`
37+
explicitly as the pullbacks and pushouts of binary (co)fans in the base category.
38+
39+
For `Over X`, one could construct these binary products from the general theory of arbitrary
40+
products from the next section, ie
41+
```
42+
(Cones.postcomposeEquivalence (diagramIsoCospan _).symm).trans
43+
(Over.ConstructProducts.conesEquiv _ (pair (Over.mk f) (Over.mk g)))
44+
```
45+
but this gives worse defeqs.
46+
47+
For `Under X`, there is currently no general theory of arbitrary coproducts.
48+
-/
49+
50+
namespace CategoryTheory.Limits
51+
section Over
52+
variable {f : Y ⟶ X} {g : Z ⟶ X}
53+
54+
/-- Pullback cones to `X` are the same thing as binary fans in `Over X`. -/
55+
@[simps]
56+
def pullbackConeEquivBinaryFan : PullbackCone f g ≌ BinaryFan (Over.mk f) (.mk g) where
57+
functor.obj c := .mk (Over.homMk (U := .mk (c.fst ≫ f)) (V := .mk f) c.fst rfl)
58+
(Over.homMk (U := .mk (c.fst ≫ f)) (V := .mk g) c.snd c.condition.symm)
59+
functor.map {c₁ c₂} a := { hom := Over.homMk a.hom, w := by rintro (_|_) <;> aesop_cat }
60+
inverse.obj c := PullbackCone.mk c.fst.left c.snd.left (c.fst.w.trans c.snd.w.symm)
61+
inverse.map {c₁ c₂} a := {
62+
hom := a.hom.left
63+
w := by rintro (_|_|_) <;> simp [← Over.comp_left_assoc, ← Over.comp_left]
64+
}
65+
unitIso := NatIso.ofComponents (fun c ↦ c.eta) (by intros; ext; dsimp; simp)
66+
counitIso := NatIso.ofComponents (fun X ↦ BinaryFan.ext (Over.isoMk (Iso.refl _)
67+
(by simpa using X.fst.w.symm)) (by ext; dsimp; simp) (by ext; dsimp; simp))
68+
(by intros; ext; dsimp; simp [BinaryFan.ext])
69+
functor_unitIso_comp c := by ext; dsimp; simp [BinaryFan.ext]
70+
71+
/-- A binary fan in `Over X` is a limit if its corresponding pullback cone to `X` is a limit. -/
72+
-- `IsLimit.ofConeEquiv` isn't used here because the lift it defines is `𝟙 _ ≫ pullback.lift`.
73+
-- TODO: Define `IsLimit.copy`?
74+
@[simps!]
75+
def IsLimit.pullbackConeEquivBinaryFanFunctor {c : PullbackCone f g} (hc : IsLimit c) :
76+
IsLimit <| pullbackConeEquivBinaryFan.functor.obj c :=
77+
BinaryFan.isLimitMk
78+
-- TODO: Drop `BinaryFan.IsLimit.lift'`. Instead provide the lemmas it bundles separately.
79+
-- TODO: Define `abbrev BinaryFan.IsLimit (c : BinaryFan X Y) := IsLimit c` for dot notation?
80+
(fun s ↦ Over.homMk (hc.lift <| pullbackConeEquivBinaryFan.inverse.obj s) <| by
81+
simpa using s.fst.w)
82+
(fun s ↦ Over.OverMorphism.ext (hc.fac _ _)) (fun s ↦ Over.OverMorphism.ext (hc.fac _ _))
83+
fun s m e₁ e₂ ↦ by
84+
ext1
85+
apply PullbackCone.IsLimit.hom_ext hc
86+
· simpa using congr(($e₁).left)
87+
· simpa using congr(($e₂).left)
88+
89+
/-- A pullback cone to `X` is a limit if its corresponding binary fan in `Over X` is a limit. -/
90+
-- This could also be `(IsLimit.ofConeEquiv pullbackConeEquivBinaryFan.symm).symm hc`, but possibly
91+
-- bad defeqs?
92+
def IsLimit.pullbackConeEquivBinaryFanInverse {c : BinaryFan (Over.mk f) (.mk g)} (hc : IsLimit c) :
93+
IsLimit <| pullbackConeEquivBinaryFan.inverse.obj c :=
94+
PullbackCone.IsLimit.mk
95+
(c.fst.w.trans c.snd.w.symm)
96+
(fun s ↦ (hc.lift <| pullbackConeEquivBinaryFan.functor.obj s).left)
97+
(fun s ↦ by simpa only using congr($(hc.fac _ _).left))
98+
(fun s ↦ by simpa only using congr($(hc.fac _ _).left))
99+
<| fun s m hm₁ hm₂ ↦ by
100+
change PullbackCone f g at s
101+
have := hc.uniq (pullbackConeEquivBinaryFan.functor.obj s) (Over.homMk m <| by
102+
have := c.fst.w
103+
simp only [pair_obj_left, Over.mk_left, Functor.id_obj, pair_obj_right,
104+
Functor.const_obj_obj, Over.mk_hom, Functor.id_map, CostructuredArrow.right_eq_id,
105+
Discrete.functor_map_id, Category.comp_id] at hm₁ this
106+
simp [← hm₁, this])
107+
(by rintro (_ | _) <;> ext <;> simpa)
108+
exact congr(($this).left)
109+
110+
end Over
111+
112+
section Under
113+
variable {f : X ⟶ Y} {g : X ⟶ Z}
114+
115+
/-- Pushout cocones from `X` are the same thing as binary cofans in `Under X`. -/
116+
@[simps]
117+
def pushoutCoconeEquivBinaryCofan : PushoutCocone f g ≌ BinaryCofan (Under.mk f) (.mk g) where
118+
functor.obj c := .mk (Under.homMk (U := .mk f) (V := .mk (f ≫ c.inl)) c.inl rfl)
119+
(Under.homMk (U := .mk g) (V := .mk (f ≫ c.inl)) c.inr c.condition.symm)
120+
functor.map {c₁ c₂} a := { hom := Under.homMk a.hom, w := by rintro (_|_) <;> aesop_cat }
121+
inverse.obj c := .mk c.inl.right c.inr.right (c.inl.w.symm.trans c.inr.w)
122+
inverse.map {c₁ c₂} a := {
123+
hom := a.hom.right
124+
w := by rintro (_|_|_) <;> dsimp <;> simp [← Under.comp_right]
125+
}
126+
unitIso := NatIso.ofComponents (fun c ↦ c.eta) (fun f ↦ by ext; dsimp; simp)
127+
counitIso := NatIso.ofComponents (fun X ↦ BinaryCofan.ext (Under.isoMk (.refl _)
128+
(by dsimp; simpa using X.inl.w.symm)) (by ext; dsimp; simp) (by ext; dsimp; simp))
129+
(by intros; ext; dsimp; simp)
130+
functor_unitIso_comp c := by ext; dsimp; simp
131+
132+
/-- A binary cofan in `Under X` is a colimit if its corresponding pushout cocone from `X` is a
133+
colimit. -/
134+
-- `IsColimit.ofCoconeEquiv` isn't used here because the lift it defines is `pushout.desc ≫ 𝟙 _`.
135+
-- TODO: Define `IsColimit.copy`?
136+
@[simps!]
137+
def IsColimit.pushoutCoconeEquivBinaryCofanFunctor {c : PushoutCocone f g} (hc : IsColimit c) :
138+
IsColimit <| pushoutCoconeEquivBinaryCofan.functor.obj c :=
139+
BinaryCofan.isColimitMk
140+
(fun s ↦ Under.homMk
141+
(hc.desc (PushoutCocone.mk s.inl.right s.inr.right (s.inl.w.symm.trans s.inr.w))) <| by
142+
simpa using s.inl.w.symm)
143+
(fun s ↦ Under.UnderMorphism.ext (hc.fac _ _)) (fun s ↦ Under.UnderMorphism.ext (hc.fac _ _))
144+
fun s m e₁ e₂ ↦ by
145+
ext1
146+
refine PushoutCocone.IsColimit.hom_ext hc ?_ ?_
147+
· simpa using congr(($e₁).right)
148+
· simpa using congr(($e₂).right)
149+
150+
/-- A pushout cocone from `X` is a colimit if its corresponding binary cofan in `Under X` is a
151+
colimit. -/
152+
-- This could also be `(IsColimit.ofCoconeEquiv pushoutCoconeEquivBinaryCofan.symm).symm hc`,
153+
-- but possibly bad defeqs?
154+
def IsColimit.pushoutCoconeEquivBinaryCofanInverse {c : BinaryCofan (Under.mk f) (.mk g)}
155+
(hc : IsColimit c) : IsColimit <| pushoutCoconeEquivBinaryCofan.inverse.obj c :=
156+
PushoutCocone.IsColimit.mk
157+
(c.inl.w.symm.trans c.inr.w)
158+
(fun s ↦ (hc.desc <| pushoutCoconeEquivBinaryCofan.functor.obj s).right)
159+
(fun s ↦ by simpa only using congr($(hc.fac _ _).right))
160+
(fun s ↦ by simpa only using congr($(hc.fac _ _).right))
161+
<| fun s m hm₁ hm₂ ↦ by
162+
change PushoutCocone f g at s
163+
have := hc.uniq (pushoutCoconeEquivBinaryCofan.functor.obj s) (Under.homMk m <| by
164+
have := c.inl.w
165+
simp only [pair_obj_left, Functor.const_obj_obj, Functor.id_obj, StructuredArrow.left_eq_id,
166+
Discrete.functor_map_id, Category.id_comp, Under.mk_right, Under.mk_hom, Functor.id_map,
167+
pair_obj_right] at this hm₁
168+
simp [← hm₁, ← Category.assoc, ← this])
169+
(by rintro (_ | _) <;> ext <;> simpa)
170+
exact congr(($this).right)
171+
172+
end Under
173+
end Limits
174+
175+
namespace Over
176+
section BinaryProduct
177+
variable {X : C} {Y Z : Over X}
178+
179+
open Limits
180+
181+
lemma isPullback_of_binaryFan_isLimit (c : BinaryFan Y Z) (hc : IsLimit c) :
182+
IsPullback c.fst.left c.snd.left Y.hom Z.hom :=
183+
⟨by simp, ⟨hc.pullbackConeEquivBinaryFanInverse⟩⟩
184+
185+
variable (Y Z) [HasPullback Y.hom Z.hom] [HasBinaryProduct Y Z]
24186

25-
namespace CategoryTheory.Over
187+
/-- The product of `Y` and `Z` in `Over X` is isomorpic to `Y ×ₓ Z`. -/
188+
noncomputable
189+
def prodLeftIsoPullback :
190+
(Y ⨯ Z).left ≅ pullback Y.hom Z.hom :=
191+
(Over.isPullback_of_binaryFan_isLimit _ (prodIsProd Y Z)).isoPullback
192+
193+
@[reassoc (attr := simp)]
194+
lemma prodLeftIsoPullback_hom_fst :
195+
(prodLeftIsoPullback Y Z).hom ≫ pullback.fst _ _ = (prod.fst (X := Y)).left :=
196+
IsPullback.isoPullback_hom_fst _
197+
198+
@[reassoc (attr := simp)]
199+
lemma prodLeftIsoPullback_hom_snd :
200+
(prodLeftIsoPullback Y Z).hom ≫ pullback.snd _ _ = (prod.snd (X := Y)).left :=
201+
IsPullback.isoPullback_hom_snd _
202+
203+
@[reassoc (attr := simp)]
204+
lemma prodLeftIsoPullback_inv_fst :
205+
(prodLeftIsoPullback Y Z).inv ≫ (prod.fst (X := Y)).left = pullback.fst _ _ :=
206+
IsPullback.isoPullback_inv_fst _
207+
208+
@[reassoc (attr := simp)]
209+
lemma prodLeftIsoPullback_inv_snd :
210+
(prodLeftIsoPullback Y Z).inv ≫ (prod.snd (X := Y)).left = pullback.snd _ _ :=
211+
IsPullback.isoPullback_inv_snd _
212+
213+
end BinaryProduct
214+
215+
/-!
216+
### Arbitrary products
217+
218+
In this section, we prove that `J`-indexed products in `Over X` correspond to `J`-indexed pullbacks
219+
in `C`.
220+
-/
26221

27222
namespace ConstructProducts
28223

@@ -164,46 +359,4 @@ theorem over_hasTerminal (B : C) : HasTerminal (Over B) where
164359
dsimp at this
165360
rwa [Category.comp_id, Category.comp_id] at this } }
166361

167-
section BinaryProduct
168-
169-
variable {X : C} {Y Z : Over X}
170-
171-
open Limits
172-
173-
lemma isPullback_of_binaryFan_isLimit (c : BinaryFan Y Z) (hc : IsLimit c) :
174-
IsPullback c.fst.left c.snd.left Y.hom Z.hom :=
175-
⟨by simp, ⟨((IsLimit.postcomposeHomEquiv (diagramIsoCospan _) _).symm
176-
((IsLimit.ofConeEquiv (ConstructProducts.conesEquiv X _).symm).symm hc)).ofIsoLimit
177-
(PullbackCone.isoMk _)⟩⟩
178-
179-
variable (Y Z) [HasPullback Y.hom Z.hom] [HasBinaryProduct Y Z]
180-
181-
/-- The product of `Y` and `Z` in `Over X` is isomorpic to `Y ×ₓ Z`. -/
182-
noncomputable
183-
def prodLeftIsoPullback :
184-
(Y ⨯ Z).left ≅ pullback Y.hom Z.hom :=
185-
(Over.isPullback_of_binaryFan_isLimit _ (prodIsProd Y Z)).isoPullback
186-
187-
@[reassoc (attr := simp)]
188-
lemma prodLeftIsoPullback_hom_fst :
189-
(prodLeftIsoPullback Y Z).hom ≫ pullback.fst _ _ = (prod.fst (X := Y)).left :=
190-
IsPullback.isoPullback_hom_fst _
191-
192-
@[reassoc (attr := simp)]
193-
lemma prodLeftIsoPullback_hom_snd :
194-
(prodLeftIsoPullback Y Z).hom ≫ pullback.snd _ _ = (prod.snd (X := Y)).left :=
195-
IsPullback.isoPullback_hom_snd _
196-
197-
@[reassoc (attr := simp)]
198-
lemma prodLeftIsoPullback_inv_fst :
199-
(prodLeftIsoPullback Y Z).inv ≫ (prod.fst (X := Y)).left = pullback.fst _ _ :=
200-
IsPullback.isoPullback_inv_fst _
201-
202-
@[reassoc (attr := simp)]
203-
lemma prodLeftIsoPullback_inv_snd :
204-
(prodLeftIsoPullback Y Z).inv ≫ (prod.snd (X := Y)).left = pullback.snd _ _ :=
205-
IsPullback.isoPullback_inv_snd _
206-
207-
end BinaryProduct
208-
209362
end CategoryTheory.Over

‎Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -202,6 +202,11 @@ def BinaryFan.ext {A B : C} {c c' : BinaryFan A B} (e : c.pt ≅ c'.pt)
202202
(h₁ : c.fst = e.hom ≫ c'.fst) (h₂ : c.snd = e.hom ≫ c'.snd) : c ≅ c' :=
203203
Cones.ext e (fun j => by rcases j with ⟨⟨⟩⟩ <;> assumption)
204204

205+
@[simp]
206+
lemma BinaryFan.ext_hom_hom {A B : C} {c c' : BinaryFan A B} (e : c.pt ≅ c'.pt)
207+
(h₁ : c.fst = e.hom ≫ c'.fst) (h₂ : c.snd = e.hom ≫ c'.snd) :
208+
(ext e h₁ h₂).hom.hom = e.hom := rfl
209+
205210
/-- A convenient way to show that a binary fan is a limit. -/
206211
def BinaryFan.IsLimit.mk {X Y : C} (s : BinaryFan X Y)
207212
(lift : ∀ {T : C} (_ : T ⟶ X) (_ : T ⟶ Y), T ⟶ s.pt)
@@ -237,6 +242,11 @@ def BinaryCofan.ext {A B : C} {c c' : BinaryCofan A B} (e : c.pt ≅ c'.pt)
237242
(h₁ : c.inl ≫ e.hom = c'.inl) (h₂ : c.inr ≫ e.hom = c'.inr) : c ≅ c' :=
238243
Cocones.ext e (fun j => by rcases j with ⟨⟨⟩⟩ <;> assumption)
239244

245+
@[simp]
246+
lemma BinaryCofan.ext_hom_hom {A B : C} {c c' : BinaryCofan A B} (e : c.pt ≅ c'.pt)
247+
(h₁ : c.inl ≫ e.hom = c'.inl) (h₂ : c.inr ≫ e.hom = c'.inr) :
248+
(ext e h₁ h₂).hom.hom = e.hom := rfl
249+
240250
@[simp]
241251
theorem BinaryCofan.ι_app_left {X Y : C} (s : BinaryCofan X Y) :
242252
s.ι.app ⟨WalkingPair.left⟩ = s.inl := rfl

0 commit comments

Comments
 (0)