Skip to content

Commit 3ef0e8b

Browse files
mattrobballmattrobball
committed
golf (co)yoneda proofs
1 parent 16bd36d commit 3ef0e8b

1 file changed

Lines changed: 43 additions & 71 deletions

File tree

‎Mathlib/CategoryTheory/Limits/HasLimits.lean‎

Lines changed: 43 additions & 71 deletions
Original file line numberDiff line numberDiff line change
@@ -143,39 +143,39 @@ instance (priority := 100) hasLimitsOfShapeOfHasLimits {J : Type u₁} [Category
143143

144144
-- Interface to the `HasLimit` class.
145145
/-- An arbitrary choice of limit cone for a functor. -/
146-
def Limit.cone (F : J ⥤ C) [HasLimit F] : Cone F :=
146+
def limit.cone (F : J ⥤ C) [HasLimit F] : Cone F :=
147147
(getLimitCone F).cone
148-
#align category_theory.limits.limit.cone CategoryTheory.Limits.Limit.cone
148+
#align category_theory.limits.limit.cone CategoryTheory.Limits.limit.cone
149149

150150
/-- An arbitrary choice of limit object of a functor. -/
151151
def limit (F : J ⥤ C) [HasLimit F] :=
152-
(Limit.cone F).pt
152+
(limit.cone F).pt
153153
#align category_theory.limits.limit CategoryTheory.Limits.limit
154154

155155
/-- The projection from the limit object to a value of the functor. -/
156156
def limit.π (F : J ⥤ C) [HasLimit F] (j : J) : limit F ⟶ F.obj j :=
157-
(Limit.cone F).π.app j
157+
(limit.cone F).π.app j
158158
#align category_theory.limits.limit.π CategoryTheory.Limits.limit.π
159159

160160
@[simp]
161-
theorem limit.cone_x {F : J ⥤ C} [HasLimit F] : (Limit.cone F).pt = limit F :=
161+
theorem limit.cone_x {F : J ⥤ C} [HasLimit F] : (limit.cone F).pt = limit F :=
162162
rfl
163163
set_option linter.uppercaseLean3 false in
164164
#align category_theory.limits.limit.cone_X CategoryTheory.Limits.limit.cone_x
165165

166166
@[simp]
167-
theorem limit.cone_π {F : J ⥤ C} [HasLimit F] : (Limit.cone F).π.app = limit.π _ :=
167+
theorem limit.cone_π {F : J ⥤ C} [HasLimit F] : (limit.cone F).π.app = limit.π _ :=
168168
rfl
169169
#align category_theory.limits.limit.cone_π CategoryTheory.Limits.limit.cone_π
170170

171171
@[reassoc (attr := simp)]
172172
theorem limit.w (F : J ⥤ C) [HasLimit F] {j j' : J} (f : j ⟶ j') :
173173
limit.π F j ≫ F.map f = limit.π F j' :=
174-
(Limit.cone F).w f
174+
(limit.cone F).w f
175175
#align category_theory.limits.limit.w CategoryTheory.Limits.limit.w
176176

177177
/-- Evidence that the arbitrary choice of cone provied by `limit.cone F` is a limit cone. -/
178-
def limit.isLimit (F : J ⥤ C) [HasLimit F] : IsLimit (Limit.cone F) :=
178+
def limit.isLimit (F : J ⥤ C) [HasLimit F] : IsLimit (limit.cone F) :=
179179
(getLimitCone F).isLimit
180180
#align category_theory.limits.limit.is_limit CategoryTheory.Limits.limit.isLimit
181181

@@ -213,7 +213,7 @@ theorem limMap_π {F G : J ⥤ C} [HasLimit F] [HasLimit G] (α : F ⟶ G) (j :
213213
#align category_theory.limits.lim_map_π CategoryTheory.Limits.limMap_π
214214

215215
/-- The cone morphism from any cone to the arbitrary choice of limit cone. -/
216-
def limit.coneMorphism {F : J ⥤ C} [HasLimit F] (c : Cone F) : c ⟶ Limit.cone F :=
216+
def limit.coneMorphism {F : J ⥤ C} [HasLimit F] (c : Cone F) : c ⟶ limit.cone F :=
217217
(limit.isLimit F).liftConeMorphism c
218218
#align category_theory.limits.limit.cone_morphism CategoryTheory.Limits.limit.coneMorphism
219219

@@ -279,7 +279,7 @@ theorem limit.lift_map {F G : J ⥤ C} [HasLimit F] [HasLimit G] (c : Cone F) (
279279
#align category_theory.limits.limit.lift_map CategoryTheory.Limits.limit.lift_map
280280

281281
@[simp]
282-
theorem limit.lift_cone {F : J ⥤ C} [HasLimit F] : limit.lift F (Limit.cone F) = 𝟙 (limit F) :=
282+
theorem limit.lift_cone {F : J ⥤ C} [HasLimit F] : limit.lift F (limit.cone F) = 𝟙 (limit F) :=
283283
(limit.isLimit _).lift_self
284284
#align category_theory.limits.limit.lift_cone CategoryTheory.Limits.limit.lift_cone
285285

@@ -294,7 +294,7 @@ def limit.homIso (F : J ⥤ C) [HasLimit F] (W : C) :
294294

295295
@[simp]
296296
theorem limit.homIso_hom (F : J ⥤ C) [HasLimit F] {W : C} (f : ULift (W ⟶ limit F)) :
297-
(limit.homIso F W).hom f = (const J).map f.down ≫ (Limit.cone F).π :=
297+
(limit.homIso F W).hom f = (const J).map f.down ≫ (limit.cone F).π :=
298298
(limit.isLimit F).homIso_hom f
299299
#align category_theory.limits.limit.hom_iso_hom CategoryTheory.Limits.limit.homIso_hom
300300

@@ -316,7 +316,7 @@ theorem limit.lift_extend {F : J ⥤ C} [HasLimit F] (c : Cone F) {X : C} (f : X
316316
-/
317317
theorem hasLimitOfIso {F G : J ⥤ C} [HasLimit F] (α : F ≅ G) : HasLimit G :=
318318
HasLimit.mk
319-
{ cone := (Cones.postcompose α.hom).obj (Limit.cone F)
319+
{ cone := (Cones.postcompose α.hom).obj (limit.cone F)
320320
isLimit :=
321321
{ lift := fun s => limit.lift F ((Cones.postcompose α.inv).obj s)
322322
fac := fun s j =>
@@ -410,7 +410,7 @@ variable (F) [HasLimit F] (E : K ⥤ J) [HasLimit (E ⋙ F)]
410410
/-- The canonical morphism from the limit of `F` to the limit of `E ⋙ F`.
411411
-/
412412
def limit.pre : limit F ⟶ limit (E ⋙ F) :=
413-
limit.lift (E ⋙ F) ((Limit.cone F).whisker E)
413+
limit.lift (E ⋙ F) ((limit.cone F).whisker E)
414414
#align category_theory.limits.limit.pre CategoryTheory.Limits.limit.pre
415415

416416
@[reassoc (attr := simp)]
@@ -468,7 +468,7 @@ variable (F) [HasLimit F] (G : C ⥤ D) [HasLimit (F ⋙ G)]
468468
/-- The canonical morphism from `G` applied to the limit of `F` to the limit of `F ⋙ G`.
469469
-/
470470
def limit.post : G.obj (limit F) ⟶ limit (F ⋙ G) :=
471-
limit.lift (F ⋙ G) (mapCone G (Limit.cone F))
471+
limit.lift (F ⋙ G) (mapCone G (limit.cone F))
472472
#align category_theory.limits.limit.post CategoryTheory.Limits.limit.post
473473

474474
@[reassoc (attr := simp)]
@@ -511,7 +511,7 @@ open CategoryTheory.Equivalence
511511

512512
instance hasLimitEquivalenceComp (e : K ≌ J) [HasLimit F] : HasLimit (e.functor ⋙ F) :=
513513
HasLimit.mk
514-
{ cone := Cone.whisker e.functor (Limit.cone F)
514+
{ cone := Cone.whisker e.functor (limit.cone F)
515515
isLimit := IsLimit.whiskerEquivalence (limit.isLimit F) e }
516516
#align category_theory.limits.has_limit_equivalence_comp CategoryTheory.Limits.hasLimitEquivalenceComp
517517

@@ -535,7 +535,7 @@ variable [HasLimitsOfShape J C]
535535
section
536536

537537
/-- `limit F` is functorial in `F`, when `C` has all limits of shape `J`. -/
538-
@[simps obj]
538+
@[simps]
539539
def lim : (J ⥤ C) ⥤ C where
540540
obj F := limit F
541541
map α := limMap α
@@ -552,10 +552,10 @@ end
552552
variable {G : J ⥤ C} (α : F ⟶ G)
553553

554554
-- We generate this manually since `simps` gives it a weird name.
555-
@[simp]
556-
theorem limMap_eq_limMap : lim.map α = limMap α :=
557-
rfl
558-
#align category_theory.limits.lim_map_eq_lim_map CategoryTheory.Limits.limMap_eq_limMap
555+
-- @[simp]
556+
-- theorem limMap_eq_limMap : lim.map α = limMap α :=
557+
-- rfl
558+
-- #align category_theory.limits.lim_map_eq_lim_map CategoryTheory.Limits.limMap_eq_limMap
559559

560560
theorem limit.map_pre [HasLimitsOfShape K C] (E : K ⥤ J) :
561561
lim.map α ≫ limit.pre G E = limit.pre F E ≫ lim.map (whiskerLeft E α) := by
@@ -586,23 +586,9 @@ and cones over `F` with cone point `W`
586586
is natural in `F`.
587587
-/
588588
def limYoneda :
589-
lim ⋙ yoneda ⋙ (whiskeringRight _ _ _).obj uliftFunctor.{u₁} ≅ CategoryTheory.cones J C := by
590-
refine
591-
NatIso.ofComponents (fun F => NatIso.ofComponents (fun W => limit.homIso F (unop W)) ?_) ?_
592-
· intro X Y f
593-
dsimp [yoneda,uliftFunctor,cones]
594-
funext g
595-
dsimp [const,cones]
596-
apply NatTrans.ext
597-
aesop_cat
598-
· intro X Y f
599-
dsimp [yoneda,uliftFunctor]
600-
ext Z
601-
dsimp
602-
funext g
603-
dsimp [const,cones]
604-
apply NatTrans.ext
605-
aesop_cat
589+
lim ⋙ yoneda ⋙ (whiskeringRight _ _ _).obj uliftFunctor.{u₁} ≅ CategoryTheory.cones J C :=
590+
NatIso.ofComponents (fun F => NatIso.ofComponents (fun W => limit.homIso F (unop W))
591+
<| by intros ; funext ; aesop_cat) <| by intros ; ext ; funext ; aesop_cat
606592
#align category_theory.limits.lim_yoneda CategoryTheory.Limits.limYoneda
607593

608594
/-- The constant functor and limit functor are adjoint to each other-/
@@ -738,40 +724,40 @@ instance (priority := 100) hasColimitsOfShapeOfHasColimitsOfSize {J : Type u₁}
738724

739725
-- Interface to the `HasColimit` class.
740726
/-- An arbitrary choice of colimit cocone of a functor. -/
741-
def Colimit.cocone (F : J ⥤ C) [HasColimit F] : Cocone F :=
727+
def colimit.cocone (F : J ⥤ C) [HasColimit F] : Cocone F :=
742728
(getColimitCocone F).cocone
743-
#align category_theory.limits.colimit.cocone CategoryTheory.Limits.Colimit.cocone
729+
#align category_theory.limits.colimit.cocone CategoryTheory.Limits.colimit.cocone
744730

745731
/-- An arbitrary choice of colimit object of a functor. -/
746732
def colimit (F : J ⥤ C) [HasColimit F] :=
747-
(Colimit.cocone F).pt
733+
(colimit.cocone F).pt
748734
#align category_theory.limits.colimit CategoryTheory.Limits.colimit
749735

750736
/-- The coprojection from a value of the functor to the colimit object. -/
751737
def colimit.ι (F : J ⥤ C) [HasColimit F] (j : J) : F.obj j ⟶ colimit F :=
752-
(Colimit.cocone F).ι.app j
738+
(colimit.cocone F).ι.app j
753739
#align category_theory.limits.colimit.ι CategoryTheory.Limits.colimit.ι
754740

755741
@[simp]
756742
theorem colimit.cocone_ι {F : J ⥤ C} [HasColimit F] (j : J) :
757-
(Colimit.cocone F).ι.app j = colimit.ι _ j :=
743+
(colimit.cocone F).ι.app j = colimit.ι _ j :=
758744
rfl
759745
#align category_theory.limits.colimit.cocone_ι CategoryTheory.Limits.colimit.cocone_ι
760746

761747
@[simp]
762-
theorem colimit.cocone_x {F : J ⥤ C} [HasColimit F] : (Colimit.cocone F).pt = colimit F :=
748+
theorem colimit.cocone_x {F : J ⥤ C} [HasColimit F] : (colimit.cocone F).pt = colimit F :=
763749
rfl
764750
set_option linter.uppercaseLean3 false in
765751
#align category_theory.limits.colimit.cocone_X CategoryTheory.Limits.colimit.cocone_x
766752

767753
@[reassoc (attr := simp)]
768754
theorem colimit.w (F : J ⥤ C) [HasColimit F] {j j' : J} (f : j ⟶ j') :
769755
F.map f ≫ colimit.ι F j' = colimit.ι F j :=
770-
(Colimit.cocone F).w f
756+
(colimit.cocone F).w f
771757
#align category_theory.limits.colimit.w CategoryTheory.Limits.colimit.w
772758

773759
/-- Evidence that the arbitrary choice of cocone is a colimit cocone. -/
774-
def colimit.isColimit (F : J ⥤ C) [HasColimit F] : IsColimit (Colimit.cocone F) :=
760+
def colimit.isColimit (F : J ⥤ C) [HasColimit F] : IsColimit (colimit.cocone F) :=
775761
(getColimitCocone F).isColimit
776762
#align category_theory.limits.colimit.is_colimit CategoryTheory.Limits.colimit.isColimit
777763

@@ -818,7 +804,7 @@ theorem ι_colimMap {F G : J ⥤ C} [HasColimit F] [HasColimit G] (α : F ⟶ G)
818804
#align category_theory.limits.ι_colim_map CategoryTheory.Limits.ι_colimMap
819805

820806
/-- The cocone morphism from the arbitrary choice of colimit cocone to any cocone. -/
821-
def colimit.coconeMorphism {F : J ⥤ C} [HasColimit F] (c : Cocone F) : Colimit.cocone F ⟶ c :=
807+
def colimit.coconeMorphism {F : J ⥤ C} [HasColimit F] (c : Cocone F) : colimit.cocone F ⟶ c :=
822808
(colimit.isColimit F).descCoconeMorphism c
823809
#align category_theory.limits.colimit.cocone_morphism CategoryTheory.Limits.colimit.coconeMorphism
824810

@@ -881,7 +867,7 @@ theorem colimit.hom_ext {F : J ⥤ C} [HasColimit F] {X : C} {f f' : colimit F
881867

882868
@[simp]
883869
theorem colimit.desc_cocone {F : J ⥤ C} [HasColimit F] :
884-
colimit.desc F (Colimit.cocone F) = 𝟙 (colimit F) :=
870+
colimit.desc F (colimit.cocone F) = 𝟙 (colimit F) :=
885871
(colimit.isColimit _).desc_self
886872
#align category_theory.limits.colimit.desc_cocone CategoryTheory.Limits.colimit.desc_cocone
887873

@@ -896,7 +882,7 @@ def colimit.homIso (F : J ⥤ C) [HasColimit F] (W : C) :
896882

897883
@[simp]
898884
theorem colimit.homIso_hom (F : J ⥤ C) [HasColimit F] {W : C} (f : ULift (colimit F ⟶ W)) :
899-
(colimit.homIso F W).hom f = (Colimit.cocone F).ι ≫ (const J).map f.down :=
885+
(colimit.homIso F W).hom f = (colimit.cocone F).ι ≫ (const J).map f.down :=
900886
(colimit.isColimit F).homIso_hom f
901887
#align category_theory.limits.colimit.hom_iso_hom CategoryTheory.Limits.colimit.homIso_hom
902888

@@ -920,7 +906,7 @@ theorem colimit.desc_extend (F : J ⥤ C) [HasColimit F] (c : Cocone F) {X : C}
920906
-/
921907
theorem hasColimitOfIso {F G : J ⥤ C} [HasColimit F] (α : G ≅ F) : HasColimit G :=
922908
HasColimit.mk
923-
{ cocone := (Cocones.precompose α.hom).obj (Colimit.cocone F)
909+
{ cocone := (Cocones.precompose α.hom).obj (colimit.cocone F)
924910
isColimit :=
925911
{ desc := fun s => colimit.desc F ((Cocones.precompose α.inv).obj s)
926912
fac := fun s j =>
@@ -1008,7 +994,7 @@ variable (F) [HasColimit F] (E : K ⥤ J) [HasColimit (E ⋙ F)]
1008994
/-- The canonical morphism from the colimit of `E ⋙ F` to the colimit of `F`.
1009995
-/
1010996
def colimit.pre : colimit (E ⋙ F) ⟶ colimit F :=
1011-
colimit.desc (E ⋙ F) ((Colimit.cocone F).whisker E)
997+
colimit.desc (E ⋙ F) ((colimit.cocone F).whisker E)
1012998
#align category_theory.limits.colimit.pre CategoryTheory.Limits.colimit.pre
1013999

10141000
@[reassoc (attr := simp)]
@@ -1072,7 +1058,7 @@ variable (F) [HasColimit F] (G : C ⥤ D) [HasColimit (F ⋙ G)]
10721058
to `G` applied to the colimit of `F`.
10731059
-/
10741060
def colimit.post : colimit (F ⋙ G) ⟶ G.obj (colimit F) :=
1075-
colimit.desc (F ⋙ G) (mapCocone G (Colimit.cocone F))
1061+
colimit.desc (F ⋙ G) (mapCocone G (colimit.cocone F))
10761062
#align category_theory.limits.colimit.post CategoryTheory.Limits.colimit.post
10771063

10781064
@[reassoc (attr := simp)]
@@ -1121,7 +1107,7 @@ open CategoryTheory.Equivalence
11211107

11221108
instance hasColimit_equivalence_comp (e : K ≌ J) [HasColimit F] : HasColimit (e.functor ⋙ F) :=
11231109
HasColimit.mk
1124-
{ cocone := Cocone.whisker e.functor (Colimit.cocone F)
1110+
{ cocone := Cocone.whisker e.functor (colimit.cocone F)
11251111
isColimit := IsColimit.whiskerEquivalence (colimit.isColimit F) e }
11261112
#align category_theory.limits.has_colimit_equivalence_comp CategoryTheory.Limits.hasColimit_equivalence_comp
11271113

@@ -1141,7 +1127,7 @@ section
11411127
-- attribute [local simp] colimMap -- Porting note
11421128

11431129
/-- `colimit F` is functorial in `F`, when `C` has all colimits of shape `J`. -/
1144-
@[simps obj]
1130+
@[simps]
11451131
def colim : (J ⥤ C) ⥤ C where
11461132
obj F := colimit F
11471133
map α := colimMap α
@@ -1199,24 +1185,10 @@ morphisms from the cone point of the colimit cocone for `F` to `W`
11991185
and cocones over `F` with cone point `W`
12001186
is natural in `F`.
12011187
-/
1202-
def colimCoyoneda : colim.op ⋙ coyoneda ⋙ (whiskeringRight _ _ _).obj uliftFunctor.{u₁} ≅
1203-
CategoryTheory.cocones J C := by
1204-
refine
1205-
NatIso.ofComponents (fun F => NatIso.ofComponents (colimit.homIso (unop F)) ?_) ?_
1206-
· intro X Y f
1207-
dsimp [coyoneda,uliftFunctor,cocones]
1208-
funext g
1209-
dsimp [const,cocones]
1210-
apply NatTrans.ext
1211-
aesop_cat
1212-
· intro X Y f
1213-
dsimp [coyoneda,uliftFunctor]
1214-
ext Z
1215-
dsimp
1216-
funext g
1217-
dsimp [const,cocones]
1218-
apply NatTrans.ext
1219-
aesop_cat
1188+
def colimCoyoneda : colim.op ⋙ coyoneda ⋙ (whiskeringRight _ _ _).obj uliftFunctor.{u₁}
1189+
≅ CategoryTheory.cocones J C :=
1190+
NatIso.ofComponents (fun F => NatIso.ofComponents (fun W => colimit.homIso (unop F) (op W))
1191+
<| by intros ; funext ; aesop_cat) <| by intros ; ext ; funext ; aesop_cat
12201192
#align category_theory.limits.colim_coyoneda CategoryTheory.Limits.colimCoyoneda
12211193

12221194
/-- The colimit functor and constant functor are adjoint to each other

0 commit comments

Comments
 (0)