Skip to content

fix: clean up some sorries in PartialProd #32

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
Aug 24, 2025
Merged

fix: clean up some sorries in PartialProd #32

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
43 changes: 20 additions & 23 deletions Poly/ForMathlib/CategoryTheory/PartialProduct.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -167,50 +167,47 @@ theorem overPullbackToStar_prod_snd [HasBinaryProducts C]
simp only [forgetAdjStar.homEquiv_left_lift]
aesop

abbrev partialProd (c : LimitFan s X) : C :=
c.cone.pt
abbrev partialProd (c : LimitFan s X) : C := c.cone.pt

abbrev partialProd.cone (c : LimitFan s X) : Fan s X :=
c.cone
abbrev partialProd.cone (c : LimitFan s X) : Fan s X := c.cone

abbrev partialProd.isLimit (c : LimitFan s X) : IsLimit (partialProd.cone c) :=
c.isLimit
abbrev partialProd.isLimit (c : LimitFan s X) : IsLimit (cone c) := c.isLimit

abbrev partialProd.fst (c : LimitFan s X) : partialProd c ⟶ B :=
Fan.fst <| partialProd.cone c
abbrev partialProd.fst (c : LimitFan s X) : partialProd c ⟶ B := (cone c).fst

abbrev partialProd.snd (c : LimitFan s X) :
pullback (partialProd.fst c) s ⟶ X :=
Fan.snd <| partialProd.cone c
abbrev partialProd.snd (c : LimitFan s X) : pullback (fst c) s ⟶ X := (cone c).snd

/-- If the partial product of `s` and `X` exists, then every pair of morphisms `f : W ⟶ B` and
`g : pullback f s ⟶ X` induces a morphism `W ⟶ partialProd s X`. -/
abbrev partialProd.lift {W} (c : LimitFan s X)
(f : W ⟶ B) (g : pullback f s ⟶ X) : W ⟶ partialProd c :=
((partialProd.isLimit c)).lift (Fan.mk f g)
(isLimit c).lift (Fan.mk f g)

@[reassoc, simp]
theorem partialProd.lift_fst {W} {c : LimitFan s X} (f : W ⟶ B) (g : pullback f s ⟶ X) :
partialProd.lift c f g ≫ partialProd.fst c = f :=
((partialProd.isLimit c)).fac_left (Fan.mk f g)
lift c f g ≫ fst c = f :=
(isLimit c).fac_left (Fan.mk f g)

@[reassoc]
theorem partialProd.lift_snd {W} (c : LimitFan s X) (f : W ⟶ B) (g : pullback f s ⟶ X) :
(comparison (partialProd.lift c f g)) ≫ (partialProd.snd c) =
comparison (partialProd.lift c f g) ≫ snd c =
(pullback.congrHom (partialProd.lift_fst f g) rfl).hom ≫ g := by
let h := ((partialProd.isLimit c)).fac_right (Fan.mk f g)
conv_rhs => arg 2; exact ((isLimit c).fac_right (Fan.mk f g)).symm
rw [← pullbackMap_comparison]
simp [pullbackMap, pullback.map]
sorry
rw [← Category.assoc]; congr 1
ext <;> simp [pullbackMap]

-- theorem hom_lift (h : IsLimit t) {W : C} (m : W ⟶ t.pt) :
-- m = h.lift { pt := W, π := { app := fun b => m ≫ t.π.app b } } :=
-- h.uniq { pt := W, π := { app := fun b => m ≫ t.π.app b } } m fun _ => rfl

