From ce229b4c207baa603eb128a7887e4ff4a54b7838 Mon Sep 17 00:00:00 2001 From: openhands Date: Sat, 10 Oct 2026 21:03:50 -0400 Subject: [PATCH 01/11] feat: bump Poly to Lean 4.34.1 --- .gitignore | 1 + Poly/Bifunctor/Basic.lean | 19 +- Poly/Bifunctor/Sigma.lean | 96 ++++++--- .../CategoryTheory/Comma/Over/Pullback.lean | 114 +++++++--- .../CategoryTheory/Comma/Over/Sections.lean | 87 ++++++-- Poly/ForMathlib/CategoryTheory/Elements.lean | 20 +- .../Shapes/Pullback/IsPullback/Basic.lean | 8 +- .../LocallyCartesianClosed/Basic.lean | 9 +- .../LocallyCartesianClosed/BeckChevalley.lean | 22 +- .../Distributivity.lean | 20 +- Poly/ForMathlib/CategoryTheory/NatTrans.lean | 2 +- .../CategoryTheory/PartialProduct.lean | 21 +- Poly/ForMathlib/CategoryTheory/Types.lean | 8 +- Poly/MvPoly/Basic.lean | 2 +- Poly/Type/Univariate.lean | 12 +- Poly/UvPoly/Basic.lean | 41 ++-- Poly/UvPoly/UPFan.lean | 2 +- Poly/UvPoly/UPIso.lean | 13 +- Poly/Widget/CommDiag.lean | 11 +- README.md | 2 +- lake-manifest.json | 36 ++-- lakefile.lean | 6 +- lean-toolchain | 2 +- vendor/checkdecls/.gitignore | 4 + vendor/checkdecls/LICENSE | 201 ++++++++++++++++++ vendor/checkdecls/Main.lean | 26 +++ vendor/checkdecls/UPSTREAM.md | 27 +++ vendor/checkdecls/lake-manifest.json | 6 + vendor/checkdecls/lakefile.lean | 13 ++ vendor/checkdecls/lean-toolchain | 1 + 30 files changed, 637 insertions(+), 195 deletions(-) create mode 100644 vendor/checkdecls/.gitignore create mode 100644 vendor/checkdecls/LICENSE create mode 100644 vendor/checkdecls/Main.lean create mode 100644 vendor/checkdecls/UPSTREAM.md create mode 100644 vendor/checkdecls/lake-manifest.json create mode 100644 vendor/checkdecls/lakefile.lean create mode 100644 vendor/checkdecls/lean-toolchain diff --git a/.gitignore b/.gitignore index fa55280..79529d2 100644 --- a/.gitignore +++ b/.gitignore @@ -40,6 +40,7 @@ docs/_includes/sorries.md *.synctex.gz(busy) *.pdfsync *.json +!vendor/checkdecls/lake-manifest.json *.auctex-auto build/ diff --git a/Poly/Bifunctor/Basic.lean b/Poly/Bifunctor/Basic.lean index 17503a9..976ad57 100644 --- a/Poly/Bifunctor/Basic.lean +++ b/Poly/Bifunctor/Basic.lean @@ -39,8 +39,11 @@ theorem comp₂_comp {𝒞' : Type*} [Category 𝒞'] def comp₂_iso {F₁ F₂ : 𝒟' ⥤ 𝒟} {P₁ P₂ : 𝒞 ⥤ 𝒟 ⥤ ℰ} (i : F₁ ≅ F₂) (j : P₁ ≅ P₂) : F₁ ⋙₂ P₁ ≅ F₂ ⋙₂ P₂ := NatIso.ofComponents₂ (fun C D => (j.app C).app (F₁.obj D) ≪≫ (P₂.obj C).mapIso (i.app D)) - (fun _ _ => by simp [NatTrans.naturality_app_assoc]) + (fun _ _ => by + dsimp [comp₂] + simp [NatTrans.naturality_app_assoc]) (fun C f => by + dsimp [comp₂] have := congr_arg (P₂.obj C).map (i.hom.naturality f) simp only [map_comp] at this simp [this]) @@ -70,12 +73,12 @@ theorem comp₂_naturality₂_left (F : 𝒟 ⥤ 𝒞) (P : 𝒞ᵒᵖ ⥤ 𝒟 (i : F ⋙₂ coyoneda (C := 𝒞) ⟶ P) (X Y : 𝒞) (Z : 𝒟) (f : X ⟶ Y) (g : Y ⟶ F.obj Z) : -- The `op`s really are a pain. Why can't they be definitional like in Lean 3 :( (i.app <| .op X).app Z (f ≫ g) = (P.map f.op).app Z ((i.app <| .op Y).app Z g) := by - simp [← FunctorToTypes.naturality₂_left] + exact FunctorToTypes.naturality₂_left _ _ i f.op g theorem comp₂_naturality₂_right (F : 𝒟 ⥤ 𝒞) (P : 𝒞ᵒᵖ ⥤ 𝒟 ⥤ Type v) (i : F ⋙₂ coyoneda (C := 𝒞) ⟶ P) (X : 𝒞) (Y Z : 𝒟) (f : X ⟶ F.obj Y) (g : Y ⟶ Z) : (i.app <| .op X).app Z (f ≫ F.map g) = (P.obj <| .op X).map g ((i.app <| .op X).app Y f) := by - simp [← FunctorToTypes.naturality₂_right] + exact FunctorToTypes.naturality₂_right _ _ i g f end coyoneda @@ -87,8 +90,14 @@ variable {𝒟 : Type*} [Category 𝒟] def coyoneda_iso {F : 𝒞 ⥤ 𝒟} {G : 𝒟 ⥤ 𝒞} (A : F ⊣ G) : F.op ⋙ coyoneda (C := 𝒟) ≅ G ⋙₂ coyoneda (C := 𝒞) := NatIso.ofComponents₂ (fun C D => Equiv.toIso <| A.homEquiv C.unop D) - (fun _ _ => by ext : 1; simp [A.homEquiv_naturality_left]) - (fun _ _ => by ext : 1; simp [A.homEquiv_naturality_right]) + (fun _ f => by + apply ConcreteCategory.hom_ext + intro g + exact A.homEquiv_naturality_left f.unop g) + (fun _ f => by + apply ConcreteCategory.hom_ext + intro g + exact A.homEquiv_naturality_right g f) end Adjunction end CategoryTheory diff --git a/Poly/Bifunctor/Sigma.lean b/Poly/Bifunctor/Sigma.lean index d453d2d..70e372f 100644 --- a/Poly/Bifunctor/Sigma.lean +++ b/Poly/Bifunctor/Sigma.lean @@ -45,20 +45,22 @@ a functor `F'` s.t. `F'.Elements ≅ F.Elements × 𝒟`; very awkward. - known concrete instances are `𝒟 ∈ {Type, Cat, Grpd}` -/ def Sigma {F : 𝒞 ⥤ Type w} (G : F.Elements ⥤ 𝒟 ⥤ Type v) : 𝒞 ⥤ 𝒟 ⥤ Type (max w v) := by refine curry.obj { - obj := fun (C, D) => (a : F.obj C) × (G.obj ⟨C, a⟩).obj D - map := fun (f, g) ⟨a, b⟩ => - ⟨F.map f a, (G.map ⟨f, rfl⟩).app _ ((G.obj ⟨_, a⟩).map g b)⟩ + obj := fun (C, D) => (a : F.obj C) × (G.obj (F.elementsMk C a)).obj D + map := fun fg => TypeCat.ofHom fun ⟨a, b⟩ => + ⟨F.map fg.1 a, (G.map ⟨fg.1, rfl⟩).app _ ((G.obj (F.elementsMk _ a)).map fg.2 b)⟩ map_id := ?_ map_comp := ?_ } <;> { intros - ext ⟨a, b⟩ : 1 - dsimp + apply ConcreteCategory.hom_ext + rintro ⟨a, b⟩ + dsimp +instances congr! 1 with h . simp - . rw! [h]; simp [FunctorToTypes.naturality] + . rw! [h]; simp [NatTrans.naturality_apply] } +set_option backward.isDefEq.respectTransparency.types false in def Sigma.isoCongrLeft {F₁ F₂ : 𝒞 ⥤ Type w} /- Q: What kind of map `F₂.Elements ⥤ F₁.Elements` could `NatTrans.mapElements i.hom` generalize to? @@ -69,38 +71,42 @@ def Sigma.isoCongrLeft {F₁ F₂ : 𝒞 ⥤ Type w} refine NatIso.ofComponents₂ (fun C D => Equiv.toIso { toFun := fun ⟨a, b⟩ => ⟨i.hom.app C a, b⟩ - invFun := fun ⟨a, b⟩ => ⟨i.inv.app C a, cast (by simp) b⟩ - left_inv := fun ⟨_, _⟩ => by simp - right_inv := fun ⟨_, _⟩ => by simp + invFun := fun ⟨a, b⟩ => ⟨i.inv.app C a, cast (by simp [NatTrans.mapElements]) b⟩ + left_inv := fun ⟨_, _⟩ => by simp [Sigma, NatTrans.mapElements] + right_inv := fun ⟨_, _⟩ => by simp [Sigma] }) ?_ ?_ <;> { intros - ext : 1 - dsimp + apply ConcreteCategory.hom_ext + rintro ⟨a, b⟩ + dsimp +instances [Sigma, Equiv.toIso] apply have h := ?_; Sigma.ext h ?_ - . simp [FunctorToTypes.naturality] - . dsimp [Sigma] at h ⊢ + . simp [NatTrans.naturality_apply] + . dsimp +instances [Sigma] at h ⊢ rw! [← h] simp [NatTrans.mapElements] } +set_option backward.isDefEq.respectTransparency.types false in def Sigma.isoCongrRight {F : 𝒞 ⥤ Type w} {G₁ G₂ : F.Elements ⥤ 𝒟 ⥤ Type v} (i : G₁ ≅ G₂) : Sigma G₁ ≅ Sigma G₂ := by refine NatIso.ofComponents₂ (fun C D => Equiv.toIso { - toFun := fun ⟨a, b⟩ => ⟨a, (i.hom.app ⟨C, a⟩).app D b⟩ - invFun := fun ⟨a, b⟩ => ⟨a, (i.inv.app ⟨C, a⟩).app D b⟩ - left_inv := fun ⟨_, _⟩ => by simp - right_inv := fun ⟨_, _⟩ => by simp + toFun := fun ⟨a, b⟩ => ⟨a, (i.hom.app (F.elementsMk C a)).app D b⟩ + invFun := fun ⟨a, b⟩ => ⟨a, (i.inv.app (F.elementsMk C a)).app D b⟩ + left_inv := fun ⟨_, _⟩ => by simp [Sigma] + right_inv := fun ⟨_, _⟩ => by simp [Sigma] }) ?_ ?_ <;> { intros - ext : 1 - dsimp + apply ConcreteCategory.hom_ext + rintro ⟨a, b⟩ + dsimp +instances [Sigma, Equiv.toIso] apply have h := ?_; Sigma.ext h ?_ . simp - . dsimp [Sigma] at h ⊢ - simp [FunctorToTypes.naturality₂_left, FunctorToTypes.naturality₂_right] + . dsimp +instances [Sigma] at h ⊢ + simp [FunctorToTypes.naturality₂_left] } +set_option backward.isDefEq.respectTransparency false in theorem comp₂_Sigma {𝒟' : Type*} [Category 𝒟'] {F : 𝒞 ⥤ Type w} (G : 𝒟' ⥤ 𝒟) (P : F.Elements ⥤ 𝒟 ⥤ Type v) : G ⋙₂ Sigma P = Sigma (G ⋙₂ P) := by @@ -110,12 +116,15 @@ theorem comp₂_Sigma {𝒟' : Type*} [Category 𝒟'] . intro; simp . intros apply heq_of_eq - ext : 1 - apply Sigma.ext <;> simp + apply ConcreteCategory.hom_ext + intro x + apply Sigma.ext <;> simp [comp₂, Sigma] . intros apply heq_of_eq - ext : 3 - apply Sigma.ext <;> simp + ext D : 2 + apply ConcreteCategory.hom_ext + intro x + apply Sigma.ext <;> simp [comp₂, Sigma] end CategoryTheory.Functor @@ -133,41 +142,60 @@ def equiv_Sigma {A : 𝒞} (X : 𝒞) (U : Over A) : (X ⟶ U.left) ≃ (b : X invFun p := p.snd.left left_inv _ := by simp right_inv := fun _ => by - dsimp; congr! 1 with h + dsimp +instances; congr! 1 with h . simp . rw! [h]; simp @[simps] def equivalence_Elements (A : 𝒞) : (yoneda.obj A).Elements ≌ (Over A)ᵒᵖ where functor := { - obj := fun x => .op <| Over.mk x.snd - map := fun f => .op <| Over.homMk f.val.unop (by simpa using f.property) + obj := fun x => .op <| Over.mk x.val + map := fun f => .op <| Over.homMk f.hom.unop (by simpa using f.map_val) } inverse := { - obj := fun U => ⟨.op U.unop.left, U.unop.hom⟩ + obj := fun U => (yoneda.obj A).elementsMk (.op U.unop.left) U.unop.hom map := fun f => ⟨.op f.unop.left, by simp⟩ } - unitIso := NatIso.ofComponents Iso.refl (by simp) + unitIso := NatIso.ofComponents Iso.refl (by intro X Y f; simp; rfl) counitIso := NatIso.ofComponents Iso.refl -- TODO: `simp` fails to unify `id_comp`/`comp_id` (fun f => by simp [Category.comp_id f, Category.id_comp f]) +set_option backward.isDefEq.respectTransparency.types false in /-- For `X ∈ 𝒞` and `f ∈ 𝒞/A`, `𝒞(X, Over.forget f) ≅ Σ(g: X ⟶ A), 𝒞/A(g, f)`. -/ def forget_iso_Sigma (A : 𝒞) : Over.forget A ⋙₂ coyoneda (C := 𝒞) ≅ Functor.Sigma ((equivalence_Elements A).functor ⋙ coyoneda (C := Over A)) := by refine NatIso.ofComponents₂ (fun X U => Equiv.toIso <| equiv_Sigma X.unop U) ?_ ?_ . intros X Y U f - ext : 1 - dsimp + apply ConcreteCategory.hom_ext + intro g + change X.unop ⟶ U.left at g + dsimp +instances [Functor.comp₂, Functor.Sigma] + simp only [Equiv.toIso_hom_hom_apply] + change (⟨(f.unop ≫ g) ≫ U.hom, Over.homMk (f.unop ≫ g) rfl⟩ : + (b : Y.unop ⟶ A) × (Over.mk b ⟶ U)) = + ⟨f.unop ≫ (g ≫ U.hom), + (Over.homMk f.unop rfl : + Over.mk (f.unop ≫ (g ≫ U.hom)) ⟶ Over.mk (g ≫ U.hom)) ≫ + Over.homMk g rfl ≫ 𝟙 U⟩ apply have h := ?_; Sigma.ext h ?_ . simp . dsimp at h ⊢ rw! [h] simp . intros X Y U f - ext : 1 - dsimp + apply ConcreteCategory.hom_ext + intro g + change U.unop ⟶ X.left at g + dsimp +instances [Functor.comp₂, Functor.Sigma] + simp only [Equiv.toIso_hom_hom_apply] + change (⟨(g ≫ f.left) ≫ Y.hom, Over.homMk (g ≫ f.left) rfl⟩ : + (b : U.unop ⟶ A) × (Over.mk b ⟶ Y)) = + ⟨𝟙 U.unop ≫ (g ≫ X.hom), + (Over.homMk (𝟙 U.unop) rfl : + Over.mk (𝟙 U.unop ≫ (g ≫ X.hom)) ⟶ Over.mk (g ≫ X.hom)) ≫ + Over.homMk g rfl ≫ f⟩ apply have h := ?_; Sigma.ext h ?_ . simp . dsimp at h ⊢ diff --git a/Poly/ForMathlib/CategoryTheory/Comma/Over/Pullback.lean b/Poly/ForMathlib/CategoryTheory/Comma/Over/Pullback.lean index d5569d6..8ec5e03 100644 --- a/Poly/ForMathlib/CategoryTheory/Comma/Over/Pullback.lean +++ b/Poly/ForMathlib/CategoryTheory/Comma/Over/Pullback.lean @@ -32,9 +32,13 @@ theorem isCartesian_mapPullbackAdj_counit [HasPullbacks C] {X Y : C} (f : X ⟶ (h₁₂ := Over.homMk (V := Over.mk f) (pullback.snd B.hom f) <| by simp) (v₁₃ := Over.mkIdTerminal.from _) (h₂₂ := Over.mkIdTerminal.from _) - case p => ext; simp + case p => + ext + simp + exact pullback.lift_fst .. . apply (Over.forget Y).reflect_isPullback convert (IsPullback.of_hasPullback A.hom f).flip using 1 <;> simp + exact pullback.lift_snd .. . apply (Over.forget Y).reflect_isPullback convert (IsPullback.of_hasPullback B.hom f).flip using 1 <;> simp @@ -102,7 +106,7 @@ end Reindex section BinaryProduct -open Sigma Reindex +open Over.Sigma Reindex variable [HasFiniteWidePullbacks C] {X : C} @@ -113,13 +117,21 @@ def isBinaryProductSigmaReindex (Y Z : Over X) : · intro s fapply Over.homMk · exact pullback.lift (s.π.app ⟨.right⟩).left (s.π.app ⟨ .left ⟩).left (by aesop) - · aesop - · rintro s ⟨⟨l⟩|⟨r⟩⟩ <;> apply Over.OverMorphism.ext <;> simp [Reindex.sndProj] + · change pullback.lift _ _ _ ≫ pullback.snd Z.hom Y.hom ≫ Y.hom = s.pt.hom + rw [pullback.lift_snd_assoc] + exact Over.w _ + · rintro s ⟨⟨l⟩|⟨r⟩⟩ <;> apply Over.OverMorphism.ext + · exact pullback.lift_snd .. + · exact pullback.lift_fst .. · intro s m h apply Over.OverMorphism.ext - apply pullback.hom_ext <;> simp - · exact congr_arg CommaMorphism.left (h ⟨ .right⟩) - · exact congr_arg CommaMorphism.left (h ⟨ .left ⟩) + apply pullback.hom_ext + · change m.left ≫ pullback.fst Z.hom Y.hom = pullback.lift _ _ _ ≫ pullback.fst _ _ + rw [pullback.lift_fst] + exact congr_arg CommaMorphism.left (h ⟨ .right⟩) + · change m.left ≫ pullback.snd Z.hom Y.hom = pullback.lift _ _ _ ≫ pullback.snd _ _ + rw [pullback.lift_snd] + exact congr_arg CommaMorphism.left (h ⟨ .left ⟩) /-- The object `(Sigma Y) (Reindex Y Z)` is isomorphic to the binary product `Y × Z` in `Over X`. -/ @@ -150,7 +162,7 @@ end Over section TensorLeft -open Over Functor +open Over CategoryTheory.Functor variable [HasFiniteWidePullbacks C] {X : C} @@ -160,19 +172,32 @@ def Over.sigmaReindexNatIsoTensorLeft (Y : Over X) : (pullback Y.hom) ⋙ (map Y.hom) ≅ tensorLeft Y := by fapply NatIso.ofComponents · intro Z - simp only [const_obj_obj, Functor.id_obj, comp_obj, Over.pullback] exact sigmaReindexIsoProd Y Z · intro Z Z' f - dsimp - ext1 <;> simp_rw [assoc] - · rw [whiskerLeft_fst] - iterate rw [sigmaReindexIsoProd_hom_comp_fst] - ext + have hm : Y ◁ f = Limits.prod.map (𝟙 Y) f := by + ext1 + · simp only [whiskerLeft_fst] + exact (Category.comp_id _).symm.trans (Limits.prod.map_fst (𝟙 Y) f).symm + · simp only [whiskerLeft_snd] + exact (Limits.prod.map_snd (𝟙 Y) f).symm + change (map Y.hom).map ((pullback Y.hom).map f) ≫ (sigmaReindexIsoProd Y Z').hom = + (sigmaReindexIsoProd Y Z).hom ≫ Y ◁ f + rw [hm] + change (map Y.hom).map ((pullback Y.hom).map f) ≫ (sigmaReindexIsoProd Y Z').hom = + (sigmaReindexIsoProd Y Z).hom ≫ Limits.prod.map (𝟙 Y) f + have hf (Z : Over X) : (sigmaReindexIsoProd Y Z).hom ≫ Limits.prod.fst = + Reindex.fstProj Y Z := sigmaReindexIsoProd_hom_comp_fst + have hs (Z : Over X) : (sigmaReindexIsoProd Y Z).hom ≫ Limits.prod.snd = + Reindex.sndProj Y Z := sigmaReindexIsoProd_hom_comp_snd + apply Limits.prod.hom_ext + · simp only [assoc, hf, Limits.prod.map_fst, Category.comp_id] + apply Over.OverMorphism.ext simp - · rw [whiskerLeft_snd] - iterate rw [sigmaReindexIsoProd_hom_comp_snd, ← assoc, sigmaReindexIsoProd_hom_comp_snd] - ext + exact pullback.lift_snd .. + · rw [assoc, hs, assoc, Limits.prod.map_snd, ← assoc, hs] + apply Over.OverMorphism.ext simp [Reindex.sndProj] + exact pullback.lift_fst .. lemma Over.sigmaReindexNatIsoTensorLeft_hom_app {Y : Over X} (Z : Over X) : @@ -192,8 +217,15 @@ def Functor.toOverTerminal [HasTerminal C] : C ⥤ Over (⊤_ C) where /-- The slice category over the terminal object is equivalent to the original category. -/ def equivOverTerminal [HasTerminal C] : Over (⊤_ C) ≌ C := CategoryTheory.Equivalence.mk (Over.forget _) (Functor.toOverTerminal C) - (NatIso.ofComponents (fun X => Over.isoMk (Iso.refl _))) - (NatIso.ofComponents (fun X => Iso.refl _)) + (NatIso.ofComponents (fun X => Over.isoMk (Iso.refl _)) (by + intro X Y f + ext + change f.left ≫ 𝟙 _ = 𝟙 _ ≫ f.left + simp)) + (NatIso.ofComponents (fun X => Iso.refl _) (by + intro X Y f + change f ≫ 𝟙 _ = 𝟙 _ ≫ f + simp)) namespace Over @@ -201,9 +233,17 @@ open CartesianMonoidalCategory variable {C} +private theorem star_obj_hom_eq_fst [HasBinaryProducts C] (I X : C) : + ((star I).obj X).hom = prod.fst := + prod.lift_fst .. + lemma star_map [HasBinaryProducts C] {X : C} {Y Z : C} (f : Y ⟶ Z) : - (star X).map f = Over.homMk (prod.map (𝟙 X) f) (by aesop) := by - simp [star] + (star X).map f = Over.homMk (prod.map (𝟙 X) f) (by + change prod.map (𝟙 X) f ≫ ((star X).obj Z).hom = ((star X).obj Y).hom + rw [star_obj_hom_eq_fst, star_obj_hom_eq_fst] + exact (prod.map_fst _ _).trans (Category.comp_id _)) := by + apply Over.OverMorphism.ext + exact star_map_left X f /-- Note that the binary products assumption is necessary: the existence of a right adjoint to `Over.forget X` is equivalent to the existence of each binary product `X ⨯ -`. @@ -227,7 +267,10 @@ def starForgetIsoTensorLeft [HasFiniteLimits C] (X : C) : · intro Z exact Iso.refl _ · intro Z Z' f - simp [whiskerLeftProdMapId] + change prod.map (𝟙 X) f ≫ 𝟙 _ = 𝟙 _ ≫ X ◁ f + rw [whiskerLeftProdMapId] + change prod.map (𝟙 X) f ≫ 𝟙 (X ⨯ Z') = 𝟙 (X ⨯ Z) ≫ prod.map (𝟙 X) f + simp namespace forgetAdjStar @@ -235,21 +278,28 @@ variable [HasBinaryProducts C] @[simp] theorem unit_app {I : C} (X : Over I): (forgetAdjStar I).unit.app X = - Over.homMk (prod.lift X.hom (𝟙 X.left)) := by - ext - simp [forgetAdjStar, Adjunction.comp, Equivalence.symm] + Over.homMk (prod.lift X.hom (𝟙 X.left)) (by + change prod.lift X.hom (𝟙 X.left) ≫ ((star I).obj X.left).hom = X.hom + rw [star_obj_hom_eq_fst] + exact prod.lift_fst ..) := by + apply Over.OverMorphism.ext + exact Over.forgetAdjStar_unit_app_left I X @[simp] theorem counit_app {I : C} (X : C) : ((forgetAdjStar I).counit.app X) = prod.snd := by - simp [Over.forgetAdjStar, Adjunction.comp, Equivalence.symm] + exact Over.forgetAdjStar_counit_app I X @[simp] theorem homEquiv_homMk_lift {I : C} {X : Over I} {A : C} {f : X.left ⟶ A} : ((forgetAdjStar I).homEquiv X A) f = - Over.homMk (prod.lift X.hom f) := by + Over.homMk (prod.lift X.hom f) (by + rw [star_obj_hom_eq_fst] + exact prod.lift_fst ..) := by rw [Adjunction.homEquiv_unit, unit_app] - ext + apply Over.OverMorphism.ext + change prod.lift _ (𝟙 _) ≫ prod.map (𝟙 I) f = prod.lift _ f + rw [prod.lift_map] simp @[simp] @@ -261,9 +311,13 @@ theorem homEquiv_left_lift {I : C} {X : Over I} {A : C} {f : X.left ⟶ A} : theorem homEquiv_lift' {X I : C} {u : X ⟶ I} {A : C} {f : X ⟶ A} : ((forgetAdjStar I).homEquiv (.mk u) A) f = - Over.homMk (prod.lift u f) := by + Over.homMk (prod.lift u f) (by + rw [star_obj_hom_eq_fst] + exact prod.lift_fst ..) := by rw [Adjunction.homEquiv_unit, unit_app] - ext + apply Over.OverMorphism.ext + change prod.lift _ (𝟙 _) ≫ prod.map (𝟙 I) f = prod.lift _ f + rw [prod.lift_map] simp @[simp] diff --git a/Poly/ForMathlib/CategoryTheory/Comma/Over/Sections.lean b/Poly/ForMathlib/CategoryTheory/Comma/Over/Sections.lean index 609ffd6..b9f9e37 100644 --- a/Poly/ForMathlib/CategoryTheory/Comma/Over/Sections.lean +++ b/Poly/ForMathlib/CategoryTheory/Comma/Over/Sections.lean @@ -106,14 +106,14 @@ def sectionsMap {X X' : Over I} (u : X ⟶ X') : lemma sectionsMap_id {X : Over I} : sectionsMap (𝟙 X) = 𝟙 _ := by apply pullback.hom_ext · aesop - · simp [sectionsMap] + · simp [sectionsMap, pullback.map] @[simp] lemma sectionsMap_comp {X X' X'' : Over I} (u : X ⟶ X') (v : X' ⟶ X'') : sectionsMap (u ≫ v) = sectionsMap u ≫ sectionsMap v := by - apply pullback.hom_ext - · aesop - · simp [sectionsMap] + unfold sectionsMap + rw [pullback.map_comp] + simp only [id_comp, Functor.map_comp, Over.comp_left] variable (I) @@ -140,6 +140,12 @@ def sectionsCurry {X : Over I} {A : C} (u : (star I).obj A ⟶ X) : (MonoidalClosed.uncurry_injective _) rw [MonoidalClosed.uncurry_natural_left] simp [curryId, MonoidalClosed.uncurry_natural_right, MonoidalClosed.uncurry_curry] + have hu : u.left ≫ X.hom = prod.fst := (Over.w u).trans (prod.lift_fst ..) + calc + fst I A = (prodIsoTensorObj I A).inv ≫ prod.fst := prodIsoTensorObj_inv_fst.symm + _ = (prodIsoTensorObj I A).inv ≫ (u.left ≫ X.hom) := + congrArg (fun k : I ⨯ A ⟶ I => (prodIsoTensorObj I A).inv ≫ k) hu.symm + _ = ((prodIsoTensorObj I A).inv ≫ u.left) ≫ X.hom := (Category.assoc _ _ _).symm /-- The uncurrying operation `Hom A (section X) → Hom ((star I).obj A) X`. -/ def sectionsUncurry {X : Over I} {A : C} (v : A ⟶ (sections I).obj X) : @@ -147,32 +153,53 @@ def sectionsUncurry {X : Over I} {A : C} (v : A ⟶ (sections I).obj X) : let v₂ : A ⟶ (I ⟹ X.left) := v ≫ pullback.snd .. have w : terminal.from A ≫ (curryId I) = v₂ ≫ (ihom I).map X.hom := by rw [IsTerminal.hom_ext terminalIsTerminal (terminal.from A ) (v ≫ (pullback.fst ..))] - simp [v₂, pullback.condition] + exact (Category.assoc _ _ _).trans + ((congrArg (fun k => v ≫ k) + (pullback.condition (f := curryId I) (g := (ihom I).map X.hom))).trans + (Category.assoc _ _ _).symm) dsimp [curryId] at w have w' := homEquiv_naturality_right_square (F := MonoidalCategory.tensorLeft I) (adj := ihom.adjunction I) _ _ _ _ w simp [MonoidalClosed.curry] at w' refine Over.homMk ((prodIsoTensorObj I A).hom ≫ MonoidalClosed.uncurry v₂) ?_ · dsimp [MonoidalClosed.uncurry] at * - rw [Category.assoc, ← w'] - simp [star_obj_hom] + change ((prodIsoTensorObj I A).hom ≫ ((ihom.adjunction I).homEquiv A X.left).symm v₂) ≫ + X.hom = prod.lift prod.fst (𝟙 (I ⨯ A)) ≫ prod.fst + rw [Category.assoc, ← w', prodIsoTensorObj_hom_fst, prod.lift_fst] + +private theorem sectionsCurry_snd {X : Over I} {A : C} (u : (star I).obj A ⟶ X) : + sectionsCurry u ≫ pullback.snd (curryId I) ((ihom I).map X.hom) = + MonoidalClosed.curry ((prodIsoTensorObj I A).inv ≫ u.left) := + pullback.lift_snd .. + +private theorem sectionsMap_snd {X X' : Over I} (u : X ⟶ X') : + sectionsMap u ≫ pullback.snd (curryId I) ((ihom I).map X'.hom) = + pullback.snd (curryId I) ((ihom I).map X.hom) ≫ (ihom I).map u.left := + pullback.lift_snd .. @[simp] theorem sections_curry_uncurry {X : Over I} {A : C} {v : A ⟶ (sections I).obj X} : sectionsCurry (sectionsUncurry v) = v := by - dsimp [sectionsCurry, sectionsUncurry] - let v₂ : A ⟶ (I ⟹ X.left) := v ≫ pullback.snd _ _ apply pullback.hom_ext - · simp - rw [IsTerminal.hom_ext terminalIsTerminal (terminal.from A ) (v ≫ (pullback.fst ..))] - · simp + · exact terminalIsTerminal.hom_ext _ _ + · calc + sectionsCurry (sectionsUncurry v) ≫ pullback.snd _ _ = + MonoidalClosed.curry ((prodIsoTensorObj I A).inv ≫ (sectionsUncurry v).left) := + sectionsCurry_snd _ + _ = MonoidalClosed.curry ((prodIsoTensorObj I A).inv ≫ (prodIsoTensorObj I A).hom ≫ + MonoidalClosed.uncurry (v ≫ pullback.snd _ _)) := rfl + _ = v ≫ pullback.snd _ _ := + (congrArg MonoidalClosed.curry (Iso.inv_hom_id_assoc _ _)).trans + (MonoidalClosed.curry_uncurry _) @[simp] theorem sections_uncurry_curry {X : Over I} {A : C} {u : (star I).obj A ⟶ X} : sectionsUncurry (sectionsCurry u) = u := by - dsimp [sectionsCurry, sectionsUncurry] - ext - simp + apply Over.OverMorphism.ext + exact (congrArg (fun k => (prodIsoTensorObj I A).hom ≫ MonoidalClosed.uncurry k) + (sectionsCurry_snd u)).trans + ((congrArg (fun k => (prodIsoTensorObj I A).hom ≫ k) + (MonoidalClosed.uncurry_curry _)).trans (Iso.hom_inv_id_assoc _ _)) /-- An auxiliary definition which is used to define the adjunction between the star functor and the sections functor. See starSectionsAdjunction`. -/ @@ -185,17 +212,31 @@ def coreHomEquiv : CoreHomEquiv (star I) (sections I) where } homEquiv_naturality_left_symm := by intro A' A X g v - dsimp [sectionsCurry, sectionsUncurry, curryId] - simp only [star_map] - rw [← Over.homMk_comp] -- note: in a newer version of mathlib this is `Over.homMk_eta` - congr 1 - simp [MonoidalClosed.uncurry_natural_left] + let v₂ : A ⟶ I ⟹ X.left := v ≫ pullback.snd _ _ + have h : (prodIsoTensorObj I A').hom ≫ MonoidalClosed.uncurry (g ≫ v₂) = + prod.map (𝟙 I) g ≫ (prodIsoTensorObj I A).hom ≫ MonoidalClosed.uncurry v₂ := by + rw [MonoidalClosed.uncurry_natural_left, ← Category.assoc, ← id_tensorHom, + ← prodMap_comp_prodIsoTensorObj_hom, Category.assoc] + apply Over.OverMorphism.ext + exact (congrArg (fun k => (prodIsoTensorObj I A').hom ≫ MonoidalClosed.uncurry k) + (Category.assoc g v (pullback.snd _ _))).trans h homEquiv_naturality_right := by intro A X' X u g - dsimp [sectionsCurry, sectionsUncurry, curryId] apply pullback.hom_ext (IsTerminal.hom_ext terminalIsTerminal _ _) - simp [sectionsMap, curryId] - rw [← MonoidalClosed.curry_natural_right, Category.assoc] + calc + sectionsCurry (u ≫ g) ≫ pullback.snd _ _ = + MonoidalClosed.curry ((prodIsoTensorObj I A).inv ≫ (u ≫ g).left) := + sectionsCurry_snd _ + _ = MonoidalClosed.curry (((prodIsoTensorObj I A).inv ≫ u.left) ≫ g.left) := + congrArg MonoidalClosed.curry (Category.assoc _ _ _).symm + _ = MonoidalClosed.curry ((prodIsoTensorObj I A).inv ≫ u.left) ≫ (ihom I).map g.left := + MonoidalClosed.curry_natural_right _ _ + _ = (sectionsCurry u ≫ pullback.snd _ _) ≫ (ihom I).map g.left := + congrArg (fun k => k ≫ (ihom I).map g.left) (sectionsCurry_snd u).symm + _ = sectionsCurry u ≫ (pullback.snd _ _ ≫ (ihom I).map g.left) := Category.assoc _ _ _ + _ = sectionsCurry u ≫ (sectionsMap g ≫ pullback.snd _ _) := + congrArg (fun k => sectionsCurry u ≫ k) (sectionsMap_snd g).symm + _ = (sectionsCurry u ≫ sectionsMap g) ≫ pullback.snd _ _ := (Category.assoc _ _ _).symm variable (I) diff --git a/Poly/ForMathlib/CategoryTheory/Elements.lean b/Poly/ForMathlib/CategoryTheory/Elements.lean index b19ae69..d8038ea 100644 --- a/Poly/ForMathlib/CategoryTheory/Elements.lean +++ b/Poly/ForMathlib/CategoryTheory/Elements.lean @@ -10,22 +10,22 @@ namespace CategoryTheory.CategoryOfElements variable {𝒞 𝒟 : Type*} [Category 𝒞] [Category 𝒟] variable (F : 𝒞 ⥤ Type*) (G : F.Elements ⥤ 𝒟) --- FIXME(mathlib): `NatTrans.mapElements` and `CategoryOfElements.map` are the same thing - @[simp] theorem map_homMk_id {X : 𝒞} (a : F.obj X) (eq : F.map (𝟙 X) a = a) : - -- NOTE: without `α := X ⟶ X`, a bad discrimination tree key involving `⟨X, a⟩.1` is generated. - G.map (Subtype.mk (α := X ⟶ X) (𝟙 X) eq) = 𝟙 (G.obj ⟨X, a⟩) := + G.map (X := F.elementsMk X a) (Y := F.elementsMk X a) + (Functor.Elements.homMk (𝟙 X) eq) = 𝟙 (G.obj (F.elementsMk X a)) := show G.map (𝟙 _) = 𝟙 _ by simp @[simp] theorem map_homMk_comp {X Y Z : 𝒞} (f : X ⟶ Y) (g : Y ⟶ Z) (a : F.obj X) eq : - G.map (Y := ⟨Z, F.map g (F.map f a)⟩) (Subtype.mk (α := X ⟶ Z) (f ≫ g) eq) = - G.map (X := ⟨X, a⟩) (Y := ⟨Y, F.map f a⟩) (Subtype.mk (α := X ⟶ Y) f rfl) ≫ - G.map (Subtype.mk g rfl) := by - set X : F.Elements := ⟨X, a⟩ - set Y : F.Elements := ⟨Y, F.map f a⟩ - set Z : F.Elements := ⟨Z, F.map g (F.map f a)⟩ + G.map (X := F.elementsMk X a) (Y := F.elementsMk Z (F.map g (F.map f a))) + (Functor.Elements.homMk (f ≫ g) eq) = + G.map (X := F.elementsMk X a) (Y := F.elementsMk Y (F.map f a)) + (Functor.Elements.homMk f rfl) ≫ + G.map (Functor.Elements.homMk g rfl) := by + set X : F.Elements := F.elementsMk X a + set Y : F.Elements := F.elementsMk Y (F.map f a) + set Z : F.Elements := F.elementsMk Z (F.map g (F.map f a)) set f : X ⟶ Y := ⟨f, rfl⟩ set g : Y ⟶ Z := ⟨g, rfl⟩ show G.map (f ≫ g) = G.map f ≫ G.map g diff --git a/Poly/ForMathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean b/Poly/ForMathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean index e76ce64..1c8a96d 100644 --- a/Poly/ForMathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean +++ b/Poly/ForMathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean @@ -22,9 +22,13 @@ theorem reflect_isPullback let i := cospanCompIso F h i apply IsLimit.equivOfNatIsoOfIso i.symm pb.cone _ _ pb.isLimit let j : - ((Cones.postcompose i.symm.hom).obj pb.cone).pt ≅ + ((Cone.postcompose i.symm.hom).obj pb.cone).pt ≅ (F.mapCone <| PullbackCone.mk f g sq.w).pt := Iso.refl _ - apply WalkingCospan.ext j <;> simp +zetaDelta + apply WalkingCospan.ext j + · change F.map f ≫ 𝟙 _ = 𝟙 _ ≫ F.map f + simp + · change F.map g ≫ 𝟙 _ = 𝟙 _ ≫ F.map g + simp end CategoryTheory.Functor diff --git a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Basic.lean b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Basic.lean index c1726dd..a340cce 100644 --- a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Basic.lean +++ b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Basic.lean @@ -62,8 +62,8 @@ universe v u namespace CategoryTheory -open CategoryTheory Category MonoidalCategory CartesianMonoidalCategory Limits Functor Adjunction - Over +open CategoryTheory Category MonoidalCategory CartesianMonoidalCategory Limits + CategoryTheory.Functor Adjunction Over variable {C : Type u} [Category.{v} C] @@ -177,6 +177,7 @@ instance isMultiplicative : (ExponentiableMorphism (C:= C)).IsMultiplicative whe comp_mem f g fexp gexp := by infer_instance /-- A morphism with a pushforward is an exponentiable object in the slice category. -/ +@[instance_reducible] def exponentiableOverMk [HasFiniteWidePullbacks C] {X I : C} (f : X ⟶ I) [ExponentiableMorphism f] : Closed (Over.mk f) where @@ -192,7 +193,7 @@ morphism `X.hom`. Here the pushforward functor along a morphism `f : I ⟶ J` is defined using the section functor `Over (Over.mk f) ⥤ Over J`. -/ -def ofOverExponentiable [HasFiniteWidePullbacks C] {I : C} (X : Over I) [Closed X] : +theorem ofOverExponentiable [HasFiniteWidePullbacks C] {I : C} (X : Over I) [Closed X] : ExponentiableMorphism X.hom := ⟨X.iteratedSliceEquiv.inverse ⋙ sections X, ⟨by refine ofNatIsoLeft (Adjunction.comp ?_ ?_) (starIteratedSliceForwardIsoPullback X.hom) @@ -282,10 +283,12 @@ abbrev ev' {I : C} (X : Over I) (Y : Over X.left) : Reindex X (Pi X Y) ⟶ Y := adj X.hom |>.counit.app Y /-- A locally cartesian closed category with a terminal object is cartesian closed. -/ +@[instance_reducible] def monoidalClosed [HasTerminal C] : MonoidalClosed C := cartesianClosedOfEquiv <| equivOverTerminal C /-- The slices of a locally cartesian closed category are locally cartesian closed. -/ +@[instance_reducible] def overLocallyCartesianClosed (I : C) : LocallyCartesianClosed (Over I) := by apply (config := { allowSynthFailures:= true}) mkOfCartesianClosedOver intro X diff --git a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/BeckChevalley.lean b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/BeckChevalley.lean index ff77bff..1b06775 100644 --- a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/BeckChevalley.lean +++ b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/BeckChevalley.lean @@ -49,7 +49,7 @@ in Mathematical Structures in Computer Science, 2024][Hazratpour_Riehl_2024] noncomputable section namespace CategoryTheory -open Category Functor Adjunction Limits NatTrans ExponentiableMorphism +open Category CategoryTheory.Functor Adjunction Limits NatTrans ExponentiableMorphism universe v u @@ -97,7 +97,8 @@ map k | ↙ | map h -/ --pullbackBeckChevalleySquare def pullbackMapTwoSquare : TwoSquare (pullback f) (map k) (map h) (pullback g) := - mateEquiv (mapPullbackAdj f) (mapPullbackAdj g) (mapIsoSquare sq).hom + mateEquiv (mapPullbackAdj f) (mapPullbackAdj g) + (TwoSquare.mk _ _ _ _ (mapIsoSquare sq).hom) /-- The natural transformation `pullback f ⋙ forget X ⟶ forget Y ⋙ 𝟭 C` @@ -111,8 +112,10 @@ forget Y | ↙ | forget X ``` -/ def pullbackForgetTwoSquare : TwoSquare (pullback f) (forget Y) (forget X) (𝟭 C) := - mateEquiv (mapPullbackAdj f) Adjunction.id (mapForget f).inv + mateEquiv (mapPullbackAdj f) Adjunction.id + (TwoSquare.mk _ _ _ _ (mapForget f).inv) +set_option backward.isDefEq.respectTransparency.types false in theorem isCartesian_pullbackForgetTwoSquare {X Y : C} (f : X ⟶ Y) : NatTrans.IsCartesian (pullbackForgetTwoSquare f) := by unfold pullbackForgetTwoSquare @@ -282,9 +285,9 @@ theorem pullback.map_isIso_of_pullback_right_of_comm_cube {W X Y Z S T : C} IsIso (pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ sq_bot.w pb_right.w.symm) := by let m := pullback.map f₁ f₂ g₁ g₂ i₁ i₂ i₃ sq_bot.w pb_right.w.symm have sq_top : CommSq (pullback.snd f₁ f₂) m i₂ (pullback.snd g₁ g₂) := by - aesop + exact ⟨by simp [m, pullback.map, pullback.lift_snd]⟩ have sq_left : CommSq m (pullback.fst f₁ f₂) (pullback.fst g₁ g₂) i₁ := by - aesop + exact ⟨by simp [m, pullback.map, pullback.lift_fst]⟩ let pb' : IsPullback m (pullback.fst f₁ f₂) (pullback.fst g₁ g₂) i₁ := by apply IsPullback.left_face_of_comm_cube (sq_top := sq_top) (sq_bot := sq_bot) (sq_left := sq_left) (pb_back := (IsPullback.of_hasPullback f₁ f₂).flip) @@ -298,7 +301,7 @@ end IsPullback variable [HasPullbacks C] variable {X Y Z W : C} {h : X ⟶ Z} {f : X ⟶ Y} {g : Z ⟶ W} {k : Y ⟶ W} -(sq : CommSq h f g k) (A : Over Y) + (sq : CommSq h f g k) (A : Over Y) open IsPullback Over @@ -309,10 +312,11 @@ theorem mapPullbackAdj.counit_app_left : @[simp] theorem pullbackMapTwoSquare_app : (pullbackMapTwoSquare h f g k sq).app A = - Over.homMk (pullback.map _ _ (A.hom ≫ k) _ _ h k (id_comp _).symm sq.w.symm) (by aesop) := by + Over.homMk (pullback.map _ _ (A.hom ≫ k) _ _ h k (id_comp _).symm sq.w.symm) (by simp [pullback.map, pullback.lift_snd]) := by ext - simp only [homMk_left, pullbackMapTwoSquare, mapIsoSquare] - aesop + simp only [homMk_left, pullbackMapTwoSquare, mapIsoSquare, mateEquiv_apply] + apply pullback.hom_ext <;> + simp [pullback.map, pullback.lift_fst, pullback.lift_snd, pullback.lift_fst_assoc, Category.assoc] theorem forget_map_pullbackMapTwoSquare : (Over.forget Z).map ((pullbackMapTwoSquare h f g k sq).app A) = diff --git a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean index ac406aa..8b7ebcb 100644 --- a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean +++ b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean @@ -29,7 +29,7 @@ We construct a natural isomorphism noncomputable section namespace CategoryTheory -open Category Functor Adjunction Limits NatTrans Over ExponentiableMorphism Reindex +open Category CategoryTheory.Functor Adjunction Limits NatTrans Over ExponentiableMorphism Reindex LocallyCartesianClosed universe v u @@ -50,7 +50,7 @@ exponentiable morphisms, we'll usually prove all morphims are exponential unifor from LocallyCartesianClosed structure. The instance is inferred from the LocallyCartesianClosed structure, but we should prove this more generally without assuming the LCCC structure. -/ -def exponentiableMorphism : ExponentiableMorphism (g f u) := by infer_instance +theorem exponentiableMorphism : ExponentiableMorphism (g f u) := by infer_instance namespace ExponentiableMorphism @@ -61,10 +61,14 @@ def mapPullbackAdj_regularMono {C} [Category C] [HasPullbacks C] {A B : C} (F : have := congr($((whiskerLeft_comp_whiskerRight η η)).app X) refine ⟨_, _, _, this, Fork.IsLimit.mk' _ fun s => ?_⟩ have hi := (Fork.ι s).w; simp at hi - have w := congr($(Fork.condition s).left ≫ pullback.fst .. ≫ pullback.snd ..); simp [η] at w + have w := congr($(Fork.condition s).left ≫ pullback.fst .. ≫ pullback.snd ..) + simp [η, pullback.lift_snd, pullback.lift_fst_assoc] at w refine ⟨homMk (s.ι.left ≫ pullback.fst ..) (by simp [w, hi]), ?_, ?_⟩ - · ext; simp; ext <;> simp [η]; rw [w] - · intro m H; ext; simpa [η] using congr(($H).left ≫ pullback.fst ..) + · ext; simp; ext <;> simp [η, pullback.lift_fst, pullback.lift_snd]; rw [w] + · intro m H + ext + simpa [η, pullback.lift_fst, pullback.lift_snd, pullback.lift_fst_assoc] using + congr(($H).left ≫ pullback.fst ..) /-- The pullback of exponentiable morphisms is exponentiable. -/ theorem of_isPullback {C' : Type u} [Category.{v} C'] [HasPullbacks C'] [HasTerminal C'] @@ -99,7 +103,7 @@ We show that the pasting of the 2-cells in below is an isomorphism. so the 2-cell is an iso. -/ -def cellLeftTriangle : e f u ≫ u = w f u := by +theorem cellLeftTriangle : e f u ≫ u = w f u := by unfold e w v have := ((ev f).app (Over.mk u)).w aesop_cat @@ -116,7 +120,7 @@ lemma isCartesian_cellLeft : IsCartesian (cellLeft f u) := by simp only [id_obj, mk_left] at α u sorry -def cellRightCommSq : CommSq (g f u) (w f u) (v f u) f := +theorem cellRightCommSq : CommSq (g f u) (w f u) (v f u) f := IsPullback.toCommSq (IsPullback.of_hasPullback _ _) def cellRight' : pushforward (g f u) ⋙ map (v f u) @@ -137,7 +141,7 @@ def pasteCell2 : (pullback (e f u) ⋙ map (w f u)) ⋙ pushforward f def pasteCell := pasteCell1 f u ≫ pasteCell2 f u -def paste : IsCartesian (pasteCell f u) := by +theorem paste : IsCartesian (pasteCell f u) := by apply IsCartesian.comp · unfold pasteCell1 apply (isCartesian_cellRight' f u).whiskerLeft diff --git a/Poly/ForMathlib/CategoryTheory/NatTrans.lean b/Poly/ForMathlib/CategoryTheory/NatTrans.lean index fea7cc5..151e0ac 100644 --- a/Poly/ForMathlib/CategoryTheory/NatTrans.lean +++ b/Poly/ForMathlib/CategoryTheory/NatTrans.lean @@ -19,7 +19,7 @@ variable {K : Type*} [Category K] {D : Type*} [Category D] namespace NatTrans -open Functor +open CategoryTheory.Functor /-- A natural transformation is *cartesian* if all its naturality squares are pullbacks. -/ diff --git a/Poly/ForMathlib/CategoryTheory/PartialProduct.lean b/Poly/ForMathlib/CategoryTheory/PartialProduct.lean index e33d783..7a2a2ac 100644 --- a/Poly/ForMathlib/CategoryTheory/PartialProduct.lean +++ b/Poly/ForMathlib/CategoryTheory/PartialProduct.lean @@ -21,7 +21,7 @@ noncomputable section namespace CategoryTheory -open CategoryTheory Category Limits Functor Over +open CategoryTheory Category Limits CategoryTheory.Functor Over variable {C : Type*} [Category C] [HasPullbacks C] @@ -66,7 +66,11 @@ def Fan.overPullbackToStar [HasBinaryProducts C] (c : Fan s X) : @[reassoc (attr := simp)] theorem Fan.overPullbackToStar_snd {c : Fan s X} [HasBinaryProducts C] : (Fan.overPullbackToStar c).left ≫ prod.snd = c.snd := by - simp [Fan.overPullbackToStar, Adjunction.homEquiv, forgetAdjStar.unit_app] + change ((forgetAdjStar E).homEquiv ((Over.pullback s).obj c.over) X c.snd).left ≫ + prod.snd = c.snd + exact (congrArg (fun k => k ≫ prod.snd) + (forgetAdjStar.homEquiv_left_lift (I := E) (X := (Over.pullback s).obj c.over) + (f := c.snd))).trans (prod.lift_snd _ _) -- note: the reason we use `(Over.pullback s).map` instead of `pullback.map` is that -- we want to readily use lemmas about the adjunction `pullback s ⊣ pushforward s` in `UvPoly`. @@ -110,7 +114,8 @@ instance : Category (Fan s X) where rw [← f.w_right, ← g.w_right] simp_rw [← Category.assoc] congr 1 - ext <;> simp [pullbackMap] + ext <;> simp [pullbackMap, pullback.lift_fst, pullback.lift_snd, + pullback.lift_fst_assoc, Category.assoc] ⟩ id_comp f := by dsimp; ext; simp comp_id f := by dsimp; ext; simp @@ -165,9 +170,7 @@ def overPullbackToStar [HasBinaryProducts C] {W} (f : W ⟶ B) (g : pullback f s theorem overPullbackToStar_prod_snd [HasBinaryProducts C] {W} {f : W ⟶ B} {g : pullback f s ⟶ X} : (overPullbackToStar f g).left ≫ prod.snd = g := by - simp only [overPullbackToStar, Fan.overPullbackToStar, Fan.over] - simp only [forgetAdjStar.homEquiv_left_lift] - aesop + exact Fan.overPullbackToStar_snd (c := Fan.mk f g) abbrev partialProd (c : LimitFan s X) : C := c.cone.pt @@ -197,7 +200,8 @@ theorem partialProd.lift_snd {W} (c : LimitFan s X) (f : W ⟶ B) (g : pullback conv_rhs => arg 2; exact ((isLimit c).fac_right (Fan.mk f g)).symm rw [← pullbackMap_comparison] rw [← Category.assoc]; congr 1 - ext <;> simp [pullbackMap] + ext <;> simp [pullbackMap, pullback.lift_fst, pullback.lift_snd, + pullback.lift_fst_assoc, pullback.map, Category.assoc] -- theorem hom_lift (h : IsLimit t) {W : C} (m : W ⟶ t.pt) : -- m = h.lift { pt := W, π := { app := fun b => m ≫ t.π.app b } } := @@ -211,5 +215,6 @@ theorem partialProd.hom_ext {W : C} (c : LimitFan s X) {f g : W ⟶ partialProd 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'] + ext <;> simp [pullbackMap, comparison, f', pullback.lift_fst, pullback.lift_snd, + pullback.lift_fst_assoc, pullback.map, Category.assoc] exact c.isLimit.uniq f' f rfl rfl diff --git a/Poly/ForMathlib/CategoryTheory/Types.lean b/Poly/ForMathlib/CategoryTheory/Types.lean index 3eb6659..6043294 100644 --- a/Poly/ForMathlib/CategoryTheory/Types.lean +++ b/Poly/ForMathlib/CategoryTheory/Types.lean @@ -21,18 +21,18 @@ variable {𝒞 𝒟 : Type*} [Category 𝒞] [Category 𝒟] (F G : 𝒞 ⥤ theorem naturality₂_left (σ : F ⟶ G) (f : C₁ ⟶ C₂) (x : (F.obj C₁).obj D₁) : (σ.app C₂).app D₁ ((F.map f).app D₁ x) = (G.map f).app D₁ ((σ.app C₁).app D₁ x) := - congr_fun (congr_fun (congr_arg NatTrans.app (σ.naturality f)) D₁) x + types_congr_hom (congrArg (fun η => η.app D₁) (σ.naturality f)) x theorem naturality₂_right (σ : F ⟶ G) (f : D₁ ⟶ D₂) (x : (F.obj C₁).obj D₁) : (σ.app C₁).app D₂ ((F.obj C₁).map f x) = (G.obj C₁).map f ((σ.app C₁).app D₁ x) := - naturality .. + ConcreteCategory.congr_hom ((σ.app C₁).naturality f) x @[simp] theorem hom_inv_id_app_app_apply (α : F ≅ G) (C D) (x) : (α.inv.app C).app D ((α.hom.app C).app D x) = x := - congr_fun (α.hom_inv_id_app_app C D) x + ConcreteCategory.congr_hom (α.hom_inv_id_app_app C D) x @[simp] theorem inv_hom_id_app_app_apply (α : F ≅ G) (C D) (x) : (α.hom.app C).app D ((α.inv.app C).app D x) = x := - congr_fun (α.inv_hom_id_app_app C D) x + ConcreteCategory.congr_hom (α.inv_hom_id_app_app C D) x diff --git a/Poly/MvPoly/Basic.lean b/Poly/MvPoly/Basic.lean index 3edc114..6d17554 100644 --- a/Poly/MvPoly/Basic.lean +++ b/Poly/MvPoly/Basic.lean @@ -26,7 +26,7 @@ noncomputable section namespace CategoryTheory -open CategoryTheory Category Limits Functor Adjunction ExponentiableMorphism +open CategoryTheory Category Limits CategoryTheory.Functor Adjunction ExponentiableMorphism variable {C : Type*} [Category C] [HasPullbacks C] [HasTerminal C] [HasFiniteWidePullbacks C] diff --git a/Poly/Type/Univariate.lean b/Poly/Type/Univariate.lean index 0bb4cbe..89fa2aa 100644 --- a/Poly/Type/Univariate.lean +++ b/Poly/Type/Univariate.lean @@ -98,8 +98,8 @@ def sumTotalEquiv (P Q : Poly) : Total (sum P Q) ≃ Total P ⊕ Total Q where | Sum.inl ⟨b, e⟩ => ⟨Sum.inl b, e⟩ | Sum.inr ⟨c, f⟩ => ⟨Sum.inr c, f⟩ left_inv := by - simp - aesop_cat + rintro ⟨b, e⟩ + cases b <;> rfl right_inv := by aesop_cat /-- The bundle associated to a polynomial `P`. -/ @@ -177,7 +177,7 @@ theorem map_map (f : X → Y) (g : Y → Z) : /-- The associated functor of `P : Poly`. -/ def functor : Type u ⥤ Type u where obj X := P X - map {X Y} f := P.map f + map {X Y} f := TypeCat.ofHom (P.map f) variable {P} @@ -189,7 +189,7 @@ def Obj.iget [DecidableEq P.B] {X} [Inhabited X] (x : P X) (i : P.Total) : X := @[simp] theorem iget_map [DecidableEq P.B] [Inhabited X] [Inhabited Y] (x : P X) (f : X → Y) (i : P.Total) (h : i.1 = x.1) : (P.map f x).iget i = f (x.iget i) := by - simp only [Obj.iget, fst_map, *, dif_pos] + simp only [Obj.iget, fst_map, *, dite_eq_left] cases x rfl @@ -224,12 +224,12 @@ def comp.mk {X : Type u} (x : P (Q X)) : Q.comp P X := /-- Functor composition for polynomial functors in the diagrammatic order. -/ def comp.functor : Poly.functor (Q.comp P) ≅ Poly.functor Q ⋙ Poly.functor P where hom := { - app := fun X => fun ⟨b,e⟩ => + app := fun X => TypeCat.ofHom fun ⟨b,e⟩ => ⟨ b.1, fun x' => ⟨ b.2 x', fun b' => e ⟨x',b'⟩ ⟩⟩ naturality := by aesop_cat } inv := { - app X := comp.mk P Q + app X := TypeCat.ofHom (comp.mk P Q) naturality := by aesop_cat } diff --git a/Poly/UvPoly/Basic.lean b/Poly/UvPoly/Basic.lean index 74e0d4f..df28252 100644 --- a/Poly/UvPoly/Basic.lean +++ b/Poly/UvPoly/Basic.lean @@ -37,7 +37,7 @@ noncomputable section namespace CategoryTheory -open Category Limits Functor Adjunction Over ExponentiableMorphism +open Category Limits CategoryTheory.Functor Adjunction Over ExponentiableMorphism LocallyCartesianClosed variable {C : Type*} [Category C] [HasPullbacks C] @@ -134,10 +134,11 @@ C --- > C/E ----> C/B ----> C def verticalNatTrans {F : C} (P : UvPoly E B) (Q : UvPoly F B) (ρ : E ⟶ F) (h : P.p = ρ ≫ Q.p) : Q.functor ⟶ P.functor := by have sq : CommSq ρ P.p Q.p (𝟙 _) := by simp [h] - let cellLeft := (Over.starPullbackIsoStar ρ).hom + let cellLeft : TwoSquare (star F) (𝟭 C) (Over.pullback ρ) (star E) := + (Over.starPullbackIsoStar ρ).hom let cellMid := (pushforwardPullbackTwoSquare ρ P.p Q.p (𝟙 _) sq) let cellLeftMidPasted := TwoSquare.whiskerRight (cellLeft ≫ₕ cellMid) (Over.pullbackId).inv - simpa using (cellLeftMidPasted ≫ₕ (vId (Over.forget B))) + exact (cellLeftMidPasted ≫ₕ (vId (Over.forget B))).natTrans /-- A cartesian map of polynomials ``` @@ -269,7 +270,7 @@ variable {E B : C} namespace PartialProduct -open PartialProduct +open CategoryTheory.PartialProduct /-- The counit of the adjunction `pullback P.p ⊣ pushforward P.p` evaluated `(star E).obj X`. -/ def ε (P : UvPoly E B) (X : C) : pullback (P.fstProj X) P.p ⟶ E ⨯ X := @@ -284,13 +285,16 @@ def fan (P : UvPoly E B) (X : C) : PartialProduct.Fan P.p X where attribute [simp] fan_pt fan_fst +set_option backward.isDefEq.respectTransparency false in /-- `P.PartialProduct.fan` is in fact a limit fan; this provides the univeral mapping property of the polynomial functor. -/ def isLimitFan (P : UvPoly E B) (X : C) : PartialProduct.IsLimit (PartialProduct.fan P X) where lift c := (pushforwardCurry <| overPullbackToStar c.fst c.snd).left - fac_left := by aesop_cat (add norm fstProj) + fac_left := by + intro c + exact Over.w (pushforwardCurry (overPullbackToStar c.fst c.snd)) fac_right := by intro c simp only [fan_snd, PartialProduct.pullbackMap, ε, ev, ← assoc, ← comp_left] @@ -307,13 +311,13 @@ def isLimitFan (P : UvPoly E B) (X : C) : PartialProduct.IsLimit (PartialProduct simp [overPullbackToStar, PartialProduct.Fan.overPullbackToStar, PartialProduct.Fan.over] apply (Adjunction.homEquiv_apply_eq _ _ _).mpr rw [← h_right] - simp [forgetAdjStar, comp_homEquiv, Comonad.adj] - simp [Equivalence.toAdjunction, homEquiv] - simp [coalgebraEquivOver, Equivalence.symm]; rfl + rw [Adjunction.homEquiv_counit (forgetAdjStar E)] + simp [homEquiv_counit, PartialProduct.pullbackMap, fan_snd, ε, ev, Category.assoc] + rfl end PartialProduct -open PartialProduct +open CategoryTheory.UvPoly.PartialProduct /-- Morphisms `b : Γ ⟶ B` and `e : pullback b P.p ⟶ X` induce a morphism `Γ ⟶ P @ X` which is the lift of the partial product fan. -/ @@ -353,28 +357,31 @@ theorem proj_fst {Γ X : C} {P : UvPoly E B} {f : Γ ⟶ P @ X} : @[simp] theorem proj_snd {Γ X : C} {P : UvPoly E B} {f : Γ ⟶ P @ X} : (proj P f).snd = pullback.map _ _ _ _ f (𝟙 E) (𝟙 B) (by simp) (by simp) ≫ (fan P X).snd := by - simp [proj] + rfl /-- The domain of the composition of two polynomials. See `UvPoly.comp`. -/ def compDom {E B D A : C} (P : UvPoly E B) (Q : UvPoly D A) := Limits.pullback Q.p (fan P A).snd @[simps!] -def comp [HasPullbacks C] [HasTerminal C] +def comp {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 := - haveI := ExponentiableMorphism.of_isPullback (.flip <| .of_hasPullback Q.p (fan P A).snd) - haveI := ExponentiableMorphism.of_isPullback (.of_hasPullback (fan P A).fst P.p) - inferInstance + exp := by + have : ExponentiableMorphism (pullback.snd Q.p (fan P A).snd) := + ExponentiableMorphism.of_isPullback (.flip <| .of_hasPullback Q.p (fan P A).snd) + have : ExponentiableMorphism (pullback.fst (fan P A).fst P.p) := + ExponentiableMorphism.of_isPullback (.of_hasPullback (fan P A).fst P.p) + exact ExponentiableMorphism.comp + (pullback.snd Q.p (fan P A).snd) (pullback.fst (fan P A).fst P.p) /-- The associated functor of the composition of two polynomials is isomorphic to the composition of the associated functors. -/ -def compFunctorIso [HasPullbacks C] [HasTerminal C] +def compFunctorIso {E B D C : C} (P : UvPoly E B) (Q : UvPoly D C) : P.functor ⋙ Q.functor ≅ (comp P Q).functor := by sorry -instance monoidal [HasPullbacks C] [HasTerminal C] : MonoidalCategory (UvPoly.Total C) where +instance monoidal : MonoidalCategory (UvPoly.Total C) where tensorObj X Y := ⟨comp X.poly Y.poly⟩ whiskerLeft X Y₁ Y₂ := sorry whiskerRight := sorry diff --git a/Poly/UvPoly/UPFan.lean b/Poly/UvPoly/UPFan.lean index 4ccc736..cf9c656 100644 --- a/Poly/UvPoly/UPFan.lean +++ b/Poly/UvPoly/UPFan.lean @@ -8,7 +8,7 @@ import Poly.UvPoly.Basic noncomputable section namespace CategoryTheory.UvPoly -open Limits PartialProduct +open Limits CategoryTheory.UvPoly.PartialProduct universe v u variable {C : Type u} [Category.{v} C] [HasPullbacks C] [HasTerminal C] {E B : C} diff --git a/Poly/UvPoly/UPIso.lean b/Poly/UvPoly/UPIso.lean index 4843fd9..6a7c940 100644 --- a/Poly/UvPoly/UPIso.lean +++ b/Poly/UvPoly/UPIso.lean @@ -9,7 +9,7 @@ import Poly.Bifunctor.Sigma noncomputable section namespace CategoryTheory.UvPoly -open Limits Over ExponentiableMorphism Functor +open Limits Over ExponentiableMorphism CategoryTheory.Functor universe v u variable {C : Type u} [Category.{v} C] [HasPullbacks C] {E B : C} (P : UvPoly E B) @@ -25,13 +25,17 @@ def partProdsOver : Cᵒᵖ ⥤ C ⥤ Type v := @[simp] theorem partProdsOver_obj_map {X Y : C} (Γ : Cᵒᵖ) (f : X ⟶ Y) (x : (P.partProdsOver.obj Γ).obj X) : (P.partProdsOver.obj Γ).map f x = ⟨x.1, x.2 ≫ f⟩ := by - dsimp [partProdsOver] + dsimp +instances [partProdsOver, Functor.Sigma] have : 𝟙 Γ.unop ≫ x.1 = x.1 := by simp ext : 1 . simp . dsimp rw! (castMode := .all) [this] simp + change pullback.lift (f := x.1) (g := P.p) (pullback.fst x.1 P.p ≫ 𝟙 _) (pullback.snd x.1 P.p) _ ≫ + x.2 ≫ f = x.2 ≫ f + simp + rfl variable [HasTerminal C] @@ -73,7 +77,7 @@ def equiv (Γ X : C) : (Γ ⟶ P.functor.obj X) ≃ (b : Γ ⟶ B) × (pullback theorem equiv_app (Γ X : C) (be : Γ ⟶ P.functor.obj X) : P.equiv Γ X be = (P.iso_Sigma.hom.app <| .op Γ).app X be := by - dsimp [equiv] + rfl lemma equiv_naturality_left {Δ Γ : C} (σ : Δ ⟶ Γ) (X : C) (be : Γ ⟶ P.functor.obj X) : P.equiv Δ X (σ ≫ be) = @@ -82,6 +86,7 @@ lemma equiv_naturality_left {Δ Γ : C} (σ : Δ ⟶ Γ) (X : C) (be : Γ ⟶ P. (Category.assoc (obj := C) .. ▸ pullback.condition) ≫ p.2⟩ := by conv_lhs => rw [equiv_app, coyoneda.comp₂_naturality₂_left, ← equiv_app] simp + rfl -- NOTE(WN): As of Lean 4.25, kernel typechecking time is down to 1s from 10s?! lemma equiv_naturality_right {Γ X Y : C} (be : Γ ⟶ P.functor.obj X) (f : X ⟶ Y) : @@ -89,6 +94,6 @@ lemma equiv_naturality_right {Γ X Y : C} (be : Γ ⟶ P.functor.obj X) (f : X let p := equiv P Γ X be ⟨p.1, p.2 ≫ f⟩ := by conv_lhs => rw [equiv_app, coyoneda.comp₂_naturality₂_right, ← equiv_app] - simp + exact P.partProdsOver_obj_map (.op Γ) f (P.equiv Γ X be) end CategoryTheory.UvPoly diff --git a/Poly/Widget/CommDiag.lean b/Poly/Widget/CommDiag.lean index cbb13bf..aca4512 100644 --- a/Poly/Widget/CommDiag.lean +++ b/Poly/Widget/CommDiag.lean @@ -3,9 +3,10 @@ Copyright (c) 2024 Wojciech Nawrocki. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Wojciech Nawrocki -/ -import ProofWidgets.Component.GraphDisplay +import ProofWidgets.Component.ForceGraphDisplay import ProofWidgets.Component.Panel.SelectionPanel import ProofWidgets.Component.Panel.GoalTypePanel +import ProofWidgets.Presentation.Expr import Mathlib.CategoryTheory.Category.Basic /-! ## Definitions copied from Mathlib.Tactic.Widget.CommDiag @@ -70,9 +71,9 @@ where go (f : Expr) : MetaM (List (Expr × Expr)) := do structure DiagState where /-- vertex id ↦ object -/ - vertices: Std.HashMap Nat Expr := .empty + vertices: Std.HashMap Nat Expr := {} /-- morphism `f` ↦ (src, tgt) for every occurrence of `f` -/ - edges: Std.HashMap Expr (List (Nat × Nat)) := .empty + edges: Std.HashMap Expr (List (Nat × Nat)) := {} freshVertId : Nat := 0 variable {m : Type → Type} [Monad m] [MonadStateOf DiagState m] @@ -144,7 +145,7 @@ def addEq [MonadLift MetaM m] (eq : Expr) : m Unit := do open Jsx in def mkLabel (e : Expr) : MetaM (Nat × Nat × Html) := do - let fmt ← withOptions (·.setNat `pp.deepTerms.threshold 1) + let fmt ← withOptions (·.set `pp.deepTerms.threshold (1 : Nat)) (toString <$> ppExpr e) let w := min (15 + fmt.length * 6) 100 let h := max 20 (20 * (1 + fmt.length / 15)) @@ -194,7 +195,7 @@ def toHtml [MonadLift MetaM m] : m Html := do
} - return { module }) + -- see comments in https://github.com/leanprover/lean4/pull/6325 + enableInitializersExecution + let env ← Lean.importModules imports {} + let mut ok := true + for line in ← IO.FS.lines filename do + unless env.contains line.toName do + println! "{line} is missing." + ok := false + return if ok then 0 else 1 diff --git a/vendor/checkdecls/UPSTREAM.md b/vendor/checkdecls/UPSTREAM.md new file mode 100644 index 0000000..4c6e162 --- /dev/null +++ b/vendor/checkdecls/UPSTREAM.md @@ -0,0 +1,27 @@ +# checkdecls provenance and Lean migration + +Vendored from https://github.com/PatrickMassot/checkdecls at commit +`3d425859e73fcfbef85b9638c2a91708ef4a22d4` (tag `lean4.18.0`, upstream +`master` as observed on 2026-10-10). Upstream had no Lean v4.34.1 release or +branch. The original Apache-2.0 license is retained in `LICENSE`. + +Changes made for Poly's Lean v4.34.1 migration: + +- Updated `lean-toolchain` from `leanprover/lean4:v4.18.0` to + `leanprover/lean4:v4.34.1`. +- Ran `lake update`; Lake rewrote the empty manifest to schema 1.2.0 and + added `fixedToolchain: false`. This package has no dependency repositories. +- No edits to `Main.lean` or `lakefile.lean` were required. + +Verification on 2026-10-10 with Lean v4.34.1 on Linux: + +- Standalone `lake update`: exit 0. +- Standalone `lake build`: exit 0, 4 jobs, no warnings. +- Executable smoke test in a separate tiny Lean package: an imported, existing + declaration returned 0; an absent declaration returned 1 with its name; + a nonexistent declaration-list file returned 1; no arguments returned 1. + +The dependency is stored as ordinary source files, rather than an embedded Git +repository, so Poly's relative `vendor/checkdecls` path dependency is portable. +The migration logs and original-revision bundle are held in Poly's local +`.bump-v4.34.1` evidence directory. diff --git a/vendor/checkdecls/lake-manifest.json b/vendor/checkdecls/lake-manifest.json new file mode 100644 index 0000000..2f2af5a --- /dev/null +++ b/vendor/checkdecls/lake-manifest.json @@ -0,0 +1,6 @@ +{"version": "1.2.0", + "packagesDir": ".lake/packages", + "packages": [], + "name": "checkdecls", + "lakeDir": ".lake", + "fixedToolchain": false} diff --git a/vendor/checkdecls/lakefile.lean b/vendor/checkdecls/lakefile.lean new file mode 100644 index 0000000..e28ea0a --- /dev/null +++ b/vendor/checkdecls/lakefile.lean @@ -0,0 +1,13 @@ +import Lake +open Lake DSL + +package «checkdecls» { + -- add package configuration options here +} + +@[default_target] +lean_exe «checkdecls» { + root := `Main + supportInterpreter := true + weakLinkArgs := #["-lLake"] +} diff --git a/vendor/checkdecls/lean-toolchain b/vendor/checkdecls/lean-toolchain new file mode 100644 index 0000000..ba8ebf2 --- /dev/null +++ b/vendor/checkdecls/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.34.1 From 54168183a3a6ded4171a7bb60d60e2ef7548a3d2 Mon Sep 17 00:00:00 2001 From: openhands Date: Sun, 11 Oct 2026 06:44:13 -0400 Subject: [PATCH 02/11] UNITY: merge chunk Poly/MvPoly/Basic.lean:idApplyIso --- Poly/MvPoly/Basic.lean | 20 +++++++------------- 1 file changed, 7 insertions(+), 13 deletions(-) diff --git a/Poly/MvPoly/Basic.lean b/Poly/MvPoly/Basic.lean index 6d17554..46badde 100644 --- a/Poly/MvPoly/Basic.lean +++ b/Poly/MvPoly/Basic.lean @@ -104,19 +104,13 @@ def apply {I O : C} (P : MvPoly I O) [ExponentiableMorphism P.p] : Over I → Ov /-TODO: write a coercion from `MvPoly` to a functor for evaluation of polynomials at a given object.-/ -def idApplyIso (q : X ⟶ I) : (id I).apply (Over.mk q) ≅ Over.mk q where - hom := by - simp [apply] - exact { - left := by - dsimp - sorry - right := sorry - w := sorry - } - inv := sorry - hom_inv_id := sorry - inv_hom_id := sorry +/-- Evaluating the identity polynomial returns the input slice object. +The isomorphism composes the identity isomorphisms for pullback, pushforward, and map. -/ +def idApplyIso (q : X ⟶ I) : (id I).apply (Over.mk q) ≅ Over.mk q := + (Over.map (𝟙 I)).mapIso + ((pushforward (𝟙 I)).mapIso (Over.pullbackId.app (Over.mk q)) ≪≫ + (pushforwardIdIso I).app (Over.mk q)) ≪≫ + (Over.mapId I).app (Over.mk q) section Composition From 3ff0153781b3c53a905fa414581595354bd09c16 Mon Sep 17 00:00:00 2001 From: openhands Date: Sun, 11 Oct 2026 07:01:53 -0400 Subject: [PATCH 03/11] UNITY: merge chunk Poly/MvPoly/Basic.lean:prod --- .../LocallyCartesianClosed/Extensive.lean | 147 ++++++++++++++++++ Poly/MvPoly/Basic.lean | 24 ++- 2 files changed, 170 insertions(+), 1 deletion(-) create mode 100644 Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Extensive.lean diff --git a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Extensive.lean b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Extensive.lean new file mode 100644 index 0000000..22f6a20 --- /dev/null +++ b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Extensive.lean @@ -0,0 +1,147 @@ +import Mathlib.CategoryTheory.Extensive +import Mathlib.CategoryTheory.Comma.Over.Pullback +import Mathlib.CategoryTheory.Limits.Constructions.Over.Basic +import Mathlib.CategoryTheory.Adjunction.PartialAdjoint + +open CategoryTheory CategoryTheory.Limits + +noncomputable section + +namespace CategoryTheory + +universe u v + +section General + +variable {C : Type*} [Category* C] {D : Type*} [Category* D] + {D₁ : Type*} [Category* D₁] {D₂ : Type*} [Category* D₂] + +/-- If `E₁, E₂` are jointly fully faithful and `L ⋙ E₁`, `L ⋙ E₂` are left adjoints +(and the source has binary products), then `L` is a left adjoint: its right adjoint +sends `Y` to `R₁ (E₁ Y) ⨯ R₂ (E₂ Y)`. -/ +theorem isLeftAdjoint_of_jointly_fullyFaithful [HasBinaryProducts C] + (L : C ⥤ D) (E₁ : D ⥤ D₁) (E₂ : D ⥤ D₂) + (hE : ∀ {Y Y' : D}, Function.Bijective (fun φ : Y ⟶ Y' => (E₁.map φ, E₂.map φ))) + [(L ⋙ E₁).IsLeftAdjoint] [(L ⋙ E₂).IsLeftAdjoint] : L.IsLeftAdjoint := by + apply Functor.isLeftAdjoint_of_rightAdjointObjIsDefined_eq_top + ext Y + simp only [Pi.top_apply, Prop.top_eq_true, iff_true] + rw [Functor.rightAdjointObjIsDefined_iff] + let adj₁ := Adjunction.ofIsLeftAdjoint (L ⋙ E₁) + let adj₂ := Adjunction.ofIsLeftAdjoint (L ⋙ E₂) + let e : ∀ X : C, (L.obj X ⟶ Y) ≃ (E₁.obj (L.obj X) ⟶ E₁.obj Y) × (E₂.obj (L.obj X) ⟶ E₂.obj Y) := + fun _ => Equiv.ofBijective _ hE + have key : ∀ (X : C) (a : E₁.obj (L.obj X) ⟶ E₁.obj Y) (b : E₂.obj (L.obj X) ⟶ E₂.obj Y), + E₁.map ((e X).symm (a, b)) = a ∧ E₂.map ((e X).symm (a, b)) = b := + fun X a b => Prod.mk.inj ((e X).apply_symm_apply (a, b)) + refine Functor.RepresentableBy.isRepresentable (Y := + (Functor.rightAdjoint (L ⋙ E₁)).obj (E₁.obj Y) ⨯ + (Functor.rightAdjoint (L ⋙ E₂)).obj (E₂.obj Y)) + { homEquiv := fun {X} => + { toFun := fun u => (e X).symm + ((adj₁.homEquiv _ _).symm (u ≫ prod.fst), (adj₂.homEquiv _ _).symm (u ≫ prod.snd)) + invFun := fun φ => prod.lift (adj₁.homEquiv _ _ (E₁.map φ)) + (adj₂.homEquiv _ _ (E₂.map φ)) + left_inv := fun u => by + apply prod.hom_ext + · rw [prod.lift_fst, (key _ _ _).1, Equiv.apply_symm_apply] + · rw [prod.lift_snd, (key _ _ _).2, Equiv.apply_symm_apply] + right_inv := fun φ => by + apply (e X).injective + refine Prod.ext ?_ ?_ + · change E₁.map _ = E₁.map φ + rw [(key _ _ _).1, prod.lift_fst, Equiv.symm_apply_apply] + · change E₂.map _ = E₂.map φ + rw [(key _ _ _).2, prod.lift_snd, Equiv.symm_apply_apply] } + homEquiv_comp := fun {X X'} f u => by + apply (e X).injective + refine Prod.ext ?_ ?_ + · change E₁.map _ = E₁.map (L.map f ≫ _) + dsimp only [Equiv.coe_fn_mk] + rw [(key _ _ _).1, Functor.map_comp, (key _ _ _).1, Category.assoc] + exact adj₁.homEquiv_naturality_left_symm f _ + · change E₂.map _ = E₂.map (L.map f ≫ _) + dsimp only [Equiv.coe_fn_mk] + rw [(key _ _ _).2, Functor.map_comp, (key _ _ _).2, Category.assoc] + exact adj₂.homEquiv_naturality_left_symm f _ } + +end General + +section Extensive + +variable {C : Type u} [Category.{v} C] [HasFiniteLimits C] [FinitaryExtensive C] + +/-- In an extensive category, an object over `A ⨿ B` is the coproduct of its pullbacks +along the two coprojections. -/ +def isColimitPullbackCoprodInlInr {A B : C} (Y : Over (A ⨿ B)) : + IsColimit (BinaryCofan.mk (pullback.fst Y.hom (coprod.inl : A ⟶ A ⨿ B)) + (pullback.fst Y.hom (coprod.inr : B ⟶ A ⨿ B))) := + (((BinaryCofan.isVanKampen_iff _).mp + (FinitaryExtensive.van_kampen' _ (coprodIsCoprod A B)) + (BinaryCofan.mk (pullback.fst Y.hom (coprod.inl : A ⟶ A ⨿ B)) + (pullback.fst Y.hom (coprod.inr : B ⟶ A ⨿ B))) + (pullback.snd _ _) (pullback.snd _ _) Y.hom pullback.condition.symm + pullback.condition.symm).mpr + ⟨IsPullback.of_hasPullback _ _, IsPullback.of_hasPullback _ _⟩).some + +omit [HasFiniteLimits C] in +/-- Pulling back along the two coprojections is jointly fully faithful. -/ +theorem pullback_inl_inr_bijective {A B : C} {Y Y' : Over (A ⨿ B)} : + Function.Bijective (fun φ : Y ⟶ Y' => + ((Over.pullback (coprod.inl : A ⟶ A ⨿ B)).map φ, + (Over.pullback (coprod.inr : B ⟶ A ⨿ B)).map φ)) := by + have hc := isColimitPullbackCoprodInlInr Y + constructor + · intro φ ψ h + obtain ⟨h₁, h₂⟩ := Prod.mk.inj h + ext + apply BinaryCofan.IsColimit.hom_ext hc + · have := congrArg (fun χ => χ.left ≫ pullback.fst _ _) h₁ + simpa [pullback.lift_fst, pullback.lift_snd] using this + · have := congrArg (fun χ => χ.left ≫ pullback.fst _ _) h₂ + simpa [pullback.lift_fst, pullback.lift_snd] using this + · rintro ⟨a, b⟩ + obtain ⟨l, hl₁, hl₂⟩ := BinaryCofan.IsColimit.desc' hc + (a.left ≫ pullback.fst _ _) (b.left ≫ pullback.fst _ _) + have hw : l ≫ Y'.hom = Y.hom := by + apply BinaryCofan.IsColimit.hom_ext hc + · have ha := Over.w a + simp only [Over.pullback_obj_left, Over.pullback_obj_hom] at ha + simp only [BinaryCofan.mk_inl] at hl₁ ⊢ + rw [reassoc_of% hl₁, pullback.condition, ← Category.assoc, ha, + pullback.condition] + · have hb := Over.w b + simp only [Over.pullback_obj_left, Over.pullback_obj_hom] at hb + simp only [BinaryCofan.mk_inr] at hl₂ ⊢ + rw [reassoc_of% hl₂, pullback.condition, ← Category.assoc, hb, + pullback.condition] + refine ⟨Over.homMk l hw, Prod.ext ?_ ?_⟩ + · ext + apply pullback.hom_ext + · simpa [pullback.lift_fst, pullback.lift_snd] using hl₁ + · simpa [pullback.lift_fst, pullback.lift_snd] using (Over.w a).symm + · ext + apply pullback.hom_ext + · simpa [pullback.lift_fst, pullback.lift_snd] using hl₂ + · simpa [pullback.lift_fst, pullback.lift_snd] using (Over.w b).symm + +end Extensive + +/-- In a finitary extensive category with finite limits, if `f : A ⟶ S` and `g : B ⟶ S` +are exponentiable (pullback along them has a right adjoint), then so is +`coprod.desc f g : A ⨿ B ⟶ S`. -/ +theorem coprod_desc_exponentiable {C : Type u} [Category.{v} C] [HasFiniteLimits C] + [FinitaryExtensive C] {A B S : C} (f : A ⟶ S) (g : B ⟶ S) + [Functor.IsLeftAdjoint (Over.pullback f)] [Functor.IsLeftAdjoint (Over.pullback g)] : + Functor.IsLeftAdjoint (Over.pullback (coprod.desc f g)) := by + have h₁' : (Over.pullback (coprod.inl ≫ coprod.desc f g)).IsLeftAdjoint := by + simp only [coprod.inl_desc]; infer_instance + have h₂' : (Over.pullback (coprod.inr ≫ coprod.desc f g)).IsLeftAdjoint := by + simp only [coprod.inr_desc]; infer_instance + have h₁ : (Over.pullback (coprod.desc f g) ⋙ Over.pullback coprod.inl).IsLeftAdjoint := + Functor.isLeftAdjoint_of_iso (Over.pullbackComp _ _) + have h₂ : (Over.pullback (coprod.desc f g) ⋙ Over.pullback coprod.inr).IsLeftAdjoint := + Functor.isLeftAdjoint_of_iso (Over.pullbackComp _ _) + exact isLeftAdjoint_of_jointly_fullyFaithful _ _ _ pullback_inl_inr_bijective + +end CategoryTheory diff --git a/Poly/MvPoly/Basic.lean b/Poly/MvPoly/Basic.lean index 46badde..a5b340e 100644 --- a/Poly/MvPoly/Basic.lean +++ b/Poly/MvPoly/Basic.lean @@ -12,6 +12,8 @@ import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.Basic import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.BeckChevalley import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.Distributivity import Mathlib.CategoryTheory.Extensive +import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.Extensive +import Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers --import Poly.UvPoly /-! @@ -90,7 +92,27 @@ def prod {I O : C} [HasBinaryProducts C] [FinitaryExtensive C] (P Q : MvPoly I O B := pullback P.o Q.o i := coprod.desc (pullback.fst _ _ ≫ P.i) (pullback.snd _ _ ≫ Q.i) p := coprod.desc (pullback.map _ _ _ _ P.p (𝟙 _) (𝟙 _) (by aesop) (by aesop)) (pullback.map _ _ _ _ (𝟙 _) Q.p (𝟙 _) (by aesop) (by aesop)) - exp := sorry -- by extensivity -- PreservesPullbacksOfInclusions + exp := by + letI : HasFiniteLimits C := hasFiniteLimits_of_hasTerminal_and_pullbacks + haveI : ExponentiableMorphism P.p := P.exp + haveI : ExponentiableMorphism Q.p := Q.exp + haveI : ExponentiableMorphism + (pullback.map (P.p ≫ P.o) Q.o P.o Q.o P.p (𝟙 _) (𝟙 _) (by aesop) (by aesop)) := by + apply ExponentiableMorphism.of_isPullback (snd := pullback.fst _ _) + (f := pullback.fst _ _) (g := P.p) + apply IsPullback.of_right (t := (IsPullback.of_hasPullback P.o Q.o).flip) + · simpa [pullback.map, pullback.lift_snd] using + (IsPullback.of_hasPullback (P.p ≫ P.o) Q.o).flip + · simp [pullback.map, pullback.lift_fst] + haveI : ExponentiableMorphism + (pullback.map P.o (Q.p ≫ Q.o) P.o Q.o (𝟙 _) Q.p (𝟙 _) (by aesop) (by aesop)) := by + apply ExponentiableMorphism.of_isPullback (snd := pullback.snd _ _) + (f := pullback.snd _ _) (g := Q.p) + apply IsPullback.of_right (t := IsPullback.of_hasPullback P.o Q.o) + · simpa [pullback.map, pullback.lift_fst] using + IsPullback.of_hasPullback P.o (Q.p ≫ Q.o) + · simp [pullback.map, pullback.lift_snd] + exact coprod_desc_exponentiable _ _ o := pullback.fst (P.o) Q.o ≫ P.o protected def functor {I O : C} (P : MvPoly I O) : From e5297a8cdb4e2e8dbfdf404d2bf358d400aac78c Mon Sep 17 00:00:00 2001 From: openhands Date: Sun, 11 Oct 2026 07:03:22 -0400 Subject: [PATCH 04/11] UNITY: merge chunk Poly/UvPoly/Basic.lean:idApplyIso --- Poly/UvPoly/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Poly/UvPoly/Basic.lean b/Poly/UvPoly/Basic.lean index df28252..37989d3 100644 --- a/Poly/UvPoly/Basic.lean +++ b/Poly/UvPoly/Basic.lean @@ -98,7 +98,7 @@ def idIso : (UvPoly.id B).functor ≅ star B ⋙ Over.forget B := isoWhiskerRight (isoWhiskerLeft _ (pushforwardIdIso B)) (Over.forget B) /-- Evaluating the identity polynomial at an object `X` is isomorphic to `B × X`. -/ -def idApplyIso (X : C) : (id B) @ X ≅ B ⨯ X := sorry +def idApplyIso (X : C) : (id B) @ X ≅ B ⨯ X := (idIso B).app X variable {B} From 9b15d267025e5a975085823e8016acdb6f7849a3 Mon Sep 17 00:00:00 2001 From: openhands Date: Sun, 11 Oct 2026 08:28:54 -0400 Subject: [PATCH 05/11] UNITY: merge chunk Poly/ForMathlib/CategoryTheory/PartialProduct.lean:Fan.ext --- .../CategoryTheory/PartialProduct.lean | 16 ++++++++++++++-- 1 file changed, 14 insertions(+), 2 deletions(-) diff --git a/Poly/ForMathlib/CategoryTheory/PartialProduct.lean b/Poly/ForMathlib/CategoryTheory/PartialProduct.lean index 7a2a2ac..37d203f 100644 --- a/Poly/ForMathlib/CategoryTheory/PartialProduct.lean +++ b/Poly/ForMathlib/CategoryTheory/PartialProduct.lean @@ -121,14 +121,26 @@ instance : Category (Fan s X) where comp_id f := by dsimp; ext; simp assoc f g h := by dsimp; ext; simp +namespace Fan + /-- Constructs an isomorphism of `PartialProduct.Fan`s out of an isomorphism of the apexes that commutes with the projections. -/ -def Fan.ext {c c' : Fan s X} (e : c.pt ≅ c'.pt) +def ext {c c' : Fan s X} (e : c.pt ≅ c'.pt) (h₁ : e.hom ≫ c'.fst = c.fst) (h₂ : pullbackMap e.hom ≫ c'.snd = c.snd) : c ≅ c' where hom := ⟨e.hom, h₁, h₂⟩ - inv := ⟨e.inv, by simp [Iso.inv_comp_eq, h₁] , by sorry⟩ + inv := ⟨e.inv, by simp [Iso.inv_comp_eq, h₁] , by + rw [← h₂, ← Category.assoc] + have hi : e.inv ≫ c.fst = c'.fst := by simp [Iso.inv_comp_eq, h₁] + have h : pullbackMap e.inv hi ≫ pullbackMap e.hom h₁ = 𝟙 _ := by + ext <;> simp [pullbackMap, pullback.lift_fst, pullback.lift_snd, + pullback.lift_fst_assoc, Category.assoc] + rw [h, Category.id_comp]⟩ + hom_inv_id := by apply Fan.Hom.ext; exact e.hom_inv_id + inv_hom_id := by apply Fan.Hom.ext; exact e.inv_hom_id + +end Fan structure IsLimit (cone : Fan s X) where /-- There is a morphism from any cone apex to `cone.pt` -/ From 87b103d9715fe950ee294a3bb3a135ade23f1d44 Mon Sep 17 00:00:00 2001 From: openhands Date: Sun, 11 Oct 2026 08:31:51 -0400 Subject: [PATCH 06/11] UNITY: merge chunk Poly/UvPoly/Basic.lean:smul --- Poly/UvPoly/Basic.lean | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/Poly/UvPoly/Basic.lean b/Poly/UvPoly/Basic.lean index 37989d3..0350635 100644 --- a/Poly/UvPoly/Basic.lean +++ b/Poly/UvPoly/Basic.lean @@ -64,7 +64,22 @@ variable {E B : C} def const [HasInitial C] (S : C) : UvPoly (⊥_ C) S := ⟨initial.to S, sorry⟩ def smul (S : C) (P : UvPoly E B) : UvPoly (S ⨯ E) (S ⨯ B) := - ⟨prod.map (𝟙 S) P.p, sorry⟩ + ⟨prod.map (𝟙 S) P.p, by + exact ExponentiableMorphism.of_isPullback + (show IsPullback (prod.map (𝟙 S) P.p) prod.snd prod.snd P.p from { + isLimit' := ⟨PullbackCone.isLimitAux' _ (fun t ↦ by + refine ⟨prod.lift (t.fst ≫ prod.fst) t.snd, ?_, ?_, ?_⟩ + · change prod.lift (t.fst ≫ prod.fst) t.snd ≫ prod.map (𝟙 S) P.p = t.fst + ext <;> simp [PullbackCone.condition] + · change prod.lift (t.fst ≫ prod.fst) t.snd ≫ prod.snd = t.snd + simp + · intro m h₁ h₂ + dsimp only [PullbackCone.mk] at m h₁ h₂ ⊢ + change m ≫ prod.map (𝟙 S) P.p = t.fst at h₁ + change m ≫ prod.snd = t.snd at h₂ + apply prod.hom_ext + · simpa using congrArg (fun k ↦ k ≫ prod.fst) h₁ + · simpa using h₂)⟩ })⟩ /-- The product of two polynomials in a single variable. -/ def prod {E' B'} (P : UvPoly E B) (Q : UvPoly E' B') [HasBinaryCoproducts C] : From e89e93061e75a73d94ad33c6849518c7454c82c5 Mon Sep 17 00:00:00 2001 From: openhands Date: Sun, 11 Oct 2026 08:36:03 -0400 Subject: [PATCH 07/11] UNITY: merge chunk sumEquiv --- Poly/Type/Univariate.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Poly/Type/Univariate.lean b/Poly/Type/Univariate.lean index 89fa2aa..d68b1e3 100644 --- a/Poly/Type/Univariate.lean +++ b/Poly/Type/Univariate.lean @@ -149,7 +149,8 @@ def sumEquiv : (P.sum Q) X ≃ P X ⊕ Q X where | Sum.inl ⟨b, x⟩ => ⟨Sum.inl b, x⟩ | Sum.inr ⟨b, x⟩ => ⟨Sum.inr b, x⟩ left_inv := by - sorry + rintro ⟨b, x⟩ + cases b <;> rfl right_inv := by aesop_cat From 1486040c7ea0035aa88087cfbffb28dfab302e98 Mon Sep 17 00:00:00 2001 From: openhands Date: Sun, 11 Oct 2026 09:51:28 -0400 Subject: [PATCH 08/11] UNITY: merge chunk equiv --- Poly/UvPoly/UPFan.lean | 31 ++++++++++++++++++++++--------- 1 file changed, 22 insertions(+), 9 deletions(-) diff --git a/Poly/UvPoly/UPFan.lean b/Poly/UvPoly/UPFan.lean index cf9c656..628263d 100644 --- a/Poly/UvPoly/UPFan.lean +++ b/Poly/UvPoly/UPFan.lean @@ -13,22 +13,35 @@ open Limits CategoryTheory.UvPoly.PartialProduct universe v u variable {C : Type u} [Category.{v} C] [HasPullbacks C] [HasTerminal C] {E B : C} -/-- Universal property of the polynomial functor. -/ +/-- Universal property of the polynomial functor. The inverse laws follow from +partial-product hom extensionality and the two lift projection identities. -/ @[simps] def equiv (P : UvPoly E B) (Γ : C) (X : C) : (Γ ⟶ P @ X) ≃ (b : Γ ⟶ B) × (pullback b P.p ⟶ X) where toFun := P.proj invFun u := P.lift (Γ := Γ) (X := X) u.1 u.2 left_inv f := by - dsimp - symm - fapply partialProd.hom_ext ⟨fan P X, isLimitFan P X⟩ - · simp; rfl - · sorry + refine P.hom_ext ?_ ?_ + · exact lift_fst (P := P) (b := (P.proj f).1) (e := (P.proj f).2) + · change PartialProduct.comparison (P.lift (P.proj f).1 (P.proj f).2) ≫ + (fan P X).snd = _ + rw [lift_snd] + congr 1 + exact (proj_snd (P := P)).trans + (congrArg (fun k => k ≫ (fan P X).snd) + (PartialProduct.comparison_pullback.map (c := fan P X) (f := f)).symm) right_inv := by intro ⟨b, e⟩ - ext - · simp only [proj_fst, lift_fst] - · sorry + apply Sigma.ext (lift_fst (P := P)) + have w := lift_snd (P := P) (b := b) (e := e) + rw [PartialProduct.comparison_pullback.map] at w + change (P.proj (P.lift b e)).2 = _ at w + have transport {b' b : Γ ⟶ B} (h : b' = b) + (e' : pullback b' P.p ⟶ X) (e : pullback b P.p ⟶ X) + (w : e' = (pullback.congrHom h rfl).hom ≫ e) : HEq e' e := by + cases h + apply heq_of_eq + simpa [pullback.congrHom] using w + exact transport (lift_fst (P := P)) _ _ w end CategoryTheory.UvPoly From cc08a1f77c20e07a7366f0824ecd36ae472c0377 Mon Sep 17 00:00:00 2001 From: openhands Date: Sun, 11 Oct 2026 13:58:39 -0400 Subject: [PATCH 09/11] docs: mark proofs completed by Unity --- README.md | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index 9223e2d..8962228 100644 --- a/README.md +++ b/README.md @@ -18,27 +18,33 @@ As part of this formalization, we also formalize locally cartesian closed catego - [x] The Beck-Chevalley condition in LCCC - [x] LCCC structure on types - [x] LCCC structure on presheaves of types + - [x] Isomorphisms of partial-product fans (`PartialProduct.Fan.ext`) (by Unity) - [ ] Univariate Polynomial Functors - [x] Definition of univariate polynomial functors - [x] The construction of associated polynomial functors + - [x] Identity-polynomial evaluation `(id B) @ X ≅ B × X` (`UvPoly.idApplyIso`) (by Unity) - [x] Monomials - [x] Linear polynomials + - [x] Scalar multiplication preserves exponentiability (`UvPoly.smul`) (by Unity) - [x] Sums of polynomials + - [x] Evaluation-of-sums equivalence (`Poly.sumEquiv`) (by Unity) - [ ] Products of polynomials - [x] Composition of polynomials - [x] The classifying property of polynomial functors + - [x] Universal-property equivalence inverse laws (`UvPoly.equiv`) (by Unity) - [x] The monoidal category `C [X]` of univariate polynomial functors - [ ] Cartesian closedness of a category of polynomial functors - [ ] Multivariate Polynomial Functors - [x] Definition of multivariate polynomial functors - [x] The construction of associated polynomial functors + - [x] Identity-polynomial evaluation in the slice (`MvPoly.idApplyIso`) (by Unity) - [x] Monomials - [x] Linear polynomials - [ ] Symmetric polynomials - [ ] Sums of polynomials - - [ ] Products of polynomials + - [x] Products of polynomials: construction and exponentiability (`MvPoly.prod`) (by Unity) - [x] Composition of polynomials - [ ] The classifying property of polynomial functors - [ ] The bicategory of multivariate polynomial functors From ba73d5149ac19b1186b6e58648217b52db6b8cdb Mon Sep 17 00:00:00 2001 From: shiv <33400784+sosudo@users.noreply.github.com> Date: Mon, 2 Nov 2026 02:04:41 -0500 Subject: [PATCH 10/11] Clean up Poly sources and documentation for upstream --- .../LocallyCartesianClosed/BeckChevalley.lean | 6 ++- .../Distributivity.lean | 2 +- .../LocallyCartesianClosed/Extensive.lean | 15 ++++++ Poly/MvPoly/Basic.lean | 25 ++++++---- Poly/Type/Univariate.lean | 6 ++- Poly/UvPoly/Basic.lean | 9 ++-- Poly/UvPoly/UPIso.lean | 3 +- Poly/deprecated/Basic.lean | 3 +- Poly/deprecated/Exponentiable.lean | 27 +++++++---- Poly/deprecated/ForMathlib.lean | 3 +- Poly/deprecated/LCCC.lean | 6 ++- Poly/deprecated/LCCC/Basic.lean | 24 ++++++---- Poly/deprecated/LCCC/BeckChevalley.lean | 3 +- Poly/deprecated/LCCC/Presheaf.lean | 41 +++++++++++------ Poly/deprecated/LCCC/Presheaf_test.lean | 46 +++++++++++++------ Poly/deprecated/LawvereTheory.lean | 3 +- README.md | 26 ++++++----- vendor/checkdecls/UPSTREAM.md | 2 - 18 files changed, 169 insertions(+), 81 deletions(-) diff --git a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/BeckChevalley.lean b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/BeckChevalley.lean index 1b06775..b3d3a30 100644 --- a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/BeckChevalley.lean +++ b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/BeckChevalley.lean @@ -312,11 +312,13 @@ theorem mapPullbackAdj.counit_app_left : @[simp] theorem pullbackMapTwoSquare_app : (pullbackMapTwoSquare h f g k sq).app A = - Over.homMk (pullback.map _ _ (A.hom ≫ k) _ _ h k (id_comp _).symm sq.w.symm) (by simp [pullback.map, pullback.lift_snd]) := by + Over.homMk (pullback.map _ _ (A.hom ≫ k) _ _ h k (id_comp _).symm sq.w.symm) + (by simp [pullback.map, pullback.lift_snd]) := by ext simp only [homMk_left, pullbackMapTwoSquare, mapIsoSquare, mateEquiv_apply] apply pullback.hom_ext <;> - simp [pullback.map, pullback.lift_fst, pullback.lift_snd, pullback.lift_fst_assoc, Category.assoc] + simp [pullback.map, pullback.lift_fst, pullback.lift_snd, pullback.lift_fst_assoc, + Category.assoc] theorem forget_map_pullbackMapTwoSquare : (Over.forget Z).map ((pullbackMapTwoSquare h f g k sq).app A) = diff --git a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean index 8b7ebcb..9a105ad 100644 --- a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean +++ b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean @@ -43,7 +43,7 @@ abbrev v := Pi' f u abbrev P := Limits.pullback f (v f u) -- not really needed -def g := pullback.fst (v f u) f -- (μ_ (Over.mk f) (Over.mk (v f u))).left --pullback.fst (@v _ _ _ _ _ _ _ f u) f +def g := pullback.fst (v f u) f /-- This should not be an instance because it's not usually how we want to construct exponentiable morphisms, we'll usually prove all morphims are exponential uniformly diff --git a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Extensive.lean b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Extensive.lean index 22f6a20..77dbf22 100644 --- a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Extensive.lean +++ b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Extensive.lean @@ -3,6 +3,21 @@ import Mathlib.CategoryTheory.Comma.Over.Pullback import Mathlib.CategoryTheory.Limits.Constructions.Over.Basic import Mathlib.CategoryTheory.Adjunction.PartialAdjoint +/-! +# Exponentiable maps and finite coproducts + +This file proves that pulling back along the coprojections of a binary coproduct is jointly +fully faithful in a finitary extensive category. It follows that a coproduct of exponentiable +maps is exponentiable. + +## Main results + +* `isLeftAdjoint_of_jointly_fullyFaithful`: construct a right adjoint from jointly fully faithful + functors and right adjoints to their composites. +* `pullback_inl_inr_bijective`: pulling back along coprojections is jointly fully faithful. +* `coprod_desc_exponentiable`: a coproduct of exponentiable maps is exponentiable. +-/ + open CategoryTheory CategoryTheory.Limits noncomputable section diff --git a/Poly/MvPoly/Basic.lean b/Poly/MvPoly/Basic.lean index a5b340e..4868d2d 100644 --- a/Poly/MvPoly/Basic.lean +++ b/Poly/MvPoly/Basic.lean @@ -91,7 +91,9 @@ def prod {I O : C} [HasBinaryProducts C] [FinitaryExtensive C] (P Q : MvPoly I O E := (pullback (P.p ≫ P.o) Q.o) ⨿ (pullback P.o (Q.p ≫ Q.o)) B := pullback P.o Q.o i := coprod.desc (pullback.fst _ _ ≫ P.i) (pullback.snd _ _ ≫ Q.i) - p := coprod.desc (pullback.map _ _ _ _ P.p (𝟙 _) (𝟙 _) (by aesop) (by aesop)) (pullback.map _ _ _ _ (𝟙 _) Q.p (𝟙 _) (by aesop) (by aesop)) + p := coprod.desc + (pullback.map _ _ _ _ P.p (𝟙 _) (𝟙 _) (by aesop) (by aesop)) + (pullback.map _ _ _ _ (𝟙 _) Q.p (𝟙 _) (by aesop) (by aesop)) exp := by letI : HasFiniteLimits C := hasFiniteLimits_of_hasTerminal_and_pullbacks haveI : ExponentiableMorphism P.p := P.exp @@ -121,7 +123,8 @@ protected def functor {I O : C} (P : MvPoly I O) : variable (I O : C) (P : MvPoly I O) -def apply {I O : C} (P : MvPoly I O) [ExponentiableMorphism P.p] : Over I → Over O := (P.functor).obj +def apply {I O : C} (P : MvPoly I O) [ExponentiableMorphism P.p] : Over I → Over O := + (P.functor).obj /-TODO: write a coercion from `MvPoly` to a functor for evaluation of polynomials at a given object.-/ @@ -184,7 +187,8 @@ def comp.functor : P.functor ⋙ Q.functor ≅ (P.comp Q).functor := by _ ≅ Over.pullback P.i ⋙ (Over.pullback (P.m Q) ⋙ pushforward (r P Q)) ⋙ (Over.pullback (P.ε Q) ⋙ pushforward (P.q Q) ⋙ Over.map (P.w Q)) ⋙ Over.map Q.o := ?_ (Over.pullback P.i ⋙ (Over.pullback (P.m Q) ⋙ pushforward (r P Q)) ⋙ - (Over.pullback (P.ε Q) ⋙ pushforward (P.q Q) ⋙ Over.map (P.w Q)) ⋙ Over.map Q.o) ≅ _ := ?_ + (Over.pullback (P.ε Q) ⋙ pushforward (P.q Q) ⋙ Over.map (P.w Q)) ⋙ + Over.map Q.o) ≅ _ := ?_ (Over.pullback P.i ⋙ Over.pullback (P.m Q) ⋙ Over.pullback (P.n Q)) ⋙ (pushforward (P.p' Q) ⋙ pushforward (P.q Q)) ⋙ Over.map (P.w Q) ⋙ Over.map Q.o ≅ _ := ?_ (Over.pullback P.i ⋙ Over.pullback (P.m Q) ⋙ Over.pullback (P.n Q)) @@ -194,9 +198,11 @@ def comp.functor : P.functor ⋙ Q.functor ≅ (P.comp Q).functor := by apply Iso.symm letI := pullbackMapTwoSquare_of_isPullback_isIso hA' let this := asIso (pullbackMapTwoSquare (P.k Q) (P.h Q) Q.i P.o hA'.toCommSq) - exact isoWhiskerLeft (Over.pullback P.i) <| isoWhiskerLeft (pushforward P.p) <| isoWhiskerRight this <| _ + exact isoWhiskerLeft (Over.pullback P.i) <| isoWhiskerLeft (pushforward P.p) <| + isoWhiskerRight this <| _ · exact isoWhiskerLeft (Over.pullback P.i) <| isoWhiskerLeft (pushforward P.p) - <| isoWhiskerLeft (Over.pullback (P.h Q)) <| isoWhiskerRight (pentagonIso Q.p (P.k Q)) <| (Over.map Q.o) + <| isoWhiskerLeft (Over.pullback (P.h Q)) + <| isoWhiskerRight (pentagonIso Q.p (P.k Q)) <| (Over.map Q.o) · let hpb := (IsPullback.of_hasPullback P.p (pullback.fst P.o Q.i)) have (hpb : IsPullback (P.m Q) (P.r Q) P.p (P.h Q)) : @@ -206,7 +212,8 @@ def comp.functor : P.functor ⋙ Q.functor ≅ (P.comp Q).functor := by (Over.pullback (P.ε Q) ⋙ pushforward (P.q Q) ⋙ Over.map (P.w Q)) ⋙ Over.map Q.o := by {exact isoWhiskerLeft _ <| isoWhiskerRight (pushforwardPullbackIsoSquare hpb) <| _} exact this hpb - · let hpb : IsPullback (P.n Q) (P.p' Q) (P.r Q) (P.ε Q) := (IsPullback.of_hasPullback (r P Q) (ε P Q)) + · let hpb : IsPullback (P.n Q) (P.p' Q) (P.r Q) (P.ε Q) := + (IsPullback.of_hasPullback (r P Q) (ε P Q)) have (hpb : IsPullback (P.n Q) (P.p' Q) (P.r Q) (P.ε Q)) : Over.pullback P.i ⋙ Over.pullback (P.m Q) ⋙ (pushforward (r P Q) ⋙ Over.pullback (P.ε Q)) ⋙ pushforward (P.q Q) ⋙ Over.map (P.w Q) ⋙ Over.map Q.o ≅ @@ -222,7 +229,8 @@ def comp.functor : P.functor ⋙ Q.functor ≅ (P.comp Q).functor := by Over.pullback P.i ⋙ Over.pullback (P.m Q) ⋙ Over.pullback (P.n Q) := by apply Iso.trans (pullbackComp ((P.n Q) ≫ (P.m Q)) P.i) apply isoWhiskerLeft _ <| (pullbackComp (P.n Q) (P.m Q)) - exact isoWhiskerRight (this).symm ((pushforward (P.p' Q ≫ P.q Q)) ⋙ Over.map (P.w Q) ⋙ Over.map Q.o) + exact isoWhiskerRight (this).symm + ((pushforward (P.p' Q ≫ P.q Q)) ⋙ Over.map (P.w Q) ⋙ Over.map Q.o) simp only [assoc] exact isoWhiskerLeft _ <| isoWhiskerLeft _ (mapComp (P.w Q) Q.o).symm @@ -252,7 +260,8 @@ def auxFunctor (P : UvPoly E B) : Over (⊤_ C) ⥤ Over (⊤_ C) := MvPoly.fun /-- We use the equivalence between `Over (⊤_ C)` and `C` to get `functor : C ⥤ C`. Alternatively we can give a direct definition of `functor` in terms of exponentials. -/ -def functor' (P : UvPoly E B) : C ⥤ C := equivOverTerminal.functor ⋙ P.auxFunctor ⋙ equivOverTerminal.inverse +def functor' (P : UvPoly E B) : C ⥤ C := + equivOverTerminal.functor ⋙ P.auxFunctor ⋙ equivOverTerminal.inverse def functorIsoFunctor' [HasBinaryProducts C] (P : UvPoly E B) : P.functor ≅ P.functor' := by unfold functor' auxFunctor functor MvPoly.functor toMvPoly diff --git a/Poly/Type/Univariate.lean b/Poly/Type/Univariate.lean index d68b1e3..8af638d 100644 --- a/Poly/Type/Univariate.lean +++ b/Poly/Type/Univariate.lean @@ -11,7 +11,8 @@ open CategoryTheory Category Functor /-! # Polynomial functors -We define the notion of one-variable polynomial functors on the category of sets. The locally cartesian closed structure of sets is implicit in all the constructions. +We define the notion of one-variable polynomial functors on the category of sets. The locally +cartesian closed structure of sets is implicit in all the constructions. The bundle corresponding to a `P : Poly` is the projection `fst : Σ b : P.B, P.E b → P.B`. @@ -107,7 +108,8 @@ def bundle : Total P → P.B := Sigma.fst -- TODO: universe issue debugging. /- The bundle of the `sum P Q` is the sum of the bundles. -/ --- theorem sum_bundle_eq : bundle (P.sum Q) = (Sum.map P.bundle Q.bundle) ∘ (sumTotalEquiv P Q) := by +-- theorem sum_bundle_eq : bundle (P.sum Q) = (Sum.map P.bundle Q.bundle) ∘ (sumTotalEquiv P Q) := +-- by -- rfl /-- Applying `P` to an object of `Type` -/ diff --git a/Poly/UvPoly/Basic.lean b/Poly/UvPoly/Basic.lean index 0350635..a3c61e4 100644 --- a/Poly/UvPoly/Basic.lean +++ b/Poly/UvPoly/Basic.lean @@ -322,7 +322,8 @@ def isLimitFan (P : UvPoly E B) (X : C) : PartialProduct.IsLimit (PartialProduct symm 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 + apply (Adjunction.homEquiv_apply_eq (adj P.p) + (overPullbackToStar c.fst c.snd) (Over.homMk m)).mpr simp [overPullbackToStar, PartialProduct.Fan.overPullbackToStar, PartialProduct.Fan.over] apply (Adjunction.homEquiv_apply_eq _ _ _).mpr rw [← h_right] @@ -367,7 +368,8 @@ def proj {Γ X : C} (P : UvPoly E B) (f : Γ ⟶ P @ X) : theorem proj_fst {Γ X : C} {P : UvPoly E B} {f : Γ ⟶ P @ X} : (proj P f).fst = f ≫ P.fstProj X := rfl -/-- The second component of `proj` is a comparison map of pullbacks composed with `ε P X ≫ prod.snd` -/ +/-- The second component of `proj` is a comparison map of pullbacks composed with `ε P X ≫ prod.snd` +-/ -- formerly `polyPair_snd_eq_comp_u₂'` @[simp] theorem proj_snd {Γ X : C} {P : UvPoly E B} {f : Γ ⟶ P @ X} : @@ -390,7 +392,8 @@ def comp exact ExponentiableMorphism.comp (pullback.snd Q.p (fan P A).snd) (pullback.fst (fan P A).fst P.p) -/-- The associated functor of the composition of two polynomials is isomorphic to the composition of the associated functors. -/ +/-- The associated functor of the composition of two polynomials is isomorphic to the composition of +the associated functors. -/ def compFunctorIso {E B D C : C} (P : UvPoly E B) (Q : UvPoly D C) : P.functor ⋙ Q.functor ≅ (comp P Q).functor := by diff --git a/Poly/UvPoly/UPIso.lean b/Poly/UvPoly/UPIso.lean index 6a7c940..97d5a11 100644 --- a/Poly/UvPoly/UPIso.lean +++ b/Poly/UvPoly/UPIso.lean @@ -32,7 +32,8 @@ theorem partProdsOver_obj_map {X Y : C} (Γ : Cᵒᵖ) (f : X ⟶ Y) (x : (P.par . dsimp rw! (castMode := .all) [this] simp - change pullback.lift (f := x.1) (g := P.p) (pullback.fst x.1 P.p ≫ 𝟙 _) (pullback.snd x.1 P.p) _ ≫ + change pullback.lift (f := x.1) (g := P.p) + (pullback.fst x.1 P.p ≫ 𝟙 _) (pullback.snd x.1 P.p) _ ≫ x.2 ≫ f = x.2 ≫ f simp rfl diff --git a/Poly/deprecated/Basic.lean b/Poly/deprecated/Basic.lean index bc69ad1..37c9398 100644 --- a/Poly/deprecated/Basic.lean +++ b/Poly/deprecated/Basic.lean @@ -161,7 +161,8 @@ namespace baseChange open Over MonoidalCategory -/-- For an arrow `f : J ⟶ I` and an object `X : Over I`, the base-change of `X` along `f` is `pullback.snd`. -/ +/-- For an arrow `f : J ⟶ I` and an object `X : Over I`, the base-change of `X` along `f` is +`pullback.snd`. -/ lemma obj_hom_eq_pullback_snd [HasPullbacks C] {I J : C} (f : J ⟶ I) (X : Over I): ((Δ_ f).obj X).hom = pullback.snd X.hom f := rfl diff --git a/Poly/deprecated/Exponentiable.lean b/Poly/deprecated/Exponentiable.lean index 19250cc..065c1d5 100644 --- a/Poly/deprecated/Exponentiable.lean +++ b/Poly/deprecated/Exponentiable.lean @@ -27,7 +27,8 @@ a witness `adj : baseChange f ⊣ functor`. We prove that if a morphism `f : X ⟶ Y` has pushforwards then `f` is exponentiable in the slice category `Over Y`. -In particular, for a morphism `g : X ⟶ I` the exponential `f^* g` is the functor composition `(baseChange g) ⋙ (Over.map g)`. +In particular, for a morphism `g : X ⟶ I` the exponential `f^* g` is the functor composition +`(baseChange g) ⋙ (Over.map g)`. ## Notation @@ -52,7 +53,8 @@ We provide the following notations: Using the notation above, we have * `hom_eq_pullback_snd` proves that `(Δ_ f Over.mk p).hom` is `pullback.snd` -* `natIsoTensorLeft` proves that `Δ_ f` ⋙ `Σ_ f` is isomorphic to the product functor `f × _` in the slice category `Over I`. See +* `natIsoTensorLeft` proves that `Δ_ f` ⋙ `Σ_ f` is isomorphic to the product functor `f × _` in the +slice category `Over I`. See We shall prove that -/ @@ -82,7 +84,8 @@ example (I J X : C) (f : J ⟶ I) (p : X ⟶ I) : exact pullback.fst -/-- For an arrow `f : J ⟶ I` and an object `X : Over I`, the base-change of `X` along `f` is `pullback.snd`. -/ +/-- For an arrow `f : J ⟶ I` and an object `X : Over I`, the base-change of `X` along `f` is +`pullback.snd`. -/ lemma hom_eq_pullback_snd {I J : C} (f : J ⟶ I) (X : Over I): ((Δ_ f).obj X).hom = pullback.snd := rfl @@ -118,7 +121,8 @@ lemma Over.star_eq_Over.mk_prod_fst [HasBinaryProducts C] [HasTerminal C] (I : C (Over.star I).obj X = Over.mk (prod.fst : I ⨯ X ⟶ I) := by simp [Over.star, Over.mk] -/-- The base-change along `terminal.from` ER: Changed statement from an equality to an isomorphism. Proof of commutativity is stuck because of the rewrite. Perhaps I can do this another way? -/ +/-- The base-change along `terminal.from` ER: Changed statement from an equality to an isomorphism. +Proof of commutativity is stuck because of the rewrite. Perhaps I can do this another way? -/ def terminal_from [HasBinaryProducts C] [HasTerminal C] (I : C) (X : Over (⊤_ C)) : (Δ_ (terminal.from I)).obj X ≅ (Over.star I).obj (X.left) := by unfold baseChange Over.star @@ -143,7 +147,8 @@ def terminal_from [HasBinaryProducts C] [HasTerminal C] (I : C) (X : Over (⊤_ -- sorry def isLimitPullbackConeId {I J : C} (f : J ⟶ I) : - IsLimit (PullbackCone.mk (W := J) (fst:= 𝟙 J) (snd := f) (eq:= by simp) : PullbackCone f (𝟙 I)) := by + IsLimit (PullbackCone.mk (W := J) (fst:= 𝟙 J) (snd := f) (eq:= by simp) : + PullbackCone f (𝟙 I)) := by apply PullbackCone.IsLimit.mk · aesop · intro s @@ -171,7 +176,8 @@ def swapIso {X Y : Over I} : @[simp] lemma swap_eq_hom {X Y : Over I} : - ((Σ_ X.hom).obj ((Δ_ X.hom).obj Y)).hom = (pullbackSymmetry _ _).hom ≫ ((Σ_ Y.hom).obj ((Δ_ Y.hom).obj X)).hom := by + ((Σ_ X.hom).obj ((Δ_ X.hom).obj Y)).hom = + (pullbackSymmetry _ _).hom ≫ ((Σ_ Y.hom).obj ((Δ_ Y.hom).obj X)).hom := by simp only [const_obj_obj, id_obj, map_obj_left, baseChange_obj_left, map_obj_hom, baseChange_obj_hom, pullbackSymmetry_hom_comp_snd_assoc] exact pullback.condition.symm @@ -212,7 +218,8 @@ def isBinaryProduct (X Y : Over I) : · apply congr_arg CommaMorphism.left (h ⟨ .right⟩) · apply congr_arg CommaMorphism.left (h ⟨ .left⟩) -/-- The object `(Σ_ X.hom) ((Δ_ X.hom) Y)` is isomorphic to the binary product `X × Y` in the slice category. -/ +/-- The object `(Σ_ X.hom) ((Δ_ X.hom) Y)` is isomorphic to the binary product `X × Y` in the slice +category. -/ @[simps!] def isoProd (X Y : Over I) : (Σ_ X.hom).obj ((Δ_ X.hom).obj Y) ≅ Limits.prod X Y := by @@ -297,12 +304,14 @@ instance comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) adj := ofNatIsoLeft (gexp.adj.comp fexp.adj) (pullbackCompIso f g).symm /-- The conjugate isomorphism between pushforward functors. -/ -def pushforwardCompIso [HasPullbacks C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [fexp : CartesianExponentiable f] [gexp : CartesianExponentiable g] : +def pushforwardCompIso [HasPullbacks C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) + [fexp : CartesianExponentiable f] [gexp : CartesianExponentiable g] : fexp.functor ⋙ gexp.functor ≅ (comp f g).functor := conjugateIsoEquiv (gexp.adj.comp fexp.adj) ((comp f g).adj) (pullbackCompIso f g) /-- An arrow with a pushforward is exponentiable in the slice category. -/ -instance exponentiableOverMk [HasFiniteWidePullbacks C] {I : C} (f : X ⟶ I) [CartesianExponentiable f] : Exponentiable (Over.mk f) where +instance exponentiableOverMk [HasFiniteWidePullbacks C] {I : C} (f : X ⟶ I) + [CartesianExponentiable f] : Exponentiable (Over.mk f) where rightAdj := (Δ_ f) ⋙ (Π_ f) adj := by fapply ofNatIsoLeft diff --git a/Poly/deprecated/ForMathlib.lean b/Poly/deprecated/ForMathlib.lean index 2d4ad53..7a57c6d 100644 --- a/Poly/deprecated/ForMathlib.lean +++ b/Poly/deprecated/ForMathlib.lean @@ -17,7 +17,8 @@ namespace CategoryTheory.Over variable {C : Type*} [Category C] /-- This is useful when `homMk (· ≫ ·)` appears under `Functor.map` or a natural equivalence. -/ -lemma homMk_comp {B : C} {U V W : Over B} (f : U.left ⟶ V.left) (g : V.left ⟶ W.left) (fg_comp f_comp g_comp) : +lemma homMk_comp {B : C} {U V W : Over B} (f : U.left ⟶ V.left) (g : V.left ⟶ W.left) + (fg_comp f_comp g_comp) : homMk (f ≫ g) fg_comp = homMk (V := V) f f_comp ≫ homMk (U := V) g g_comp := by ext; simp diff --git a/Poly/deprecated/LCCC.lean b/Poly/deprecated/LCCC.lean index 2a5b072..fc45bb8 100644 --- a/Poly/deprecated/LCCC.lean +++ b/Poly/deprecated/LCCC.lean @@ -81,7 +81,8 @@ cartesian closed categories. 1. A locally cartesian closed category is a category C such that all the slices C/I are cartesian closed categories. -2. Equivalently, a locally cartesian closed category `C` is a category with pullbacks and terminal object such that each base change functor has a right adjoint, called the pushforward functor. +2. Equivalently, a locally cartesian closed category `C` is a category with pullbacks and terminal +object such that each base change functor has a right adjoint, called the pushforward functor. In this file we prove the equivalence of these conditions. -/ @@ -135,7 +136,8 @@ example [HasFiniteWidePullbacks C] {I : C} : HasFiniteLimits (Over I ) := by inf #check Over.hasFiniteLimits -example [LocallyCartesianClosed C] [HasFiniteWidePullbacks C] : HasFiniteLimits (Over (terminal C)) := by infer_instance +example [LocallyCartesianClosed C] [HasFiniteWidePullbacks C] : + HasFiniteLimits (Over (terminal C)) := by infer_instance #check Adjunction diff --git a/Poly/deprecated/LCCC/Basic.lean b/Poly/deprecated/LCCC/Basic.lean index e88fb28..2b07481 100644 --- a/Poly/deprecated/LCCC/Basic.lean +++ b/Poly/deprecated/LCCC/Basic.lean @@ -71,7 +71,8 @@ variable {C D : Type u} [Category.{v} C] [Category.{v} D] namespace OverBinaryProduct def pullbackCompositionIsBinaryProduct [HasPullbacks C] {I : C} (f x : Over I) : - let pbleg1 : (Over.map f.hom).obj ((Over.pullback f.hom).obj x) ⟶ f := homMk (pullback.snd ..) rfl + let pbleg1 : (Over.map f.hom).obj ((Over.pullback f.hom).obj x) ⟶ f := + homMk (pullback.snd ..) rfl let pbleg2 : (Over.map f.hom).obj ((Over.pullback f.hom).obj x) ⟶ x := Over.homMk (pullback.fst ..) (by simp [pullback.condition]) IsLimit (BinaryFan.mk (pbleg1) (pbleg2)) := by @@ -117,7 +118,8 @@ theorem OverProdIsoRightInv [HasFiniteWidePullbacks C] {I : C} (f x : Over I) : @[simp] theorem Triangle_fst [HasFiniteWidePullbacks C] {I : C} (f x : Over I) : - let pbleg1 : (Over.map f.hom).obj ((Over.pullback f.hom).obj x) ⟶ f := homMk (pullback.snd ..) rfl + let pbleg1 : (Over.map f.hom).obj ((Over.pullback f.hom).obj x) ⟶ f := + homMk (pullback.snd ..) rfl (OverProdIso f x).hom ≫ prod.fst = pbleg1 := IsLimit.conePointUniqueUpToIso_hom_comp (pullbackCompositionIsBinaryProduct f x) (Limits.prodIsProd f x) ⟨ WalkingPair.left⟩ @@ -134,7 +136,8 @@ theorem Triangle_snd [HasFiniteWidePullbacks C] {I : C} @[simp] theorem Triangle.symm_fst [HasFiniteWidePullbacks C] {I : C} (f x : Over I) : - let pbleg1 : (Over.map f.hom).obj ((Over.pullback f.hom).obj x) ⟶ f := homMk (pullback.snd ..) rfl + let pbleg1 : (Over.map f.hom).obj ((Over.pullback f.hom).obj x) ⟶ f := + homMk (pullback.snd ..) rfl (OverProdIso.symm f x).hom ≫ pbleg1 = prod.fst := IsLimit.conePointUniqueUpToIso_hom_comp (Limits.prodIsProd f x) (pullbackCompositionIsBinaryProduct f x) ⟨ WalkingPair.left⟩ @@ -182,7 +185,8 @@ namespace PushforwardAdj instance cartesianClosedOfOver [HasFiniteWidePullbacks C] [PushforwardAdj C] {I : C} : CartesianClosed (Over I) := by - refine .mk _ fun f ↦ .mk f (Over.pullback f.hom ⋙ pushforward f.hom) (ofNatIsoLeft (F := ?functor ) + refine .mk _ fun f ↦ .mk f (Over.pullback f.hom ⋙ pushforward f.hom) + (ofNatIsoLeft (F := ?functor ) ?adj ?iso ) case functor => exact (Over.pullback f.hom ⋙ Over.map f.hom) case adj => exact ((adj f.hom).comp (Over.mapPullbackAdj f.hom)) @@ -269,7 +273,8 @@ def PushforwardObjTo [HasFiniteWidePullbacks C] [OverCC C] rw [CartesianClosed.uncurry_natural_right, CartesianClosed.uncurry_curry] simp have conj : ((Over.map f).map u ≫ (homMk x.hom rfl : (Over.map f).obj x ⟶ Over.mk f)) = - (homMk ((Over.pullback f).obj y).hom : (Over.map f).obj ((Over.pullback f).obj y) ⟶ Over.mk f) := + (homMk ((Over.pullback f).obj y).hom : + (Over.map f).obj ((Over.pullback f).obj y) ⟶ Over.mk f) := OverMorphism.ext (by aesop_cat) exact conj ▸ (Triangle.symm_fst (Over.mk f) y).symm @@ -327,7 +332,8 @@ def pushforwardAdj [HasFiniteWidePullbacks C] [OverCC C] {X Y : C} (f : X ⟶ Y) intro v refine PushforwardObjUP f x y (v ≫ pullback.snd ..) ?commute have w := v ≫= pullback.condition - have lem : (v ≫ pullback.fst ..) = mkIdTerminal.from y := IsTerminal.hom_ext mkIdTerminal _ _ + have lem : (v ≫ pullback.fst ..) = mkIdTerminal.from y := + IsTerminal.hom_ext mkIdTerminal _ _ rw [← lem, assoc, assoc, w] left_inv := by intro u @@ -346,7 +352,8 @@ def pushforwardAdj [HasFiniteWidePullbacks C] [OverCC C] {X Y : C} (f : X ⟶ Y) let w : ((mkIdTerminal (X := Y)).from y) ≫ (pushforwardCospanLeg1 f) = (v ≫ pullback.snd ..) ≫ (pushforwardCospanLeg2 f x) := by have w' := v ≫= pullback.condition - rw [assoc, ← (IsTerminal.hom_ext mkIdTerminal (v ≫ pullback.fst ..) (mkIdTerminal.from y)), + rw [assoc, ← (IsTerminal.hom_ext mkIdTerminal + (v ≫ pullback.fst ..) (mkIdTerminal.from y)), assoc, w'] have close := pushforwardAdjRightInv f x y (v ≫ pullback.snd ..) w simp @@ -397,7 +404,8 @@ namespace PushforwardAdj def idPullbackIso [HasFiniteWidePullbacks C] (X : C) : 𝟭 (Over X) ≅ (Over.pullback (𝟙 X)) := asIso ((conjugateEquiv Adjunction.id (mapPullbackAdj (𝟙 X))) (mapId X).hom) -def idIso [HasFiniteWidePullbacks C] [PushforwardAdj C] (X : C) : (pushforward (𝟙 X)) ≅ 𝟭 (Over X) := +def idIso [HasFiniteWidePullbacks C] [PushforwardAdj C] (X : C) : + (pushforward (𝟙 X)) ≅ 𝟭 (Over X) := asIso ((conjugateEquiv (adj (𝟙 X)) Adjunction.id) (idPullbackIso X).hom) diff --git a/Poly/deprecated/LCCC/BeckChevalley.lean b/Poly/deprecated/LCCC/BeckChevalley.lean index bd7e2c1..5b34067 100644 --- a/Poly/deprecated/LCCC/BeckChevalley.lean +++ b/Poly/deprecated/LCCC/BeckChevalley.lean @@ -92,7 +92,8 @@ variable {C : Type u} [Category.{v} C] open IsPullback Over /-- Calculating the counit components of mapAdjunction. -/ -theorem mapPullbackAdj.counit.app_pullback.fst [HasPullbacks C] {X Y : C} (f : X ⟶ Y) (y : Over Y) : +theorem mapPullbackAdj.counit.app_pullback.fst [HasPullbacks C] {X Y : C} + (f : X ⟶ Y) (y : Over Y) : ((mapPullbackAdj f).counit.app y).left = pullback.fst _ _ := by simp def pullbackNatTrans.app.map [HasPullbacks C] {W X Y Z : C} diff --git a/Poly/deprecated/LCCC/Presheaf.lean b/Poly/deprecated/LCCC/Presheaf.lean index c813a3d..d898e90 100644 --- a/Poly/deprecated/LCCC/Presheaf.lean +++ b/Poly/deprecated/LCCC/Presheaf.lean @@ -47,12 +47,14 @@ In MathLib the comma category is called the ``costructured arrow category''. namespace CategoryOfElements -def equivPsh {C : Type u} {D : Type v} [Category.{w} C] [Category.{w} D] (e : C ≌ D) : Psh C ≌ Psh D := by +def equivPsh {C : Type u} {D : Type v} [Category.{w} C] [Category.{w} D] (e : C ≌ D) : + Psh C ≌ Psh D := by apply congrLeft e.op variable {C : Type u} [Category.{v} C] -def presheafElementsOpIsPshCostructuredArrow (P : Psh C) : Psh (Elements P)ᵒᵖ ≌ Psh (CostructuredArrow yoneda P) := +def presheafElementsOpIsPshCostructuredArrow (P : Psh C) : + Psh (Elements P)ᵒᵖ ≌ Psh (CostructuredArrow yoneda P) := equivPsh (costructuredArrowYonedaEquivalence P) /-! @@ -61,7 +63,8 @@ The slice category (Psh C)/P is called the "over category" in MathLib and writt -/ def overPshIsPshElementsOp {P : Psh C} : Over P ≌ Psh ((Elements P)ᵒᵖ) := - Equivalence.trans (overEquivPresheafCostructuredArrow P) (symm <| equivPsh (costructuredArrowYonedaEquivalence P)) + Equivalence.trans (overEquivPresheafCostructuredArrow P) + (symm <| equivPsh (costructuredArrowYonedaEquivalence P)) /-! # 4. The slice category Psh(C)/P is a CCC @@ -76,7 +79,8 @@ attribute [local instance] ChosenFiniteProducts.ofFiniteProducts def presheafOverCCC {C : Type u} [Category.{max u v} C] (P : Psh C) : CartesianClosed (Over P) := cartesianClosedOfEquiv overPshIsPshElementsOp.symm -def allPresheafOverCCC {C : Type u} [Category.{max u v} C] : Π (P : Psh C), CartesianClosed (Over P) := +def allPresheafOverCCC {C : Type u} [Category.{max u v} C] : + Π (P : Psh C), CartesianClosed (Over P) := fun P => (presheafOverCCC P) end CategoryOfElements @@ -89,24 +93,35 @@ Use results in the file on locally cartesian closed categories. /-! # Some references -1. Wellfounded trees and dependent polynomial functors.Gambino, Nicola; Hyland, Martin. Types for proofs and programs. International workshop, TYPES 2003, Torino, Italy, 2003. Revised selected papers.. Springer Berlin, 2004. p. 210-225. +1. Wellfounded trees and dependent polynomial functors.Gambino, Nicola; Hyland, Martin. Types for +proofs and programs. International workshop, TYPES 2003, Torino, Italy, 2003. Revised selected +papers.. Springer Berlin, 2004. p. 210-225. -2. Tamara Von Glehn. Polynomials and models of type theory. PhD thesis, University of Cambridge, 2015. +2. Tamara Von Glehn. Polynomials and models of type theory. PhD thesis, University of Cambridge, +2015. -3. Joachim Kock. Data types with symmetries and polynomial functors over groupoids. Electronic Notes in Theoretical Computer Science, 286:351–365, 2012. Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVIII). +3. Joachim Kock. Data types with symmetries and polynomial functors over groupoids. Electronic Notes +in Theoretical Computer Science, 286:351–365, 2012. Proceedings of the 28th Conference on the +Mathematical Foundations of Programming Semantics (MFPS XXVIII). -4. Jean-Yves Girard. Normal functors, power series and λ-calculus. Ann. Pure Appl. Logic, 37(2):129–177, 1988. doi:10.1016/0168-0072(88)90025-5. +4. Jean-Yves Girard. Normal functors, power series and λ-calculus. Ann. Pure Appl. Logic, +37(2):129–177, 1988. doi:10.1016/0168-0072(88)90025-5. -5. David Gepner, Rune Haugseng, and Joachim Kock. 8-Operads as analytic monads. Interna- tional Mathematics Research Notices, 2021. +5. David Gepner, Rune Haugseng, and Joachim Kock. 8-Operads as analytic monads. Interna- tional +Mathematics Research Notices, 2021. -6. Nicola Gambino and Joachim Kock. Polynomial functors and polynomial monads. Mathematical Proceedings of the Cambridge Philosophical Society, 154(1):153–192, 2013. +6. Nicola Gambino and Joachim Kock. Polynomial functors and polynomial monads. Mathematical +Proceedings of the Cambridge Philosophical Society, 154(1):153–192, 2013. -7. Marcelo Fiore, Nicola Gambino, Martin Hyland, and Glynn Winskel. The cartesian closed bicategory of generalised species of structures. J. Lond. Math. Soc. (2), 77(1):203–220, 2008. +7. Marcelo Fiore, Nicola Gambino, Martin Hyland, and Glynn Winskel. The cartesian closed bicategory +of generalised species of structures. J. Lond. Math. Soc. (2), 77(1):203–220, 2008. -8. M. Fiore, N. Gambino, M. Hyland, and G. Winskel. Relative pseudomonads, Kleisli bicategories, and substitution monoidal structures. Selecta Mathematica, 24(3):2791–2830, 2018. +8. M. Fiore, N. Gambino, M. Hyland, and G. Winskel. Relative pseudomonads, Kleisli bicategories, and +substitution monoidal structures. Selecta Mathematica, 24(3):2791–2830, 2018. 9. Steve Awodey and Clive Newstead. Polynomial pseudomonads and dependent type theory, 2018. -10. Steve Awodey, Natural models of homotopy type theory, Mathematical Structures in Computer Science, 28 2 (2016) 241-286, arXiv:1406.3219. +10. Steve Awodey, Natural models of homotopy type theory, Mathematical Structures in Computer +Science, 28 2 (2016) 241-286, arXiv:1406.3219. -/ diff --git a/Poly/deprecated/LCCC/Presheaf_test.lean b/Poly/deprecated/LCCC/Presheaf_test.lean index fd887bd..956be62 100644 --- a/Poly/deprecated/LCCC/Presheaf_test.lean +++ b/Poly/deprecated/LCCC/Presheaf_test.lean @@ -83,7 +83,10 @@ def presheafCCC {C : Type v₁} [SmallCategory C] : CartesianClosed (Psh C) := /-! # 2. The category of elements -The category of elements of a *contravariant* functor P : Cᵒᵖ ⥤ Type is the opposite of the category of elements of P regarded as a covariant functor P : Cᵒᵖ ⥤ Type. Thus an object of `(Elements P)ᵒᵖ` is a pair `(X : C, x : P.obj X)` and a morphism `(X, x) ⟶ (Y, y)` is a morphism `f : X ⟶ Y` in `C` for which `P.map f` takes `y` back to `x`. +The category of elements of a *contravariant* functor P : Cᵒᵖ ⥤ Type is the opposite of the category +of elements of P regarded as a covariant functor P : Cᵒᵖ ⥤ Type. Thus an object of `(Elements P)ᵒᵖ` +is a pair `(X : C, x : P.obj X)` and a morphism `(X, x) ⟶ (Y, y)` is a morphism `f : X ⟶ Y` in `C` +for which `P.map f` takes `y` back to `x`. We have an equivalence (Elements P)ᵒᵖ ≌ (yoneda, P). In MathLib the comma category is called the ``costructured arrow category''. -/ @@ -94,7 +97,8 @@ def equivPsh {C D : Type*} [Category C] [Category D] (e : C ≌ D) : (Psh C ≌ Psh D) := by apply congrLeft e.op -def presheafElementsOpIsPshCostructuredArrow (P : Psh C) : Psh (Elements P)ᵒᵖ ≌ Psh (CostructuredArrow yoneda P) := +def presheafElementsOpIsPshCostructuredArrow (P : Psh C) : + Psh (Elements P)ᵒᵖ ≌ Psh (CostructuredArrow yoneda P) := equivPsh (costructuredArrowYonedaEquivalence P) /-! @@ -103,12 +107,15 @@ The slice category (Psh C)/P is called the "over category" in MathLib and writt -/ def overPshIsPshElementsOp {P : Psh.{u,v,max v w} C} : Over P ≌ Psh ((Elements P)ᵒᵖ) := - Equivalence.trans (overEquivPresheafCostructuredArrow P) (symm <| equivPsh (costructuredArrowYonedaEquivalence P)) + Equivalence.trans (overEquivPresheafCostructuredArrow P) + (symm <| equivPsh (costructuredArrowYonedaEquivalence P)) /-! # 4. The slice category Psh(C)/P is a CCC -We transfer the CCC structure across the equivalence (Psh C)/P ≃ Psh((Elements P)ᵒᵖ) using the following: -def cartesianClosedOfEquiv (e : C ≌ D) [CartesianClosed C] : CartesianClosed D := MonoidalClosed.ofEquiv (e.inverse.toMonoidalFunctorOfHasFiniteProducts) e.symm.toAdjunction +We transfer the CCC structure across the equivalence (Psh C)/P ≃ Psh((Elements P)ᵒᵖ) using the +following: +def cartesianClosedOfEquiv (e : C ≌ D) [CartesianClosed C] : CartesianClosed D := +MonoidalClosed.ofEquiv (e.inverse.toMonoidalFunctorOfHasFiniteProducts) e.symm.toAdjunction -/ def presheafOverCCC (P : Psh C) : CartesianClosed (Over P) := @@ -126,24 +133,35 @@ Use results in the file on locally cartesian closed categories. /-! # Some references -1. Wellfounded trees and dependent polynomial functors.Gambino, Nicola; Hyland, Martin. Types for proofs and programs. International workshop, TYPES 2003, Torino, Italy, 2003. Revised selected papers.. Springer Berlin, 2004. p. 210-225. +1. Wellfounded trees and dependent polynomial functors.Gambino, Nicola; Hyland, Martin. Types for +proofs and programs. International workshop, TYPES 2003, Torino, Italy, 2003. Revised selected +papers.. Springer Berlin, 2004. p. 210-225. -2. Tamara Von Glehn. Polynomials and models of type theory. PhD thesis, University of Cambridge, 2015. +2. Tamara Von Glehn. Polynomials and models of type theory. PhD thesis, University of Cambridge, +2015. -3. Joachim Kock. Data types with symmetries and polynomial functors over groupoids. Electronic Notes in Theoretical Computer Science, 286:351–365, 2012. Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVIII). +3. Joachim Kock. Data types with symmetries and polynomial functors over groupoids. Electronic Notes +in Theoretical Computer Science, 286:351–365, 2012. Proceedings of the 28th Conference on the +Mathematical Foundations of Programming Semantics (MFPS XXVIII). -4. Jean-Yves Girard. Normal functors, power series and λ-calculus. Ann. Pure Appl. Logic, 37(2):129–177, 1988. doi:10.1016/0168-0072(88)90025-5. +4. Jean-Yves Girard. Normal functors, power series and λ-calculus. Ann. Pure Appl. Logic, +37(2):129–177, 1988. doi:10.1016/0168-0072(88)90025-5. -5. David Gepner, Rune Haugseng, and Joachim Kock. 8-Operads as analytic monads. Interna- tional Mathematics Research Notices, 2021. +5. David Gepner, Rune Haugseng, and Joachim Kock. 8-Operads as analytic monads. Interna- tional +Mathematics Research Notices, 2021. -6. Nicola Gambino and Joachim Kock. Polynomial functors and polynomial monads. Mathematical Proceedings of the Cambridge Philosophical Society, 154(1):153–192, 2013. +6. Nicola Gambino and Joachim Kock. Polynomial functors and polynomial monads. Mathematical +Proceedings of the Cambridge Philosophical Society, 154(1):153–192, 2013. -7. Marcelo Fiore, Nicola Gambino, Martin Hyland, and Glynn Winskel. The cartesian closed bicategory of generalised species of structures. J. Lond. Math. Soc. (2), 77(1):203–220, 2008. +7. Marcelo Fiore, Nicola Gambino, Martin Hyland, and Glynn Winskel. The cartesian closed bicategory +of generalised species of structures. J. Lond. Math. Soc. (2), 77(1):203–220, 2008. -8. M. Fiore, N. Gambino, M. Hyland, and G. Winskel. Relative pseudomonads, Kleisli bicategories, and substitution monoidal structures. Selecta Mathematica, 24(3):2791–2830, 2018. +8. M. Fiore, N. Gambino, M. Hyland, and G. Winskel. Relative pseudomonads, Kleisli bicategories, and +substitution monoidal structures. Selecta Mathematica, 24(3):2791–2830, 2018. 9. Steve Awodey and Clive Newstead. Polynomial pseudomonads and dependent type theory, 2018. -10. Steve Awodey, Natural models of homotopy type theory, Mathematical Structures in Computer Science, 28 2 (2016) 241-286, arXiv:1406.3219. +10. Steve Awodey, Natural models of homotopy type theory, Mathematical Structures in Computer +Science, 28 2 (2016) 241-286, arXiv:1406.3219. -/ diff --git a/Poly/deprecated/LawvereTheory.lean b/Poly/deprecated/LawvereTheory.lean index e4b16fd..4ca9994 100644 --- a/Poly/deprecated/LawvereTheory.lean +++ b/Poly/deprecated/LawvereTheory.lean @@ -1,2 +1,3 @@ --- (Tambara) The skeleton of the category `T` whose objects are finite sets and whose morphisms are the finite polynomials is the Lawvere theory of commutative semirings. +-- (Tambara) The skeleton of the category `T` whose objects are finite sets and whose morphisms are +-- the finite polynomials is the Lawvere theory of commutative semirings. -- D. Tambara, On multiplicative transfer, Comm. Alg. 21 (1993), 1393–1420. diff --git a/README.md b/README.md index 8962228..ced1bd2 100644 --- a/README.md +++ b/README.md @@ -1,10 +1,10 @@ [![License: Apache 2.0](https://img.shields.io/badge/License-Apache_2.0-lightblue.svg)](https://opensource.org/licenses/Apache-2.0) -[![Documentation](https://img.shields.io/badge/Documentation-Passing-green)](https://sinhp.github.io/groupoid_model_in_lean4/docs/Poly/UvPoly.html) -[![Paper](https://img.shields.io/badge/Paper-WIP-blue)](https://sinhp.github.io/groupoid_model_in_lean4/blueprint/sect0005.html) +[![Documentation](https://img.shields.io/badge/Documentation-blue)](https://sinhp.github.io/Poly/docs/) +[![Blueprint](https://img.shields.io/badge/Blueprint-WIP-blue)](https://sinhp.github.io/Poly/blueprint/) -[Built with Lean 4.34.1](https://github.com/sosudo/Poly/blob/master/lean-toolchain) +[Built with Lean 4.34.1](lean-toolchain) -# Lean4 Formalization Of Polynomial Functors +# Lean 4 Formalization of Polynomial Functors This repository is a [Lean 4](https://github.com/leanprover/lean4) formalization of the theory of Polynomial Functors. Polynomial Functors categorify polynomial functions. @@ -12,46 +12,48 @@ We use this repository as a dependency in the [HoTTLean](https://github.com/sinh ## Content (under development) +Some constructions still contain unfinished proofs. + As part of this formalization, we also formalize locally cartesian closed categories in Lean4. - [x] Locally cartesian closed categories - [x] The Beck-Chevalley condition in LCCC - [x] LCCC structure on types - [x] LCCC structure on presheaves of types - - [x] Isomorphisms of partial-product fans (`PartialProduct.Fan.ext`) (by Unity) + - [x] Isomorphisms of partial-product fans (`PartialProduct.Fan.ext`) - [ ] Univariate Polynomial Functors - [x] Definition of univariate polynomial functors - [x] The construction of associated polynomial functors - - [x] Identity-polynomial evaluation `(id B) @ X ≅ B × X` (`UvPoly.idApplyIso`) (by Unity) + - [x] Identity-polynomial evaluation `(id B) @ X ≅ B × X` (`UvPoly.idApplyIso`) - [x] Monomials - [x] Linear polynomials - - [x] Scalar multiplication preserves exponentiability (`UvPoly.smul`) (by Unity) + - [x] Scalar multiplication preserves exponentiability (`UvPoly.smul`) - [x] Sums of polynomials - - [x] Evaluation-of-sums equivalence (`Poly.sumEquiv`) (by Unity) + - [x] Evaluation-of-sums equivalence (`Poly.sumEquiv`) - [ ] Products of polynomials - [x] Composition of polynomials - [x] The classifying property of polynomial functors - - [x] Universal-property equivalence inverse laws (`UvPoly.equiv`) (by Unity) + - [x] Universal-property equivalence inverse laws (`UvPoly.equiv`) - [x] The monoidal category `C [X]` of univariate polynomial functors - [ ] Cartesian closedness of a category of polynomial functors - [ ] Multivariate Polynomial Functors - [x] Definition of multivariate polynomial functors - [x] The construction of associated polynomial functors - - [x] Identity-polynomial evaluation in the slice (`MvPoly.idApplyIso`) (by Unity) + - [x] Identity-polynomial evaluation in the slice (`MvPoly.idApplyIso`) - [x] Monomials - [x] Linear polynomials - [ ] Symmetric polynomials - [ ] Sums of polynomials - - [x] Products of polynomials: construction and exponentiability (`MvPoly.prod`) (by Unity) + - [x] Products in finitary extensive categories: construction and exponentiability (`MvPoly.prod`) - [x] Composition of polynomials - [ ] The classifying property of polynomial functors - [ ] The bicategory of multivariate polynomial functors - [ ] The double category of polynomial functors - [ ] Differentiation -- [ ] Induction, Well-foundedtrees, Transfinite Induction +- [ ] Induction, Well-founded trees, Transfinite Induction - [ ] Polynomial functors and the semantics of linear logic - [ ] A relational presentation of polynomial functors diff --git a/vendor/checkdecls/UPSTREAM.md b/vendor/checkdecls/UPSTREAM.md index 4c6e162..252a285 100644 --- a/vendor/checkdecls/UPSTREAM.md +++ b/vendor/checkdecls/UPSTREAM.md @@ -23,5 +23,3 @@ Verification on 2026-10-10 with Lean v4.34.1 on Linux: The dependency is stored as ordinary source files, rather than an embedded Git repository, so Poly's relative `vendor/checkdecls` path dependency is portable. -The migration logs and original-revision bundle are held in Poly's local -`.bump-v4.34.1` evidence directory. From 2feaff4a7f310f4edb907484b786bd9a751acef6 Mon Sep 17 00:00:00 2001 From: shiv <33400784+sosudo@users.noreply.github.com> Date: Mon, 9 Nov 2026 01:42:31 -0500 Subject: [PATCH 11/11] chore: restore upstream formatting around the Lean changes --- .../LocallyCartesianClosed/BeckChevalley.lean | 6 +-- .../Distributivity.lean | 2 +- Poly/MvPoly/Basic.lean | 25 ++++------ Poly/Type/Univariate.lean | 6 +-- Poly/UvPoly/Basic.lean | 9 ++-- Poly/UvPoly/UPIso.lean | 3 +- Poly/deprecated/Basic.lean | 3 +- Poly/deprecated/Exponentiable.lean | 27 ++++------- Poly/deprecated/ForMathlib.lean | 3 +- Poly/deprecated/LCCC.lean | 6 +-- Poly/deprecated/LCCC/Basic.lean | 24 ++++------ Poly/deprecated/LCCC/BeckChevalley.lean | 3 +- Poly/deprecated/LCCC/Presheaf.lean | 41 ++++++----------- Poly/deprecated/LCCC/Presheaf_test.lean | 46 ++++++------------- Poly/deprecated/LawvereTheory.lean | 3 +- 15 files changed, 67 insertions(+), 140 deletions(-) diff --git a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/BeckChevalley.lean b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/BeckChevalley.lean index b3d3a30..1b06775 100644 --- a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/BeckChevalley.lean +++ b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/BeckChevalley.lean @@ -312,13 +312,11 @@ theorem mapPullbackAdj.counit_app_left : @[simp] theorem pullbackMapTwoSquare_app : (pullbackMapTwoSquare h f g k sq).app A = - Over.homMk (pullback.map _ _ (A.hom ≫ k) _ _ h k (id_comp _).symm sq.w.symm) - (by simp [pullback.map, pullback.lift_snd]) := by + Over.homMk (pullback.map _ _ (A.hom ≫ k) _ _ h k (id_comp _).symm sq.w.symm) (by simp [pullback.map, pullback.lift_snd]) := by ext simp only [homMk_left, pullbackMapTwoSquare, mapIsoSquare, mateEquiv_apply] apply pullback.hom_ext <;> - simp [pullback.map, pullback.lift_fst, pullback.lift_snd, pullback.lift_fst_assoc, - Category.assoc] + simp [pullback.map, pullback.lift_fst, pullback.lift_snd, pullback.lift_fst_assoc, Category.assoc] theorem forget_map_pullbackMapTwoSquare : (Over.forget Z).map ((pullbackMapTwoSquare h f g k sq).app A) = diff --git a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean index 9a105ad..8b7ebcb 100644 --- a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean +++ b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean @@ -43,7 +43,7 @@ abbrev v := Pi' f u abbrev P := Limits.pullback f (v f u) -- not really needed -def g := pullback.fst (v f u) f +def g := pullback.fst (v f u) f -- (μ_ (Over.mk f) (Over.mk (v f u))).left --pullback.fst (@v _ _ _ _ _ _ _ f u) f /-- This should not be an instance because it's not usually how we want to construct exponentiable morphisms, we'll usually prove all morphims are exponential uniformly diff --git a/Poly/MvPoly/Basic.lean b/Poly/MvPoly/Basic.lean index 4868d2d..a5b340e 100644 --- a/Poly/MvPoly/Basic.lean +++ b/Poly/MvPoly/Basic.lean @@ -91,9 +91,7 @@ def prod {I O : C} [HasBinaryProducts C] [FinitaryExtensive C] (P Q : MvPoly I O E := (pullback (P.p ≫ P.o) Q.o) ⨿ (pullback P.o (Q.p ≫ Q.o)) B := pullback P.o Q.o i := coprod.desc (pullback.fst _ _ ≫ P.i) (pullback.snd _ _ ≫ Q.i) - p := coprod.desc - (pullback.map _ _ _ _ P.p (𝟙 _) (𝟙 _) (by aesop) (by aesop)) - (pullback.map _ _ _ _ (𝟙 _) Q.p (𝟙 _) (by aesop) (by aesop)) + p := coprod.desc (pullback.map _ _ _ _ P.p (𝟙 _) (𝟙 _) (by aesop) (by aesop)) (pullback.map _ _ _ _ (𝟙 _) Q.p (𝟙 _) (by aesop) (by aesop)) exp := by letI : HasFiniteLimits C := hasFiniteLimits_of_hasTerminal_and_pullbacks haveI : ExponentiableMorphism P.p := P.exp @@ -123,8 +121,7 @@ protected def functor {I O : C} (P : MvPoly I O) : variable (I O : C) (P : MvPoly I O) -def apply {I O : C} (P : MvPoly I O) [ExponentiableMorphism P.p] : Over I → Over O := - (P.functor).obj +def apply {I O : C} (P : MvPoly I O) [ExponentiableMorphism P.p] : Over I → Over O := (P.functor).obj /-TODO: write a coercion from `MvPoly` to a functor for evaluation of polynomials at a given object.-/ @@ -187,8 +184,7 @@ def comp.functor : P.functor ⋙ Q.functor ≅ (P.comp Q).functor := by _ ≅ Over.pullback P.i ⋙ (Over.pullback (P.m Q) ⋙ pushforward (r P Q)) ⋙ (Over.pullback (P.ε Q) ⋙ pushforward (P.q Q) ⋙ Over.map (P.w Q)) ⋙ Over.map Q.o := ?_ (Over.pullback P.i ⋙ (Over.pullback (P.m Q) ⋙ pushforward (r P Q)) ⋙ - (Over.pullback (P.ε Q) ⋙ pushforward (P.q Q) ⋙ Over.map (P.w Q)) ⋙ - Over.map Q.o) ≅ _ := ?_ + (Over.pullback (P.ε Q) ⋙ pushforward (P.q Q) ⋙ Over.map (P.w Q)) ⋙ Over.map Q.o) ≅ _ := ?_ (Over.pullback P.i ⋙ Over.pullback (P.m Q) ⋙ Over.pullback (P.n Q)) ⋙ (pushforward (P.p' Q) ⋙ pushforward (P.q Q)) ⋙ Over.map (P.w Q) ⋙ Over.map Q.o ≅ _ := ?_ (Over.pullback P.i ⋙ Over.pullback (P.m Q) ⋙ Over.pullback (P.n Q)) @@ -198,11 +194,9 @@ def comp.functor : P.functor ⋙ Q.functor ≅ (P.comp Q).functor := by apply Iso.symm letI := pullbackMapTwoSquare_of_isPullback_isIso hA' let this := asIso (pullbackMapTwoSquare (P.k Q) (P.h Q) Q.i P.o hA'.toCommSq) - exact isoWhiskerLeft (Over.pullback P.i) <| isoWhiskerLeft (pushforward P.p) <| - isoWhiskerRight this <| _ + exact isoWhiskerLeft (Over.pullback P.i) <| isoWhiskerLeft (pushforward P.p) <| isoWhiskerRight this <| _ · exact isoWhiskerLeft (Over.pullback P.i) <| isoWhiskerLeft (pushforward P.p) - <| isoWhiskerLeft (Over.pullback (P.h Q)) - <| isoWhiskerRight (pentagonIso Q.p (P.k Q)) <| (Over.map Q.o) + <| isoWhiskerLeft (Over.pullback (P.h Q)) <| isoWhiskerRight (pentagonIso Q.p (P.k Q)) <| (Over.map Q.o) · let hpb := (IsPullback.of_hasPullback P.p (pullback.fst P.o Q.i)) have (hpb : IsPullback (P.m Q) (P.r Q) P.p (P.h Q)) : @@ -212,8 +206,7 @@ def comp.functor : P.functor ⋙ Q.functor ≅ (P.comp Q).functor := by (Over.pullback (P.ε Q) ⋙ pushforward (P.q Q) ⋙ Over.map (P.w Q)) ⋙ Over.map Q.o := by {exact isoWhiskerLeft _ <| isoWhiskerRight (pushforwardPullbackIsoSquare hpb) <| _} exact this hpb - · let hpb : IsPullback (P.n Q) (P.p' Q) (P.r Q) (P.ε Q) := - (IsPullback.of_hasPullback (r P Q) (ε P Q)) + · let hpb : IsPullback (P.n Q) (P.p' Q) (P.r Q) (P.ε Q) := (IsPullback.of_hasPullback (r P Q) (ε P Q)) have (hpb : IsPullback (P.n Q) (P.p' Q) (P.r Q) (P.ε Q)) : Over.pullback P.i ⋙ Over.pullback (P.m Q) ⋙ (pushforward (r P Q) ⋙ Over.pullback (P.ε Q)) ⋙ pushforward (P.q Q) ⋙ Over.map (P.w Q) ⋙ Over.map Q.o ≅ @@ -229,8 +222,7 @@ def comp.functor : P.functor ⋙ Q.functor ≅ (P.comp Q).functor := by Over.pullback P.i ⋙ Over.pullback (P.m Q) ⋙ Over.pullback (P.n Q) := by apply Iso.trans (pullbackComp ((P.n Q) ≫ (P.m Q)) P.i) apply isoWhiskerLeft _ <| (pullbackComp (P.n Q) (P.m Q)) - exact isoWhiskerRight (this).symm - ((pushforward (P.p' Q ≫ P.q Q)) ⋙ Over.map (P.w Q) ⋙ Over.map Q.o) + exact isoWhiskerRight (this).symm ((pushforward (P.p' Q ≫ P.q Q)) ⋙ Over.map (P.w Q) ⋙ Over.map Q.o) simp only [assoc] exact isoWhiskerLeft _ <| isoWhiskerLeft _ (mapComp (P.w Q) Q.o).symm @@ -260,8 +252,7 @@ def auxFunctor (P : UvPoly E B) : Over (⊤_ C) ⥤ Over (⊤_ C) := MvPoly.fun /-- We use the equivalence between `Over (⊤_ C)` and `C` to get `functor : C ⥤ C`. Alternatively we can give a direct definition of `functor` in terms of exponentials. -/ -def functor' (P : UvPoly E B) : C ⥤ C := - equivOverTerminal.functor ⋙ P.auxFunctor ⋙ equivOverTerminal.inverse +def functor' (P : UvPoly E B) : C ⥤ C := equivOverTerminal.functor ⋙ P.auxFunctor ⋙ equivOverTerminal.inverse def functorIsoFunctor' [HasBinaryProducts C] (P : UvPoly E B) : P.functor ≅ P.functor' := by unfold functor' auxFunctor functor MvPoly.functor toMvPoly diff --git a/Poly/Type/Univariate.lean b/Poly/Type/Univariate.lean index 8af638d..d68b1e3 100644 --- a/Poly/Type/Univariate.lean +++ b/Poly/Type/Univariate.lean @@ -11,8 +11,7 @@ open CategoryTheory Category Functor /-! # Polynomial functors -We define the notion of one-variable polynomial functors on the category of sets. The locally -cartesian closed structure of sets is implicit in all the constructions. +We define the notion of one-variable polynomial functors on the category of sets. The locally cartesian closed structure of sets is implicit in all the constructions. The bundle corresponding to a `P : Poly` is the projection `fst : Σ b : P.B, P.E b → P.B`. @@ -108,8 +107,7 @@ def bundle : Total P → P.B := Sigma.fst -- TODO: universe issue debugging. /- The bundle of the `sum P Q` is the sum of the bundles. -/ --- theorem sum_bundle_eq : bundle (P.sum Q) = (Sum.map P.bundle Q.bundle) ∘ (sumTotalEquiv P Q) := --- by +-- theorem sum_bundle_eq : bundle (P.sum Q) = (Sum.map P.bundle Q.bundle) ∘ (sumTotalEquiv P Q) := by -- rfl /-- Applying `P` to an object of `Type` -/ diff --git a/Poly/UvPoly/Basic.lean b/Poly/UvPoly/Basic.lean index a3c61e4..0350635 100644 --- a/Poly/UvPoly/Basic.lean +++ b/Poly/UvPoly/Basic.lean @@ -322,8 +322,7 @@ def isLimitFan (P : UvPoly E B) (X : C) : PartialProduct.IsLimit (PartialProduct symm 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 + apply (Adjunction.homEquiv_apply_eq (adj P.p) (overPullbackToStar c.fst c.snd) (Over.homMk m)).mpr simp [overPullbackToStar, PartialProduct.Fan.overPullbackToStar, PartialProduct.Fan.over] apply (Adjunction.homEquiv_apply_eq _ _ _).mpr rw [← h_right] @@ -368,8 +367,7 @@ def proj {Γ X : C} (P : UvPoly E B) (f : Γ ⟶ P @ X) : theorem proj_fst {Γ X : C} {P : UvPoly E B} {f : Γ ⟶ P @ X} : (proj P f).fst = f ≫ P.fstProj X := rfl -/-- The second component of `proj` is a comparison map of pullbacks composed with `ε P X ≫ prod.snd` --/ +/-- The second component of `proj` is a comparison map of pullbacks composed with `ε P X ≫ prod.snd` -/ -- formerly `polyPair_snd_eq_comp_u₂'` @[simp] theorem proj_snd {Γ X : C} {P : UvPoly E B} {f : Γ ⟶ P @ X} : @@ -392,8 +390,7 @@ def comp exact ExponentiableMorphism.comp (pullback.snd Q.p (fan P A).snd) (pullback.fst (fan P A).fst P.p) -/-- The associated functor of the composition of two polynomials is isomorphic to the composition of -the associated functors. -/ +/-- The associated functor of the composition of two polynomials is isomorphic to the composition of the associated functors. -/ def compFunctorIso {E B D C : C} (P : UvPoly E B) (Q : UvPoly D C) : P.functor ⋙ Q.functor ≅ (comp P Q).functor := by diff --git a/Poly/UvPoly/UPIso.lean b/Poly/UvPoly/UPIso.lean index 97d5a11..6a7c940 100644 --- a/Poly/UvPoly/UPIso.lean +++ b/Poly/UvPoly/UPIso.lean @@ -32,8 +32,7 @@ theorem partProdsOver_obj_map {X Y : C} (Γ : Cᵒᵖ) (f : X ⟶ Y) (x : (P.par . dsimp rw! (castMode := .all) [this] simp - change pullback.lift (f := x.1) (g := P.p) - (pullback.fst x.1 P.p ≫ 𝟙 _) (pullback.snd x.1 P.p) _ ≫ + change pullback.lift (f := x.1) (g := P.p) (pullback.fst x.1 P.p ≫ 𝟙 _) (pullback.snd x.1 P.p) _ ≫ x.2 ≫ f = x.2 ≫ f simp rfl diff --git a/Poly/deprecated/Basic.lean b/Poly/deprecated/Basic.lean index 37c9398..bc69ad1 100644 --- a/Poly/deprecated/Basic.lean +++ b/Poly/deprecated/Basic.lean @@ -161,8 +161,7 @@ namespace baseChange open Over MonoidalCategory -/-- For an arrow `f : J ⟶ I` and an object `X : Over I`, the base-change of `X` along `f` is -`pullback.snd`. -/ +/-- For an arrow `f : J ⟶ I` and an object `X : Over I`, the base-change of `X` along `f` is `pullback.snd`. -/ lemma obj_hom_eq_pullback_snd [HasPullbacks C] {I J : C} (f : J ⟶ I) (X : Over I): ((Δ_ f).obj X).hom = pullback.snd X.hom f := rfl diff --git a/Poly/deprecated/Exponentiable.lean b/Poly/deprecated/Exponentiable.lean index 065c1d5..19250cc 100644 --- a/Poly/deprecated/Exponentiable.lean +++ b/Poly/deprecated/Exponentiable.lean @@ -27,8 +27,7 @@ a witness `adj : baseChange f ⊣ functor`. We prove that if a morphism `f : X ⟶ Y` has pushforwards then `f` is exponentiable in the slice category `Over Y`. -In particular, for a morphism `g : X ⟶ I` the exponential `f^* g` is the functor composition -`(baseChange g) ⋙ (Over.map g)`. +In particular, for a morphism `g : X ⟶ I` the exponential `f^* g` is the functor composition `(baseChange g) ⋙ (Over.map g)`. ## Notation @@ -53,8 +52,7 @@ We provide the following notations: Using the notation above, we have * `hom_eq_pullback_snd` proves that `(Δ_ f Over.mk p).hom` is `pullback.snd` -* `natIsoTensorLeft` proves that `Δ_ f` ⋙ `Σ_ f` is isomorphic to the product functor `f × _` in the -slice category `Over I`. See +* `natIsoTensorLeft` proves that `Δ_ f` ⋙ `Σ_ f` is isomorphic to the product functor `f × _` in the slice category `Over I`. See We shall prove that -/ @@ -84,8 +82,7 @@ example (I J X : C) (f : J ⟶ I) (p : X ⟶ I) : exact pullback.fst -/-- For an arrow `f : J ⟶ I` and an object `X : Over I`, the base-change of `X` along `f` is -`pullback.snd`. -/ +/-- For an arrow `f : J ⟶ I` and an object `X : Over I`, the base-change of `X` along `f` is `pullback.snd`. -/ lemma hom_eq_pullback_snd {I J : C} (f : J ⟶ I) (X : Over I): ((Δ_ f).obj X).hom = pullback.snd := rfl @@ -121,8 +118,7 @@ lemma Over.star_eq_Over.mk_prod_fst [HasBinaryProducts C] [HasTerminal C] (I : C (Over.star I).obj X = Over.mk (prod.fst : I ⨯ X ⟶ I) := by simp [Over.star, Over.mk] -/-- The base-change along `terminal.from` ER: Changed statement from an equality to an isomorphism. -Proof of commutativity is stuck because of the rewrite. Perhaps I can do this another way? -/ +/-- The base-change along `terminal.from` ER: Changed statement from an equality to an isomorphism. Proof of commutativity is stuck because of the rewrite. Perhaps I can do this another way? -/ def terminal_from [HasBinaryProducts C] [HasTerminal C] (I : C) (X : Over (⊤_ C)) : (Δ_ (terminal.from I)).obj X ≅ (Over.star I).obj (X.left) := by unfold baseChange Over.star @@ -147,8 +143,7 @@ def terminal_from [HasBinaryProducts C] [HasTerminal C] (I : C) (X : Over (⊤_ -- sorry def isLimitPullbackConeId {I J : C} (f : J ⟶ I) : - IsLimit (PullbackCone.mk (W := J) (fst:= 𝟙 J) (snd := f) (eq:= by simp) : - PullbackCone f (𝟙 I)) := by + IsLimit (PullbackCone.mk (W := J) (fst:= 𝟙 J) (snd := f) (eq:= by simp) : PullbackCone f (𝟙 I)) := by apply PullbackCone.IsLimit.mk · aesop · intro s @@ -176,8 +171,7 @@ def swapIso {X Y : Over I} : @[simp] lemma swap_eq_hom {X Y : Over I} : - ((Σ_ X.hom).obj ((Δ_ X.hom).obj Y)).hom = - (pullbackSymmetry _ _).hom ≫ ((Σ_ Y.hom).obj ((Δ_ Y.hom).obj X)).hom := by + ((Σ_ X.hom).obj ((Δ_ X.hom).obj Y)).hom = (pullbackSymmetry _ _).hom ≫ ((Σ_ Y.hom).obj ((Δ_ Y.hom).obj X)).hom := by simp only [const_obj_obj, id_obj, map_obj_left, baseChange_obj_left, map_obj_hom, baseChange_obj_hom, pullbackSymmetry_hom_comp_snd_assoc] exact pullback.condition.symm @@ -218,8 +212,7 @@ def isBinaryProduct (X Y : Over I) : · apply congr_arg CommaMorphism.left (h ⟨ .right⟩) · apply congr_arg CommaMorphism.left (h ⟨ .left⟩) -/-- The object `(Σ_ X.hom) ((Δ_ X.hom) Y)` is isomorphic to the binary product `X × Y` in the slice -category. -/ +/-- The object `(Σ_ X.hom) ((Δ_ X.hom) Y)` is isomorphic to the binary product `X × Y` in the slice category. -/ @[simps!] def isoProd (X Y : Over I) : (Σ_ X.hom).obj ((Δ_ X.hom).obj Y) ≅ Limits.prod X Y := by @@ -304,14 +297,12 @@ instance comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) adj := ofNatIsoLeft (gexp.adj.comp fexp.adj) (pullbackCompIso f g).symm /-- The conjugate isomorphism between pushforward functors. -/ -def pushforwardCompIso [HasPullbacks C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) - [fexp : CartesianExponentiable f] [gexp : CartesianExponentiable g] : +def pushforwardCompIso [HasPullbacks C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [fexp : CartesianExponentiable f] [gexp : CartesianExponentiable g] : fexp.functor ⋙ gexp.functor ≅ (comp f g).functor := conjugateIsoEquiv (gexp.adj.comp fexp.adj) ((comp f g).adj) (pullbackCompIso f g) /-- An arrow with a pushforward is exponentiable in the slice category. -/ -instance exponentiableOverMk [HasFiniteWidePullbacks C] {I : C} (f : X ⟶ I) - [CartesianExponentiable f] : Exponentiable (Over.mk f) where +instance exponentiableOverMk [HasFiniteWidePullbacks C] {I : C} (f : X ⟶ I) [CartesianExponentiable f] : Exponentiable (Over.mk f) where rightAdj := (Δ_ f) ⋙ (Π_ f) adj := by fapply ofNatIsoLeft diff --git a/Poly/deprecated/ForMathlib.lean b/Poly/deprecated/ForMathlib.lean index 7a57c6d..2d4ad53 100644 --- a/Poly/deprecated/ForMathlib.lean +++ b/Poly/deprecated/ForMathlib.lean @@ -17,8 +17,7 @@ namespace CategoryTheory.Over variable {C : Type*} [Category C] /-- This is useful when `homMk (· ≫ ·)` appears under `Functor.map` or a natural equivalence. -/ -lemma homMk_comp {B : C} {U V W : Over B} (f : U.left ⟶ V.left) (g : V.left ⟶ W.left) - (fg_comp f_comp g_comp) : +lemma homMk_comp {B : C} {U V W : Over B} (f : U.left ⟶ V.left) (g : V.left ⟶ W.left) (fg_comp f_comp g_comp) : homMk (f ≫ g) fg_comp = homMk (V := V) f f_comp ≫ homMk (U := V) g g_comp := by ext; simp diff --git a/Poly/deprecated/LCCC.lean b/Poly/deprecated/LCCC.lean index fc45bb8..2a5b072 100644 --- a/Poly/deprecated/LCCC.lean +++ b/Poly/deprecated/LCCC.lean @@ -81,8 +81,7 @@ cartesian closed categories. 1. A locally cartesian closed category is a category C such that all the slices C/I are cartesian closed categories. -2. Equivalently, a locally cartesian closed category `C` is a category with pullbacks and terminal -object such that each base change functor has a right adjoint, called the pushforward functor. +2. Equivalently, a locally cartesian closed category `C` is a category with pullbacks and terminal object such that each base change functor has a right adjoint, called the pushforward functor. In this file we prove the equivalence of these conditions. -/ @@ -136,8 +135,7 @@ example [HasFiniteWidePullbacks C] {I : C} : HasFiniteLimits (Over I ) := by inf #check Over.hasFiniteLimits -example [LocallyCartesianClosed C] [HasFiniteWidePullbacks C] : - HasFiniteLimits (Over (terminal C)) := by infer_instance +example [LocallyCartesianClosed C] [HasFiniteWidePullbacks C] : HasFiniteLimits (Over (terminal C)) := by infer_instance #check Adjunction diff --git a/Poly/deprecated/LCCC/Basic.lean b/Poly/deprecated/LCCC/Basic.lean index 2b07481..e88fb28 100644 --- a/Poly/deprecated/LCCC/Basic.lean +++ b/Poly/deprecated/LCCC/Basic.lean @@ -71,8 +71,7 @@ variable {C D : Type u} [Category.{v} C] [Category.{v} D] namespace OverBinaryProduct def pullbackCompositionIsBinaryProduct [HasPullbacks C] {I : C} (f x : Over I) : - let pbleg1 : (Over.map f.hom).obj ((Over.pullback f.hom).obj x) ⟶ f := - homMk (pullback.snd ..) rfl + let pbleg1 : (Over.map f.hom).obj ((Over.pullback f.hom).obj x) ⟶ f := homMk (pullback.snd ..) rfl let pbleg2 : (Over.map f.hom).obj ((Over.pullback f.hom).obj x) ⟶ x := Over.homMk (pullback.fst ..) (by simp [pullback.condition]) IsLimit (BinaryFan.mk (pbleg1) (pbleg2)) := by @@ -118,8 +117,7 @@ theorem OverProdIsoRightInv [HasFiniteWidePullbacks C] {I : C} (f x : Over I) : @[simp] theorem Triangle_fst [HasFiniteWidePullbacks C] {I : C} (f x : Over I) : - let pbleg1 : (Over.map f.hom).obj ((Over.pullback f.hom).obj x) ⟶ f := - homMk (pullback.snd ..) rfl + let pbleg1 : (Over.map f.hom).obj ((Over.pullback f.hom).obj x) ⟶ f := homMk (pullback.snd ..) rfl (OverProdIso f x).hom ≫ prod.fst = pbleg1 := IsLimit.conePointUniqueUpToIso_hom_comp (pullbackCompositionIsBinaryProduct f x) (Limits.prodIsProd f x) ⟨ WalkingPair.left⟩ @@ -136,8 +134,7 @@ theorem Triangle_snd [HasFiniteWidePullbacks C] {I : C} @[simp] theorem Triangle.symm_fst [HasFiniteWidePullbacks C] {I : C} (f x : Over I) : - let pbleg1 : (Over.map f.hom).obj ((Over.pullback f.hom).obj x) ⟶ f := - homMk (pullback.snd ..) rfl + let pbleg1 : (Over.map f.hom).obj ((Over.pullback f.hom).obj x) ⟶ f := homMk (pullback.snd ..) rfl (OverProdIso.symm f x).hom ≫ pbleg1 = prod.fst := IsLimit.conePointUniqueUpToIso_hom_comp (Limits.prodIsProd f x) (pullbackCompositionIsBinaryProduct f x) ⟨ WalkingPair.left⟩ @@ -185,8 +182,7 @@ namespace PushforwardAdj instance cartesianClosedOfOver [HasFiniteWidePullbacks C] [PushforwardAdj C] {I : C} : CartesianClosed (Over I) := by - refine .mk _ fun f ↦ .mk f (Over.pullback f.hom ⋙ pushforward f.hom) - (ofNatIsoLeft (F := ?functor ) + refine .mk _ fun f ↦ .mk f (Over.pullback f.hom ⋙ pushforward f.hom) (ofNatIsoLeft (F := ?functor ) ?adj ?iso ) case functor => exact (Over.pullback f.hom ⋙ Over.map f.hom) case adj => exact ((adj f.hom).comp (Over.mapPullbackAdj f.hom)) @@ -273,8 +269,7 @@ def PushforwardObjTo [HasFiniteWidePullbacks C] [OverCC C] rw [CartesianClosed.uncurry_natural_right, CartesianClosed.uncurry_curry] simp have conj : ((Over.map f).map u ≫ (homMk x.hom rfl : (Over.map f).obj x ⟶ Over.mk f)) = - (homMk ((Over.pullback f).obj y).hom : - (Over.map f).obj ((Over.pullback f).obj y) ⟶ Over.mk f) := + (homMk ((Over.pullback f).obj y).hom : (Over.map f).obj ((Over.pullback f).obj y) ⟶ Over.mk f) := OverMorphism.ext (by aesop_cat) exact conj ▸ (Triangle.symm_fst (Over.mk f) y).symm @@ -332,8 +327,7 @@ def pushforwardAdj [HasFiniteWidePullbacks C] [OverCC C] {X Y : C} (f : X ⟶ Y) intro v refine PushforwardObjUP f x y (v ≫ pullback.snd ..) ?commute have w := v ≫= pullback.condition - have lem : (v ≫ pullback.fst ..) = mkIdTerminal.from y := - IsTerminal.hom_ext mkIdTerminal _ _ + have lem : (v ≫ pullback.fst ..) = mkIdTerminal.from y := IsTerminal.hom_ext mkIdTerminal _ _ rw [← lem, assoc, assoc, w] left_inv := by intro u @@ -352,8 +346,7 @@ def pushforwardAdj [HasFiniteWidePullbacks C] [OverCC C] {X Y : C} (f : X ⟶ Y) let w : ((mkIdTerminal (X := Y)).from y) ≫ (pushforwardCospanLeg1 f) = (v ≫ pullback.snd ..) ≫ (pushforwardCospanLeg2 f x) := by have w' := v ≫= pullback.condition - rw [assoc, ← (IsTerminal.hom_ext mkIdTerminal - (v ≫ pullback.fst ..) (mkIdTerminal.from y)), + rw [assoc, ← (IsTerminal.hom_ext mkIdTerminal (v ≫ pullback.fst ..) (mkIdTerminal.from y)), assoc, w'] have close := pushforwardAdjRightInv f x y (v ≫ pullback.snd ..) w simp @@ -404,8 +397,7 @@ namespace PushforwardAdj def idPullbackIso [HasFiniteWidePullbacks C] (X : C) : 𝟭 (Over X) ≅ (Over.pullback (𝟙 X)) := asIso ((conjugateEquiv Adjunction.id (mapPullbackAdj (𝟙 X))) (mapId X).hom) -def idIso [HasFiniteWidePullbacks C] [PushforwardAdj C] (X : C) : - (pushforward (𝟙 X)) ≅ 𝟭 (Over X) := +def idIso [HasFiniteWidePullbacks C] [PushforwardAdj C] (X : C) : (pushforward (𝟙 X)) ≅ 𝟭 (Over X) := asIso ((conjugateEquiv (adj (𝟙 X)) Adjunction.id) (idPullbackIso X).hom) diff --git a/Poly/deprecated/LCCC/BeckChevalley.lean b/Poly/deprecated/LCCC/BeckChevalley.lean index 5b34067..bd7e2c1 100644 --- a/Poly/deprecated/LCCC/BeckChevalley.lean +++ b/Poly/deprecated/LCCC/BeckChevalley.lean @@ -92,8 +92,7 @@ variable {C : Type u} [Category.{v} C] open IsPullback Over /-- Calculating the counit components of mapAdjunction. -/ -theorem mapPullbackAdj.counit.app_pullback.fst [HasPullbacks C] {X Y : C} - (f : X ⟶ Y) (y : Over Y) : +theorem mapPullbackAdj.counit.app_pullback.fst [HasPullbacks C] {X Y : C} (f : X ⟶ Y) (y : Over Y) : ((mapPullbackAdj f).counit.app y).left = pullback.fst _ _ := by simp def pullbackNatTrans.app.map [HasPullbacks C] {W X Y Z : C} diff --git a/Poly/deprecated/LCCC/Presheaf.lean b/Poly/deprecated/LCCC/Presheaf.lean index d898e90..c813a3d 100644 --- a/Poly/deprecated/LCCC/Presheaf.lean +++ b/Poly/deprecated/LCCC/Presheaf.lean @@ -47,14 +47,12 @@ In MathLib the comma category is called the ``costructured arrow category''. namespace CategoryOfElements -def equivPsh {C : Type u} {D : Type v} [Category.{w} C] [Category.{w} D] (e : C ≌ D) : - Psh C ≌ Psh D := by +def equivPsh {C : Type u} {D : Type v} [Category.{w} C] [Category.{w} D] (e : C ≌ D) : Psh C ≌ Psh D := by apply congrLeft e.op variable {C : Type u} [Category.{v} C] -def presheafElementsOpIsPshCostructuredArrow (P : Psh C) : - Psh (Elements P)ᵒᵖ ≌ Psh (CostructuredArrow yoneda P) := +def presheafElementsOpIsPshCostructuredArrow (P : Psh C) : Psh (Elements P)ᵒᵖ ≌ Psh (CostructuredArrow yoneda P) := equivPsh (costructuredArrowYonedaEquivalence P) /-! @@ -63,8 +61,7 @@ The slice category (Psh C)/P is called the "over category" in MathLib and writt -/ def overPshIsPshElementsOp {P : Psh C} : Over P ≌ Psh ((Elements P)ᵒᵖ) := - Equivalence.trans (overEquivPresheafCostructuredArrow P) - (symm <| equivPsh (costructuredArrowYonedaEquivalence P)) + Equivalence.trans (overEquivPresheafCostructuredArrow P) (symm <| equivPsh (costructuredArrowYonedaEquivalence P)) /-! # 4. The slice category Psh(C)/P is a CCC @@ -79,8 +76,7 @@ attribute [local instance] ChosenFiniteProducts.ofFiniteProducts def presheafOverCCC {C : Type u} [Category.{max u v} C] (P : Psh C) : CartesianClosed (Over P) := cartesianClosedOfEquiv overPshIsPshElementsOp.symm -def allPresheafOverCCC {C : Type u} [Category.{max u v} C] : - Π (P : Psh C), CartesianClosed (Over P) := +def allPresheafOverCCC {C : Type u} [Category.{max u v} C] : Π (P : Psh C), CartesianClosed (Over P) := fun P => (presheafOverCCC P) end CategoryOfElements @@ -93,35 +89,24 @@ Use results in the file on locally cartesian closed categories. /-! # Some references -1. Wellfounded trees and dependent polynomial functors.Gambino, Nicola; Hyland, Martin. Types for -proofs and programs. International workshop, TYPES 2003, Torino, Italy, 2003. Revised selected -papers.. Springer Berlin, 2004. p. 210-225. +1. Wellfounded trees and dependent polynomial functors.Gambino, Nicola; Hyland, Martin. Types for proofs and programs. International workshop, TYPES 2003, Torino, Italy, 2003. Revised selected papers.. Springer Berlin, 2004. p. 210-225. -2. Tamara Von Glehn. Polynomials and models of type theory. PhD thesis, University of Cambridge, -2015. +2. Tamara Von Glehn. Polynomials and models of type theory. PhD thesis, University of Cambridge, 2015. -3. Joachim Kock. Data types with symmetries and polynomial functors over groupoids. Electronic Notes -in Theoretical Computer Science, 286:351–365, 2012. Proceedings of the 28th Conference on the -Mathematical Foundations of Programming Semantics (MFPS XXVIII). +3. Joachim Kock. Data types with symmetries and polynomial functors over groupoids. Electronic Notes in Theoretical Computer Science, 286:351–365, 2012. Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVIII). -4. Jean-Yves Girard. Normal functors, power series and λ-calculus. Ann. Pure Appl. Logic, -37(2):129–177, 1988. doi:10.1016/0168-0072(88)90025-5. +4. Jean-Yves Girard. Normal functors, power series and λ-calculus. Ann. Pure Appl. Logic, 37(2):129–177, 1988. doi:10.1016/0168-0072(88)90025-5. -5. David Gepner, Rune Haugseng, and Joachim Kock. 8-Operads as analytic monads. Interna- tional -Mathematics Research Notices, 2021. +5. David Gepner, Rune Haugseng, and Joachim Kock. 8-Operads as analytic monads. Interna- tional Mathematics Research Notices, 2021. -6. Nicola Gambino and Joachim Kock. Polynomial functors and polynomial monads. Mathematical -Proceedings of the Cambridge Philosophical Society, 154(1):153–192, 2013. +6. Nicola Gambino and Joachim Kock. Polynomial functors and polynomial monads. Mathematical Proceedings of the Cambridge Philosophical Society, 154(1):153–192, 2013. -7. Marcelo Fiore, Nicola Gambino, Martin Hyland, and Glynn Winskel. The cartesian closed bicategory -of generalised species of structures. J. Lond. Math. Soc. (2), 77(1):203–220, 2008. +7. Marcelo Fiore, Nicola Gambino, Martin Hyland, and Glynn Winskel. The cartesian closed bicategory of generalised species of structures. J. Lond. Math. Soc. (2), 77(1):203–220, 2008. -8. M. Fiore, N. Gambino, M. Hyland, and G. Winskel. Relative pseudomonads, Kleisli bicategories, and -substitution monoidal structures. Selecta Mathematica, 24(3):2791–2830, 2018. +8. M. Fiore, N. Gambino, M. Hyland, and G. Winskel. Relative pseudomonads, Kleisli bicategories, and substitution monoidal structures. Selecta Mathematica, 24(3):2791–2830, 2018. 9. Steve Awodey and Clive Newstead. Polynomial pseudomonads and dependent type theory, 2018. -10. Steve Awodey, Natural models of homotopy type theory, Mathematical Structures in Computer -Science, 28 2 (2016) 241-286, arXiv:1406.3219. +10. Steve Awodey, Natural models of homotopy type theory, Mathematical Structures in Computer Science, 28 2 (2016) 241-286, arXiv:1406.3219. -/ diff --git a/Poly/deprecated/LCCC/Presheaf_test.lean b/Poly/deprecated/LCCC/Presheaf_test.lean index 956be62..fd887bd 100644 --- a/Poly/deprecated/LCCC/Presheaf_test.lean +++ b/Poly/deprecated/LCCC/Presheaf_test.lean @@ -83,10 +83,7 @@ def presheafCCC {C : Type v₁} [SmallCategory C] : CartesianClosed (Psh C) := /-! # 2. The category of elements -The category of elements of a *contravariant* functor P : Cᵒᵖ ⥤ Type is the opposite of the category -of elements of P regarded as a covariant functor P : Cᵒᵖ ⥤ Type. Thus an object of `(Elements P)ᵒᵖ` -is a pair `(X : C, x : P.obj X)` and a morphism `(X, x) ⟶ (Y, y)` is a morphism `f : X ⟶ Y` in `C` -for which `P.map f` takes `y` back to `x`. +The category of elements of a *contravariant* functor P : Cᵒᵖ ⥤ Type is the opposite of the category of elements of P regarded as a covariant functor P : Cᵒᵖ ⥤ Type. Thus an object of `(Elements P)ᵒᵖ` is a pair `(X : C, x : P.obj X)` and a morphism `(X, x) ⟶ (Y, y)` is a morphism `f : X ⟶ Y` in `C` for which `P.map f` takes `y` back to `x`. We have an equivalence (Elements P)ᵒᵖ ≌ (yoneda, P). In MathLib the comma category is called the ``costructured arrow category''. -/ @@ -97,8 +94,7 @@ def equivPsh {C D : Type*} [Category C] [Category D] (e : C ≌ D) : (Psh C ≌ Psh D) := by apply congrLeft e.op -def presheafElementsOpIsPshCostructuredArrow (P : Psh C) : - Psh (Elements P)ᵒᵖ ≌ Psh (CostructuredArrow yoneda P) := +def presheafElementsOpIsPshCostructuredArrow (P : Psh C) : Psh (Elements P)ᵒᵖ ≌ Psh (CostructuredArrow yoneda P) := equivPsh (costructuredArrowYonedaEquivalence P) /-! @@ -107,15 +103,12 @@ The slice category (Psh C)/P is called the "over category" in MathLib and writt -/ def overPshIsPshElementsOp {P : Psh.{u,v,max v w} C} : Over P ≌ Psh ((Elements P)ᵒᵖ) := - Equivalence.trans (overEquivPresheafCostructuredArrow P) - (symm <| equivPsh (costructuredArrowYonedaEquivalence P)) + Equivalence.trans (overEquivPresheafCostructuredArrow P) (symm <| equivPsh (costructuredArrowYonedaEquivalence P)) /-! # 4. The slice category Psh(C)/P is a CCC -We transfer the CCC structure across the equivalence (Psh C)/P ≃ Psh((Elements P)ᵒᵖ) using the -following: -def cartesianClosedOfEquiv (e : C ≌ D) [CartesianClosed C] : CartesianClosed D := -MonoidalClosed.ofEquiv (e.inverse.toMonoidalFunctorOfHasFiniteProducts) e.symm.toAdjunction +We transfer the CCC structure across the equivalence (Psh C)/P ≃ Psh((Elements P)ᵒᵖ) using the following: +def cartesianClosedOfEquiv (e : C ≌ D) [CartesianClosed C] : CartesianClosed D := MonoidalClosed.ofEquiv (e.inverse.toMonoidalFunctorOfHasFiniteProducts) e.symm.toAdjunction -/ def presheafOverCCC (P : Psh C) : CartesianClosed (Over P) := @@ -133,35 +126,24 @@ Use results in the file on locally cartesian closed categories. /-! # Some references -1. Wellfounded trees and dependent polynomial functors.Gambino, Nicola; Hyland, Martin. Types for -proofs and programs. International workshop, TYPES 2003, Torino, Italy, 2003. Revised selected -papers.. Springer Berlin, 2004. p. 210-225. +1. Wellfounded trees and dependent polynomial functors.Gambino, Nicola; Hyland, Martin. Types for proofs and programs. International workshop, TYPES 2003, Torino, Italy, 2003. Revised selected papers.. Springer Berlin, 2004. p. 210-225. -2. Tamara Von Glehn. Polynomials and models of type theory. PhD thesis, University of Cambridge, -2015. +2. Tamara Von Glehn. Polynomials and models of type theory. PhD thesis, University of Cambridge, 2015. -3. Joachim Kock. Data types with symmetries and polynomial functors over groupoids. Electronic Notes -in Theoretical Computer Science, 286:351–365, 2012. Proceedings of the 28th Conference on the -Mathematical Foundations of Programming Semantics (MFPS XXVIII). +3. Joachim Kock. Data types with symmetries and polynomial functors over groupoids. Electronic Notes in Theoretical Computer Science, 286:351–365, 2012. Proceedings of the 28th Conference on the Mathematical Foundations of Programming Semantics (MFPS XXVIII). -4. Jean-Yves Girard. Normal functors, power series and λ-calculus. Ann. Pure Appl. Logic, -37(2):129–177, 1988. doi:10.1016/0168-0072(88)90025-5. +4. Jean-Yves Girard. Normal functors, power series and λ-calculus. Ann. Pure Appl. Logic, 37(2):129–177, 1988. doi:10.1016/0168-0072(88)90025-5. -5. David Gepner, Rune Haugseng, and Joachim Kock. 8-Operads as analytic monads. Interna- tional -Mathematics Research Notices, 2021. +5. David Gepner, Rune Haugseng, and Joachim Kock. 8-Operads as analytic monads. Interna- tional Mathematics Research Notices, 2021. -6. Nicola Gambino and Joachim Kock. Polynomial functors and polynomial monads. Mathematical -Proceedings of the Cambridge Philosophical Society, 154(1):153–192, 2013. +6. Nicola Gambino and Joachim Kock. Polynomial functors and polynomial monads. Mathematical Proceedings of the Cambridge Philosophical Society, 154(1):153–192, 2013. -7. Marcelo Fiore, Nicola Gambino, Martin Hyland, and Glynn Winskel. The cartesian closed bicategory -of generalised species of structures. J. Lond. Math. Soc. (2), 77(1):203–220, 2008. +7. Marcelo Fiore, Nicola Gambino, Martin Hyland, and Glynn Winskel. The cartesian closed bicategory of generalised species of structures. J. Lond. Math. Soc. (2), 77(1):203–220, 2008. -8. M. Fiore, N. Gambino, M. Hyland, and G. Winskel. Relative pseudomonads, Kleisli bicategories, and -substitution monoidal structures. Selecta Mathematica, 24(3):2791–2830, 2018. +8. M. Fiore, N. Gambino, M. Hyland, and G. Winskel. Relative pseudomonads, Kleisli bicategories, and substitution monoidal structures. Selecta Mathematica, 24(3):2791–2830, 2018. 9. Steve Awodey and Clive Newstead. Polynomial pseudomonads and dependent type theory, 2018. -10. Steve Awodey, Natural models of homotopy type theory, Mathematical Structures in Computer -Science, 28 2 (2016) 241-286, arXiv:1406.3219. +10. Steve Awodey, Natural models of homotopy type theory, Mathematical Structures in Computer Science, 28 2 (2016) 241-286, arXiv:1406.3219. -/ diff --git a/Poly/deprecated/LawvereTheory.lean b/Poly/deprecated/LawvereTheory.lean index 4ca9994..e4b16fd 100644 --- a/Poly/deprecated/LawvereTheory.lean +++ b/Poly/deprecated/LawvereTheory.lean @@ -1,3 +1,2 @@ --- (Tambara) The skeleton of the category `T` whose objects are finite sets and whose morphisms are --- the finite polynomials is the Lawvere theory of commutative semirings. +-- (Tambara) The skeleton of the category `T` whose objects are finite sets and whose morphisms are the finite polynomials is the Lawvere theory of commutative semirings. -- D. Tambara, On multiplicative transfer, Comm. Alg. 21 (1993), 1393–1420.