Skip to content

chore: golf some proofs and generalize some universe variables #167

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Vtec234 merged 1 commit into from
Nov 10, 2025
Merged

chore: golf some proofs and generalize some universe variables #167

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
105 changes: 37 additions & 68 deletions HoTTLean/ForMathlib/CategoryTheory/Functor/IsPullback.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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]
Expand Down Expand Up @@ -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

Expand All @@ -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
Expand Down Expand Up @@ -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

Expand Down
12 changes: 6 additions & 6 deletions HoTTLean/Groupoids/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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

Expand Down
6 changes: 3 additions & 3 deletions HoTTLean/Groupoids/ClovenIsofibration.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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']
Expand All @@ -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]
Expand Down
20 changes: 10 additions & 10 deletions HoTTLean/Groupoids/IsPullback.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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
Expand Down