From d593ad42dc9973b74a99d76a90e3023a5365feb4 Mon Sep 17 00:00:00 2001 From: jlh18 Date: Sun, 9 Nov 2025 13:02:00 -0500 Subject: [PATCH] golfs --- .../CategoryTheory/Functor/IsPullback.lean | 105 ++++++------------ HoTTLean/Groupoids/Basic.lean | 12 +- HoTTLean/Groupoids/ClovenIsofibration.lean | 6 +- HoTTLean/Groupoids/IsPullback.lean | 20 ++-- 4 files changed, 56 insertions(+), 87 deletions(-) diff --git a/HoTTLean/ForMathlib/CategoryTheory/Functor/IsPullback.lean b/HoTTLean/ForMathlib/CategoryTheory/Functor/IsPullback.lean index d49b15e0..0dc8f53e 100644 --- a/HoTTLean/ForMathlib/CategoryTheory/Functor/IsPullback.lean +++ b/HoTTLean/ForMathlib/CategoryTheory/Functor/IsPullback.lean @@ -469,78 +469,47 @@ end def isoIsPullback {P P' X Y Z : Type*} [Category P] [Category P'] [Category X] [Category Y] [Category Z] - {fst : P ⥤ X} {snd : P ⥤ Y} {f : X ⥤ Z} {g : Y ⥤ Z} - {fst' : P' ⥤ X} {snd' : P' ⥤ Y} (h : Functor.IsPullback fst snd f g) - (h' : Functor.IsPullback fst' snd' f g) : - P ≅≅ P' where + {fst : P ⥤ X} {snd : P ⥤ Y} {f : X ⥤ Z} {g : Y ⥤ Z} + {fst' : P' ⥤ X} {snd' : P' ⥤ Y} (h : Functor.IsPullback fst snd f g) + (h' : Functor.IsPullback fst' snd' f g) : P ≅≅ P' where hom := h.toChosen ⋙ h'.fromChosen inv := h'.toChosen ⋙ h.fromChosen hom_inv_id := by - fapply Functor.ext - · intro A - have e : ((h.toChosen ⋙ h'.fromChosen) ⋙ h'.toChosen ⋙ h.fromChosen) = - (h.toChosen ⋙ (h'.fromChosen ⋙ h'.toChosen) ⋙ h.fromChosen) := by - simp [comp] - simp only[e,from_to_id,Functor.id_comp,to_from_id] - · intro A B t - have e : ((h.toChosen ⋙ h'.fromChosen) ⋙ h'.toChosen ⋙ h.fromChosen) = - (h.toChosen ⋙ (h'.fromChosen ⋙ h'.toChosen) ⋙ h.fromChosen) := by - simp[comp] - rw! [e] - simp only [← heq_eq_eq,heq_eqToHom_comp_iff,heq_comp_eqToHom_iff] - rw [from_to_id,Functor.id_comp,to_from_id] + conv => lhs; rw [Functor.assoc]; rhs; rw [← Functor.assoc]; rw [from_to_id] + simp [Functor.id_comp, to_from_id] inv_hom_id := by - fapply Functor.ext - · intro A - have e : ((h'.toChosen ⋙ h.fromChosen) ⋙ h.toChosen ⋙ h'.fromChosen) = - (h'.toChosen ⋙ (h.fromChosen ⋙ h.toChosen) ⋙ h'.fromChosen) := by - simp[comp] - simp only [e,from_to_id,Functor.id_comp,to_from_id] - · intro A B t - have e : ((h'.toChosen ⋙ h.fromChosen) ⋙ h.toChosen ⋙ h'.fromChosen) = - (h'.toChosen ⋙ (h.fromChosen ⋙ h.toChosen) ⋙ h'.fromChosen) := by - simp [comp] - rw! [e] - simp only[← heq_eq_eq,heq_eqToHom_comp_iff,heq_comp_eqToHom_iff] - rw [from_to_id,Functor.id_comp,to_from_id] + conv => lhs; rw [Functor.assoc]; rhs; rw [← Functor.assoc]; rw [from_to_id] + simp [Functor.id_comp, to_from_id] lemma isoIsPullback.inv_comp_left {P P' X Y Z : Type*} [Category P] [Category P'] [Category X] [Category Y] [Category Z] - {fst : P ⥤ X} {snd : P ⥤ Y} {f : X ⥤ Z} {g : Y ⥤ Z} - {fst' : P' ⥤ X} {snd' : P' ⥤ Y} (h : Functor.IsPullback fst snd f g) - (h' : Functor.IsPullback fst' snd' f g): + {fst : P ⥤ X} {snd : P ⥤ Y} {f : X ⥤ Z} {g : Y ⥤ Z} + {fst' : P' ⥤ X} {snd' : P' ⥤ Y} (h : Functor.IsPullback fst snd f g) + (h' : Functor.IsPullback fst' snd' f g) : (isoIsPullback h h').inv ⋙ fst = fst' := by - dsimp [isoIsPullback] - fapply Functor.ext - · intro A - simp only [Functor.assoc,h.from_north] - rw [toChosen_north] - · intros A B t - simp only [← heq_eq_eq,heq_eqToHom_comp_iff,heq_comp_eqToHom_iff] - rw! [Functor.assoc,h.from_north] - rw [toChosen_north] + simp [isoIsPullback, Functor.assoc, from_north, toChosen_north] -lemma isoIsPullback.hom_comp_left {P P' X Y Z : Type*} [Category P] [Category P'] +lemma isoIsPullback.inv_comp_right {P P' X Y Z : Type*} [Category P] [Category P'] [Category X] [Category Y] [Category Z] {fst : P ⥤ X} {snd : P ⥤ Y} {f : X ⥤ Z} {g : Y ⥤ Z} {fst' : P' ⥤ X} {snd' : P' ⥤ Y} (h : Functor.IsPullback fst snd f g) - (h' : Functor.IsPullback fst' snd' f g): + (h' : Functor.IsPullback fst' snd' f g) : + (isoIsPullback h h').inv ⋙ snd = snd' := by + simp [isoIsPullback, Functor.assoc, from_west, toChosen_west] + +lemma isoIsPullback.hom_comp_left {P P' X Y Z : Type*} [Category P] [Category P'] + [Category X] [Category Y] [Category Z] + {fst : P ⥤ X} {snd : P ⥤ Y} {f : X ⥤ Z} {g : Y ⥤ Z} + {fst' : P' ⥤ X} {snd' : P' ⥤ Y} (h : Functor.IsPullback fst snd f g) + (h' : Functor.IsPullback fst' snd' f g) : (isoIsPullback h h').hom ⋙ fst' = fst := by - dsimp [isoIsPullback] - fapply Functor.ext - · intro A - simp only [Functor.assoc,h'.from_north] - rw [toChosen_north] - · intros A B t - simp only [← heq_eq_eq,heq_eqToHom_comp_iff,heq_comp_eqToHom_iff] - rw! [Functor.assoc,h'.from_north] - rw [toChosen_north] + simp [isoIsPullback, Functor.assoc, from_north, toChosen_north] lemma isoIsPullback.hom_comp_left' {P P' X Y Z : Type*} [Category P] [Category P'] [Category X] [Category Y] [Category Z] {fst : P ⥤ X} {snd : P ⥤ Y} {f : X ⥤ Z} {g : Y ⥤ Z} {fst' : P' ⥤ X} {snd' : P' ⥤ Y} (h : Functor.IsPullback fst snd f g) - (h' : Functor.IsPullback fst' snd' f g) {hom } (e: hom = (isoIsPullback h h').hom): + (h' : Functor.IsPullback fst' snd' f g) {hom} (e: hom = (isoIsPullback h h').hom) : hom ⋙ fst' = fst := by rw [e] apply isoIsPullback.hom_comp_left @@ -549,18 +518,18 @@ lemma isoIsPullback.hom_comp_right {P P' X Y Z : Type*} [Category P] [Category P [Category X] [Category Y] [Category Z] {fst : P ⥤ X} {snd : P ⥤ Y} {f : X ⥤ Z} {g : Y ⥤ Z} {fst' : P' ⥤ X} {snd' : P' ⥤ Y} (h : Functor.IsPullback fst snd f g) - (h' : Functor.IsPullback fst' snd' f g) {hom } (e: hom = (isoIsPullback h h').hom): + (h' : Functor.IsPullback fst' snd' f g) : + (isoIsPullback h h').hom ⋙ snd' = snd := by + simp [isoIsPullback, Functor.assoc, from_west, toChosen_west] + +lemma isoIsPullback.hom_comp_right' {P P' X Y Z : Type*} [Category P] [Category P'] + [Category X] [Category Y] [Category Z] + {fst : P ⥤ X} {snd : P ⥤ Y} {f : X ⥤ Z} {g : Y ⥤ Z} + {fst' : P' ⥤ X} {snd' : P' ⥤ Y} (h : Functor.IsPullback fst snd f g) + (h' : Functor.IsPullback fst' snd' f g) {hom} (e: hom = (isoIsPullback h h').hom) : hom ⋙ snd' = snd := by rw[e] - unfold isoIsPullback - fapply Functor.ext - · intro A - simp only [Functor.assoc,h'.from_west] - rw[toChosen_west] - · intros A B t - simp only [← heq_eq_eq,heq_eqToHom_comp_iff,heq_comp_eqToHom_iff] - rw! [Functor.assoc,h'.from_west] - rw [toChosen_west] + apply isoIsPullback.hom_comp_right def ofBotId {A A' B : Type*} [Category A] [Category A'] [Category B] @@ -607,7 +576,7 @@ theorem outer_comm_sq : no ⋙ rth ⋙ east = west ⋙ so ⋙ uth := by section horiz -variable (esah_pb : IsPullback rth sah east uth) (wsah_pb : IsPullback no west sah so) +variable (wsah_pb : IsPullback no west sah so) (esah_pb : IsPullback rth sah east uth) namespace horiz @@ -622,7 +591,7 @@ def universal : (lift : C ⥤ Algeria) ×' lift ⋙ west = Cw ∧ ∀ {l0 l1 : C ⥤ Algeria}, l0 ⋙ no ⋙ rth = l1 ⋙ no ⋙ rth → l0 ⋙ west = l1 ⋙ west → l0 = l1 := - ⟨ lift esah_pb wsah_pb Cn Cw hC, + ⟨ lift wsah_pb esah_pb Cn Cw hC, by rw [lift, ← Functor.assoc, wsah_pb.fac_left, esah_pb.fac_left], wsah_pb.fac_right _ _ _, by @@ -653,8 +622,8 @@ are both pullbacks. def horiz : IsPullback (no ⋙ rth) west east (so ⋙ uth) := IsPullback.ofUniversal (no ⋙ rth) west east (so ⋙ uth) (outer_comm_sq wsah esah) - (fun _ _ hC => horiz.universal wsah esah_pb wsah_pb _ _ hC) - (fun _ _ hC => horiz.universal wsah esah_pb wsah_pb _ _ hC) + (fun _ _ hC => horiz.universal wsah wsah_pb esah_pb _ _ hC) + (fun _ _ hC => horiz.universal wsah wsah_pb esah_pb _ _ hC) end horiz diff --git a/HoTTLean/Groupoids/Basic.lean b/HoTTLean/Groupoids/Basic.lean index 9c3ca063..6c14e87f 100644 --- a/HoTTLean/Groupoids/Basic.lean +++ b/HoTTLean/Groupoids/Basic.lean @@ -19,17 +19,17 @@ open CategoryTheory ULift Functor Groupoidal namespace CategoryTheory.PGrpd def pGrpdToGroupoidalAsSmallFunctor : PGrpd.{v, v} ⥤ - ∫(Grpd.asSmallFunctor.{max w (v+1), v, v}) := + ∫(Grpd.asSmallFunctor.{w, v, v}) := Grothendieck.functorTo PGrpd.forgetToGrpd - (fun x => AsSmall.up.obj.{v, v, max w (v + 1)} x.fiber) + (fun x => AsSmall.up.obj.{v, v, w} x.fiber) (fun f => AsSmall.up.map f.fiber) (by aesop_cat) (by aesop_cat) def groupoidalAsSmallFunctorToPGrpd : - ∫(Grpd.asSmallFunctor.{max w (v+1), v, v}) ⥤ PGrpd.{v,v} := + ∫(Grpd.asSmallFunctor.{w, v, v}) ⥤ PGrpd.{v,v} := PGrpd.functorTo Groupoidal.forget - (fun x => AsSmall.down.obj.{v, v, max w (v + 1)} x.fiber) + (fun x => AsSmall.down.obj.{v, v, w} x.fiber) (fun f => AsSmall.down.map f.fiber) (by aesop_cat) (by aesop_cat) @@ -46,9 +46,9 @@ def groupoidalAsSmallFunctorToPGrpd : ⋙ Groupoidal.forget = PGrpd.forgetToGrpd := rfl -def asSmallFunctor : PGrpd.{v, v} ⥤ PGrpd.{max w (v+1), max w (v+1)} := +def asSmallFunctor : PGrpd.{v, v} ⥤ PGrpd.{max w v, max w v} := pGrpdToGroupoidalAsSmallFunctor ⋙ - toPGrpd Grpd.asSmallFunctor.{max w (v+1), v, v} + toPGrpd Grpd.asSmallFunctor.{w, v, v} end CategoryTheory.PGrpd diff --git a/HoTTLean/Groupoids/ClovenIsofibration.lean b/HoTTLean/Groupoids/ClovenIsofibration.lean index 99fa2019..e78e16d8 100644 --- a/HoTTLean/Groupoids/ClovenIsofibration.lean +++ b/HoTTLean/Groupoids/ClovenIsofibration.lean @@ -621,12 +621,12 @@ def ofIsPullback {A B A' B' : Type u} [Groupoid.{v} A] [Groupoid.{v} B] [Groupoi have q1 : Functor.IsPullback (Groupoidal.pre IF.classifier bot ⋙ i.hom) (Groupoidal.forget (F := (bot ⋙ IF.classifier))) F bot := Functor.IsPullback.Paste.horiz eq1 (by simp [i_comp_F]) - (Functor.IsPullback.ofBotId i_comp_F.symm) (Groupoidal.pre_isPullback ..) + (Functor.IsPullback.ofBotId i_comp_F.symm) let j : A' ≅≅ Functor.Groupoidal (F := bot ⋙ IF.classifier) := Functor.IsPullback.isoIsPullback isPullback q1 have e : F' = j.hom ⋙ (Groupoidal.forget (F := bot ⋙ IF.classifier)) := - (IsPullback.isoIsPullback.hom_comp_right isPullback q1 (hom := j.hom) (by simp[j])).symm + (IsPullback.isoIsPullback.hom_comp_right' isPullback q1 (hom := j.hom) (by simp[j])).symm isoComp (Functor.ClovenIsofibration.forget ..) j _ e instance {A B A' B' : Type u} [Groupoid.{v} A] [Groupoid.{v} B] [Groupoid.{v} A'] @@ -650,7 +650,7 @@ def tpClovenIsofibration : (GroupoidModel.U.{u}.tp).ClovenIsofibration := Functor.IsPullback.isoIsPullback IsPullback.isPullbackCoreAsSmall' (Functor.Groupoidal.isPullback (Core.inclusion _ ⋙ AsSmall.down)) isoComp (Functor.ClovenIsofibration.forget _) i - _ (Functor.IsPullback.isoIsPullback.hom_comp_right _ _ rfl).symm + _ (Functor.IsPullback.isoIsPullback.hom_comp_right ..).symm instance : IsSplit tpClovenIsofibration := by dsimp [tpClovenIsofibration] diff --git a/HoTTLean/Groupoids/IsPullback.lean b/HoTTLean/Groupoids/IsPullback.lean index 171cf8a8..c6b7383b 100644 --- a/HoTTLean/Groupoids/IsPullback.lean +++ b/HoTTLean/Groupoids/IsPullback.lean @@ -37,24 +37,24 @@ theorem liftTm'_tp' : Cat.homOf liftTm'.{v,u} ≫ Cat.homOf tp'.{v+1, max u (v+2 /-- The following square is a meta-theoretic pullback -PGrpd.{v} ------- asSmallFunctor ------> PGrpd.{v+1} +PGrpd.{v} ------- asSmallFunctor ------> PGrpd.{max w (v+1)} | | | | forgetToGrpd forgetToGrpd | | | | v v -Grpd.{v} ------- asSmallFunctor -----> Grpd.{v+1} +Grpd.{v} ------- asSmallFunctor -----> Grpd.{max w (v+1)} -/ def isPullback_forgetToGrpd_forgetToGrpd : - Functor.IsPullback - PGrpd.asSmallFunctor.{v+1} + Functor.IsPullback + PGrpd.asSmallFunctor.{max w v} PGrpd.forgetToGrpd.{v} - PGrpd.forgetToGrpd.{v+1} - Grpd.asSmallFunctor.{v+1} := - Functor.IsPullback.ofIso (toPGrpd _) forget PGrpd.forgetToGrpd.{v+1} - Grpd.asSmallFunctor.{v+1} (isPullback _) + PGrpd.forgetToGrpd.{max w v} + Grpd.asSmallFunctor.{max w v} := + Functor.IsPullback.ofIso (toPGrpd _) forget PGrpd.forgetToGrpd.{max w v} + Grpd.asSmallFunctor.{max w v} (isPullback _) PGrpd.pGrpdToGroupoidalAsSmallFunctor PGrpd.groupoidalAsSmallFunctorToPGrpd PGrpd.groupoidalAsSmallFunctorToPGrpd_pGrpdToGroupoidalAsSmallFunctor @@ -82,7 +82,7 @@ def isPullback_liftTm' : Functor.IsPullback tp'.{v+1,max u (v+2)} liftTy'.{v,max u (v+2)} := Functor.IsPullback.ofIso' PGrpd.asSmallFunctor.{v+1} PGrpd.forgetToGrpd.{v} - PGrpd.forgetToGrpd.{v+1} Grpd.asSmallFunctor.{v+1} isPullback_forgetToGrpd_forgetToGrpd + PGrpd.forgetToGrpd.{v+1} Grpd.asSmallFunctor.{v+1} isPullback_forgetToGrpd_forgetToGrpd.{v+1} liftTm'.{v,max u (v+2)} tp'.{_,max u (v+2)} tp'.{v+1,max u (v+2)} liftTy'.{v,max u (v+2)} AsSmall.downIso AsSmall.downIso AsSmall.downIso AsSmall.downIso rfl rfl rfl rfl @@ -178,7 +178,7 @@ def isPullbackCoreAsSmall' : Functor.IsPullback (Core.inclusion _ ⋙ AsSmall.down) (Ctx.coreAsSmallFunctor PGrpd.forgetToGrpd) (PGrpd.forgetToGrpd) (Core.inclusion _ ⋙ AsSmall.down) := - Functor.IsPullback.Paste.horiz rfl rfl isPullbackAsSmall isPullbackCoreAsSmall + Functor.IsPullback.Paste.horiz rfl rfl isPullbackCoreAsSmall isPullbackAsSmall /-- ∫ toCo...iv A ----> coreAsSmall PGrpd