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/LocallyCartesianClosed/Extensive.lean b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Extensive.lean
new file mode 100644
index 0000000..77dbf22
--- /dev/null
+++ b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Extensive.lean
@@ -0,0 +1,162 @@
+import Mathlib.CategoryTheory.Extensive
+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
+
+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/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..37d203f 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,20 +114,33 @@ 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
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` -/
@@ -165,9 +182,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 +212,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 +227,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..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
/-!
@@ -26,7 +28,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]
@@ -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) :
@@ -104,19 +126,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
diff --git a/Poly/Type/Univariate.lean b/Poly/Type/Univariate.lean
index 0bb4cbe..d68b1e3 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`. -/
@@ -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
@@ -177,7 +178,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 +190,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 +225,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..0350635 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]
@@ -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] :
@@ -98,7 +113,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}
@@ -134,10 +149,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 +285,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 +300,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 +326,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 +372,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..628263d 100644
--- a/Poly/UvPoly/UPFan.lean
+++ b/Poly/UvPoly/UPFan.lean
@@ -8,27 +8,40 @@ 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}
-/-- 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
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..252a285
--- /dev/null
+++ b/vendor/checkdecls/UPSTREAM.md
@@ -0,0 +1,25 @@
+# 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.
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