From 626000b49f2b89be7e591662ba4d45b96227246f Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Sun, 24 Aug 2025 14:29:19 +0200 Subject: [PATCH] fix: clean up some sorries in PartialProd --- .../CategoryTheory/PartialProduct.lean | 43 +++++++++---------- Poly/UvPoly/Basic.lean | 40 +++++++++-------- 2 files changed, 43 insertions(+), 40 deletions(-) diff --git a/Poly/ForMathlib/CategoryTheory/PartialProduct.lean b/Poly/ForMathlib/CategoryTheory/PartialProduct.lean index 0a152d2..d7739eb 100644 --- a/Poly/ForMathlib/CategoryTheory/PartialProduct.lean +++ b/Poly/ForMathlib/CategoryTheory/PartialProduct.lean @@ -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 diff --git a/Poly/UvPoly/Basic.lean b/Poly/UvPoly/Basic.lean index 363f319..4e3f06e 100644 --- a/Poly/UvPoly/Basic.lean +++ b/Poly/UvPoly/Basic.lean @@ -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 @@ -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 @@ -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`. -/ @@ -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`. -/ @@ -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]