theorem partialProd.hom_ext {W : C} (c : LimitFan s X) {f g : W ⟶ partialProd c}
(h₁ : f ≫ partialProd.fst c = g ≫ partialProd.fst c)
(h₂ : comparison f ≫ partialProd.snd c =
(pullback.congrHom h₁ rfl).hom ≫ comparison g ≫ partialProd.snd c) :
(h₁ : f ≫ fst c = g ≫ fst c)
(h₂ : comparison f ≫ snd c = (pullback.congrHom h₁ rfl).hom ≫ comparison g ≫ snd c) :
f = g := by
sorry
-- apply c.isLimit.uniq
let f' : Fan s X := { pt := W, fst := f ≫ fst c, snd := comparison f ≫ snd c }
cases c.isLimit.uniq f' g (by simp [h₁, f']) <| by
refine .trans ?_ h₂.symm
rw [← Category.assoc]; congr 1
ext <;> simp [pullbackMap, comparison, f']
exact c.isLimit.uniq f' f rfl rfl
40 changes: 23 additions & 17 deletions Poly/UvPoly/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -274,11 +274,13 @@ def ε (P : UvPoly E B) (X : C) : pullback (P.fstProj X) P.p ⟶ E ⨯ X :=
((ev P.p).app ((star E).obj X)).left

/-- The partial product fan associated to a polynomial `P : UvPoly E B` and an object `X : C`. -/
@[simps]
@[simps -isSimp]
def fan (P : UvPoly E B) (X : C) : Fan P.p X where
pt := P @ X
fst := P.fstProj X
snd := (ε P X) ≫ prod.snd -- ((forgetAdjStar E).counit).app X
snd := ε P X ≫ prod.snd -- ((forgetAdjStar E).counit).app X

attribute [simp] fan_pt fan_fst

/--
`P.PartialProduct.fan` is in fact a limit fan; this provides the univeral mapping property of the
Expand All @@ -297,11 +299,15 @@ def isLimitFan (P : UvPoly E B) (X : C) : IsLimit (fan P X) where
intro c m h_left h_right
dsimp [pushforwardCurry]
symm
rw [← homMk_left m (U:= Over.mk c.fst) (V:= Over.mk (P.fstProj X))]
rw [← homMk_left m (U := Over.mk c.fst) (V := Over.mk (P.fstProj X))]
congr 1
apply (Adjunction.homEquiv_apply_eq (adj P.p) (overPullbackToStar c.fst c.snd) (Over.homMk m)).mpr
simp [overPullbackToStar, Fan.overPullbackToStar, Fan.over]
sorry
apply (Adjunction.homEquiv_apply_eq _ _ _).mpr
rw [← h_right]
simp [forgetAdjStar, comp_homEquiv, Comonad.adj]
simp [Equivalence.toAdjunction, homEquiv]
simp [coalgebraEquivOver, Equivalence.symm]; rfl

end PartialProduct

Expand All @@ -316,15 +322,18 @@ abbrev lift {Γ X : C} (P : UvPoly E B) (b : Γ ⟶ B) (e : pullback b P.p ⟶ X

@[simp]
theorem lift_fst {Γ X : C} {P : UvPoly E B} {b : Γ ⟶ B} {e : pullback b P.p ⟶ X} :
P.lift b e ≫ P.fstProj X = b := by
unfold lift
rw [← PartialProduct.fan_fst, partialProd.lift_fst]
P.lift b e ≫ P.fstProj X = b := partialProd.lift_fst ..

@[reassoc]
theorem lift_snd {Γ X : C} {P : UvPoly E B} {b : Γ ⟶ B} {e : pullback b P.p ⟶ X} :
(comparison (c:= PartialProduct.fan P X) (P.lift b e)) ≫ (ε P X) ≫ prod.snd =
(pullback.congrHom (partialProd.lift_fst b e) rfl).hom ≫ e := by
sorry
comparison (c := fan P X) (P.lift b e) ≫ (fan P X).snd =
(pullback.congrHom (partialProd.lift_fst b e) rfl).hom ≫ e := partialProd.lift_snd ..

theorem hom_ext {Γ X : C} {P : UvPoly E B} {f g : Γ ⟶ P @ X}
(h₁ : f ≫ P.fstProj X = g ≫ P.fstProj X)
(h₂ : comparison f ≫ (fan P X).snd =
(pullback.congrHom (by exact h₁) rfl).hom ≫ comparison g ≫ (fan P X).snd) :
f = g := partialProd.hom_ext ⟨fan P X, isLimitFan P X⟩ h₁ h₂

/-- A morphism `f : Γ ⟶ P @ X` projects to a morphism `b : Γ ⟶ B` and a morphism
`e : pullback b P.p ⟶ X`. -/
Expand All @@ -341,8 +350,7 @@ theorem proj_fst {Γ X : C} {P : UvPoly E B} {f : Γ ⟶ P @ X} :
-- formerly `polyPair_snd_eq_comp_u₂'`
@[simp]
theorem proj_snd {Γ X : C} {P : UvPoly E B} {f : Γ ⟶ P @ X} :
(proj P f).snd =
(pullback.map _ _ _ _ f (𝟙 E) (𝟙 B) (by aesop) (by aesop)) ≫ ε P X ≫ prod.snd := by
(proj P f).snd = pullback.map _ _ _ _ f (𝟙 E) (𝟙 B) (by simp) (by simp) ≫ (fan P X).snd := by
simp [proj]

/-- The domain of the composition of two polynomials. See `UvPoly.comp`. -/
Expand All @@ -351,11 +359,9 @@ def compDom {E B D A : C} (P : UvPoly E B) (Q : UvPoly D A) :=

@[simps!]
def comp [HasPullbacks C] [HasTerminal C]
{E B D A : C} (P : UvPoly E B) (Q : UvPoly D A) : UvPoly (compDom P Q) (P @ A) :=
{
p := (pullback.snd Q.p (fan P A).snd) ≫ (pullback.fst (fan P A).fst P.p)
exp := by sorry
}
{E B D A : C} (P : UvPoly E B) (Q : UvPoly D A) : UvPoly (compDom P Q) (P @ A) where
p := pullback.snd Q.p (fan P A).snd ≫ pullback.fst (fan P A).fst P.p
exp := sorry

/-- The associated functor of the composition of two polynomials is isomorphic to the composition of the associated functors. -/
def compFunctorIso [HasPullbacks C] [HasTerminal C]
Expand Down