From 708a54b4a4fa292afe838e0bf0e67484e58798a7 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Sat, 9 Nov 2024 23:13:10 -0500 Subject: [PATCH 01/18] feat: utilities --- Poly/Util.lean | 81 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 81 insertions(+) create mode 100644 Poly/Util.lean diff --git a/Poly/Util.lean b/Poly/Util.lean new file mode 100644 index 0000000..b29cc35 --- /dev/null +++ b/Poly/Util.lean @@ -0,0 +1,81 @@ +import Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback +import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq +import Mathlib.CategoryTheory.Comma.Over + +/-! Miscellaneous results that don't fit anywhere else. -/ + +namespace CategoryTheory + +variable {𝒞 𝒟 : Type*} [Category 𝒞] [Category 𝒟] + +/-! ## Pullbacks -/ + +@[simp] +lemma Limits.pullback.lift_fst_snd {X Y Z : 𝒞} {f : X ⟶ Z} {g : Y ⟶ Z} [HasPullback f g] (eq) : + pullback.lift (pullback.fst f g) (pullback.snd f g) eq = 𝟙 (pullback f g) := by + ext <;> simp + +/-! ## `eqToHom` -/ + +/-- Note: if possible, +it's best to immediately rewrite `eqToHom` to an isomorphism +whose data is not defined by destructing an equality +in the second premise of this lemma. -/ +-- If only there was a LiftIsos typeclass to do this for us! +lemma Sigma_hom_ext {X Y : 𝒞} {Z : 𝒟} (P : (X ⟶ Y) → 𝒟) + (p q : (f : X ⟶ Y) × (P f ⟶ Z)) + (fst_eq : p.fst = q.fst) + (snd_eq : (h : p.fst = q.fst) → p.snd = eqToHom (h ▸ rfl) ≫ q.snd) : + p = q := by + let ⟨b, e⟩ := p + let ⟨c, f⟩ := q + cases fst_eq + simp at snd_eq + simp [snd_eq] + +lemma Limits.pullback.eqToHom_eq_map {X Y Z : 𝒞} + (f₁ f₂ : X ⟶ Z) (g₁ g₂ : Y ⟶ Z) [HasPullback f₁ g₁] [HasPullback f₂ g₂] + (f_eq : f₁ = f₂) (g_eq : g₁ = g₂) : + eqToHom (by cases f_eq; cases g_eq; rfl) = + pullback.map f₁ g₁ f₂ g₂ (𝟙 X) (𝟙 Y) (𝟙 Z) (by simp [f_eq]) (by simp [g_eq]) := by + cases f_eq; cases g_eq; simp + +lemma IsPullback.eqToHom_eq_lift {P' P X Y Z : 𝒞} + {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} + (pb : IsPullback fst snd f g) (eq : P' = P) : + eqToHom eq = + pb.lift (eqToHom eq ≫ fst) (eqToHom eq ≫ snd) (by simp [pb.w]) := by + cases eq; apply pb.hom_ext <;> simp + +lemma Over.eqToHom_eq_homMk {E B : 𝒞} (f g : E ⟶ B) (eq : f = g) : + eqToHom (show (Over.mk f) = (Over.mk g) from eq ▸ rfl) = + Over.homMk (𝟙 E) (by simp [eq]) := by + cases eq; rfl + +/-! ## Over categories -/ + +namespace Over + +/-- This is useful when `homMk (· ≫ ·)` appears under `Functor.map` or a natural equivalence. -/ +lemma homMk_comp {B : 𝒞} {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 := + rfl + +@[simp] +lemma left_homMk {B : 𝒞} {U V : Over B} (f : U ⟶ V) (h) : + homMk f.left h = f := + rfl + +@[simp] +lemma homMk_id {B : 𝒞} {U : Over B} (h) : homMk (𝟙 U.left) h = 𝟙 U := + rfl + +-- -- Probably bad as a simp lemma? +-- lemma homMk_id' {E B : 𝒞} {f g : E ⟶ B} (h) : +-- homMk (U := Over.mk f) (V := Over.mk g) (𝟙 E) h = +-- (Over.isoMk (Iso.refl E) (by simpa using h)).hom := by +-- ext; simp + +end Over +end CategoryTheory From 6ef5ac40baf6ccc1fba88a20697a0a2cfd1c0c8d Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Sat, 9 Nov 2024 23:13:29 -0500 Subject: [PATCH 02/18] feat: bifunctor constructions --- Poly/Bifunctor.lean | 238 +++++++++++++++++++++++++++++++++++ Poly/Tactic/BanishCasts.lean | 48 +++++++ 2 files changed, 286 insertions(+) create mode 100644 Poly/Bifunctor.lean create mode 100644 Poly/Tactic/BanishCasts.lean diff --git a/Poly/Bifunctor.lean b/Poly/Bifunctor.lean new file mode 100644 index 0000000..ff27ba9 --- /dev/null +++ b/Poly/Bifunctor.lean @@ -0,0 +1,238 @@ +import Mathlib.CategoryTheory.Functor.Currying + +import Poly.Util +import Poly.Tactic.BanishCasts + +/-! # Bifunctors + +We define some constructions on bifunctors (aka profunctors), +that is functors in two arguments. + +Their utility in Poly is as a tool for packaging and composing natural equivalences. +For example, given `F,H : 𝒞 ⟶ ℰ` and `G,I : 𝒟 ⟶ ℰ`, +``` +F(X) ⟶ G(Y) +============ +H(X) ⟶ I(Y) +``` +would be a natural isomorphism of bifunctors `𝒞ᵒᵖ ⥤ 𝒟 ⥤ Type v` +given by `(X,Y) ↦ F(X) ⟶ G(Y)` and `(X, Y) ↦ H(X) ⟶ I(Y)`. -/ + +namespace CategoryTheory + +variable {𝒞 𝒟 ℰ : Type*} [Category 𝒞] [Category 𝒟] [Category ℰ] + +/-- Natural isomorphism of bifunctors from naturality in both arguments. -/ +def NatIso.ofComponents₂ {F G : 𝒞 ⥤ 𝒟 ⥤ ℰ} + (app : ∀ Γ X, (F.obj Γ).obj X ≅ (G.obj Γ).obj X) + (naturality_left : ∀ {Γ Δ : 𝒞} (X : 𝒟) (σ : Γ ⟶ Δ), + (F.map σ).app X ≫ (app Δ X).hom = (app Γ X).hom ≫ (G.map σ).app X := by aesop_cat) + (naturality_right : ∀ {X Y : 𝒟} (Γ : 𝒞) (f : X ⟶ Y), + (F.obj Γ).map f ≫ (app Γ Y).hom = (app Γ X).hom ≫ (G.obj Γ).map f := by aesop_cat) : + F ≅ G := + NatIso.ofComponents + (fun Γ => NatIso.ofComponents (app Γ) (fun f => by simpa using naturality_right Γ f)) + (fun σ => by ext X : 2; simpa using naturality_left X σ) + +-- /-- The bifunctor `(Γ, X) ↦ (b : Γ.unop ⟶ B) × (P.obj (Over.mk b) ⟶ X)`. -/ +-- @[simps!] +-- def Functor.Sigma_Over.{v} [Category.{v} 𝒟] {B : 𝒞} (P : Over B ⥤ 𝒟) : 𝒞ᵒᵖ ⥤ 𝒟 ⥤ Type v := +-- curry.obj { +-- obj := fun (Γ, X) => (b : Γ.unop ⟶ B) × (P.obj (Over.mk b) ⟶ X) +-- map := fun (σ, f) ⟨b, e⟩ => +-- ⟨σ.unop ≫ b, +-- P.map (Over.homMk (V := Over.mk b) σ.unop (by simp)) ≫ e ≫ f⟩ +-- map_id := fun (Γ, X) => by +-- refine funext fun _ => ?_ +-- apply Sigma_hom_ext +-- . simp [eqToHom_map] +-- . dsimp +-- intro h +-- rw [← Over.eqToHom_eq_homMk (eq := h)] +-- simp [eqToHom_map] +-- map_comp := fun {_} {_} {Y} (σ, f) (τ, g) => by +-- refine funext fun ⟨b, e⟩ => ?_ +-- apply Sigma_hom_ext +-- . simp +-- . dsimp +-- intro h +-- rw [Over.homMk_comp (U := Over.mk ((τ.unop ≫ σ.unop) ≫ b)) (V := Over.mk (σ.unop ≫ b)) +-- (f_comp := by simp) (g_comp := by simp)] +-- generalize_proofs -- I <3 generalize_proofs +-- generalize (τ.unop ≫ σ.unop) ≫ b = x at * +-- cases h +-- simp +-- } + +/-- A functor into `𝒟` that depends on `F`. -/ +-- TODO: does this correspond to a known construction? +structure DepFunctor (F : 𝒞 ⥤ Type*) (𝒟 : Type*) [Category 𝒟] where + obj : ∀ ⦃Γ⦄, F.obj Γ → 𝒟 + map : ∀ ⦃Γ Δ⦄ (σ : Γ ⟶ Δ) (b : F.obj Γ), obj b ⟶ obj (F.map σ b) + map_id : ∀ ⦃Γ⦄ (b : F.obj Γ), map (𝟙 Γ) b = eqToHom (F.map_id _ ▸ rfl) + map_comp : ∀ ⦃Γ Δ Θ⦄ (σ : Γ ⟶ Δ) (τ : Δ ⟶ Θ) (b : F.obj Γ), + map (σ ≫ τ) b = map σ b ≫ map τ (F.map σ b) ≫ eqToHom (F.map_comp .. ▸ rfl) + +attribute [reassoc] DepFunctor.map_comp +attribute [simp] DepFunctor.map_id DepFunctor.map_comp DepFunctor.map_comp_assoc + +@[simps] +def DepFunctor.isoLeft.{v} {F₁ F₂ : 𝒞 ⥤ Type v} {𝒟 : Type*} [Category 𝒟] + (F : DepFunctor F₁ 𝒟) (i : F₂ ≅ F₁) : DepFunctor F₂ 𝒟 where + obj Γ b := F.obj (i.hom.app Γ b) + map Γ _ σ b := F.map σ (i.hom.app Γ b) ≫ eqToHom (FunctorToTypes.naturality F₂ F₁ i.hom .. ▸ rfl) + map_id _ b := by simp + map_comp _ _ _ σ τ b := by + slice_rhs 2 3 => rw [← eqToHom_naturality _ (by simp [FunctorToTypes.naturality])] + simp + +structure DepNatTrans {F : 𝒞 ⥤ Type*} {𝒟 : Type*} [Category 𝒟] (G₁ G₂ : DepFunctor F 𝒟) where + app : ∀ {Γ} (b : F.obj Γ), G₁.obj b ⟶ G₂.obj b + naturality : ∀ {Γ Δ} (σ : Γ ⟶ Δ) (b : F.obj Γ), + app b ≫ G₂.map σ b = G₁.map σ b ≫ app (F.map σ b) + +attribute [reassoc] DepNatTrans.naturality + +instance (F : 𝒞 ⥤ Type*) (𝒟 : Type*) [Category 𝒟] : Category (DepFunctor F 𝒟) where + Hom := DepNatTrans + id G := { + app := fun _ => 𝟙 _ + naturality := by simp + } + comp η ν := { + app := fun b => η.app b ≫ ν.app b + naturality := by simp [η.naturality_assoc, ν.naturality] + } + id_comp := by simp + comp_id := by simp + assoc := by simp + +-- TODO: characterize isos in the above category as these things +structure DepNatIso (F : 𝒞 ⥤ Type*) {𝒟 : Type*} [Category 𝒟] (G₁ G₂ : DepFunctor F 𝒟) where + i : ∀ {Γ} (b : F.obj Γ), G₁.obj b ≅ G₂.obj b + i_naturality : ∀ {Γ Δ} (σ : Γ ⟶ Δ) (b : F.obj Γ), + (i b).hom ≫ G₂.map σ b = G₁.map σ b ≫ (i (F.map σ b)).hom + +/-- Dependent sum over a type-valued functor. +This serves to encapsulate dependent sums that vary naturally in their parameters. -/ +@[simps!] +def Functor.Sigma.{v} (F : 𝒞 ⥤ Type v) (G : DepFunctor F (𝒟 ⥤ Type v)) : 𝒞 ⥤ 𝒟 ⥤ Type v := + curry.obj { + obj := fun (Γ, X) => (b : F.obj Γ) × ((G.obj b).obj X) + map := fun (σ, f) ⟨b, e⟩ => + ⟨F.map σ b, (G.map σ b).app _ ((G.obj b).map f e)⟩ + map_id := fun (Γ, X) => by + dsimp + refine funext fun ⟨b, e⟩ => ?_ + dsimp at * + congr! 1 with h + . simp + . simp only [FunctorToTypes.map_id_apply, DepFunctor.map_id] + generalize_proofs + generalize (eq_lhs% h) = x at * + cases h + simp + map_comp := fun {_} {_} {Y} (σ, f) (τ, g) => by + refine funext fun ⟨b, e⟩ => ?_ + dsimp at * + congr! 1 with h + . simp + . simp only [FunctorToTypes.map_comp_apply, DepFunctor.map_comp] + generalize_proofs + generalize (eq_lhs% h) = x at * + cases h + simp [FunctorToTypes.naturality] + } + +-- Not super important, we don't need to treat b as an over-category element ever. +-- @[simps!] +-- def Functor.Sigma_Over'.{v} [Category.{v} 𝒟] {B : 𝒞} (P : Over B ⥤ 𝒟) : 𝒞ᵒᵖ ⥤ 𝒟 ⥤ Type v := +-- Functor.Sigma (yoneda.obj B) (fun b => coyoneda.obj $ Opposite.op $ P.obj $ Over.mk b) +-- (fun σ b => { app := fun _ e => P.map (Over.homMk (V := Over.mk b) σ.unop (by simp)) ≫ e }) +-- (fun b => by +-- ext X b +-- simp only [eqToHom_app, coyoneda_obj_obj, yoneda_obj_map, unop_id] at b ⊢ +-- generalize_proofs pf1 pf2 +-- sorry +-- -- etc +-- ) +-- (fun σ τ b => sorry) + +def Functor.Sigma.isoCongrLeft.{v} (F₁ F₂ : 𝒞 ⥤ Type v) (G : DepFunctor F₁ (𝒟 ⥤ Type v)) + (i : F₂ ≅ F₁) : Functor.Sigma F₁ G ≅ Functor.Sigma F₂ (G.isoLeft i) := + NatIso.ofComponents₂ + (fun Γ X => Equiv.toIso { + toFun := fun ⟨b, e⟩ => ⟨i.inv.app Γ b, cast (by simp) e⟩ + invFun := fun ⟨b, e⟩ => ⟨i.hom.app Γ b, e⟩ + left_inv := fun ⟨_, _⟩ => by simp + right_inv := fun ⟨_, _⟩ => by simp + }) + (fun X σ => by + ext ⟨b, e⟩ + simp only [Sigma, DepFunctor.isoLeft_obj, prod_Hom, DepFunctor.isoLeft_map, + FunctorToTypes.comp, curry_obj_obj_obj, curry_obj_map_app, FunctorToTypes.map_id_apply, + Equiv.toIso_hom, Equiv.coe_fn_mk, types_comp_apply, eqToHom_app, Sigma.mk.inj_iff, + FunctorToTypes.naturality, true_and] + generalize_proofs -- TODO: banish_casts tactic + have : (i.hom.app _ (F₂.map σ (i.inv.app _ b))) = F₁.map σ b := by + simp [FunctorToTypes.naturality] + generalize (eq_lhs% this) = x at *; cases this + have := FunctorToTypes.inv_hom_id_app_apply _ _ i _ (F₁.map σ b) + generalize (eq_lhs% this) = x at *; cases this + have := FunctorToTypes.inv_hom_id_app_apply _ _ i _ b + generalize (eq_lhs% this) = x at *; cases this + simp) + (fun Γ f => by + ext ⟨b,e⟩ + simp only [Sigma, DepFunctor.isoLeft_obj, prod_Hom, DepFunctor.isoLeft_map, + FunctorToTypes.comp, curry_obj_obj_obj, curry_obj_obj_map, DepFunctor.map_id, eqToHom_app, + Equiv.toIso_hom, Equiv.coe_fn_mk, types_comp_apply, Sigma.mk.inj_iff, + FunctorToTypes.map_id_apply, true_and] + generalize_proofs + have : F₁.map (𝟙 Γ) b = b := by simp + generalize (eq_lhs% this) = x at *; cases this + have : i.hom.app Γ (i.inv.app Γ b) = b := by simp + generalize (eq_lhs% this) = x at *; cases this + have : i.hom.app Γ (F₂.map (𝟙 Γ) (i.inv.app Γ b)) = b := + by simp [FunctorToTypes.naturality] + generalize (eq_lhs% this) = x at *; cases this + have : F₁.map (𝟙 Γ) b = b := by simp + generalize (eq_lhs% this) = x at *; cases this + simp) + +def Functor.Sigma.isoCongrRight.{v} (F : 𝒞 ⥤ Type v) (G₁ G₂ : DepFunctor F (𝒟 ⥤ Type v)) + (i : ∀ {Γ} (b : F.obj Γ), G₁.obj b ≅ G₂.obj b) + (i_naturality : ∀ {Γ Δ} (σ : Γ ⟶ Δ) (b : F.obj Γ), + (i b).hom ≫ G₂.map σ b = G₁.map σ b ≫ (i (F.map σ b)).hom) : + Functor.Sigma F G₁ ≅ Functor.Sigma F G₂ := + NatIso.ofComponents₂ + (fun Γ X => Equiv.toIso { + toFun := fun ⟨b, e⟩ => ⟨b, (i b).hom.app X e⟩ + invFun := fun ⟨b, e⟩ => ⟨b, (i b).inv.app X e⟩ + left_inv := fun ⟨_, _⟩ => by simp + right_inv := fun ⟨_, _⟩ => by simp + }) + (fun X σ => by + ext ⟨b, e⟩ + dsimp + have := congrFun (congrFun (congrArg NatTrans.app (i_naturality σ b)) X) e + simp at this + simp [Sigma, this] + ) + (fun Γ f => by + ext ⟨b, e⟩ + simp only [Sigma, prod_Hom, curry_obj_obj_obj, curry_obj_obj_map, DepFunctor.map_id, + eqToHom_app, Iso.app_hom, Iso.app_inv, Equiv.toIso_hom, Equiv.coe_fn_mk, types_comp_apply, + Sigma.mk.inj_iff, FunctorToTypes.map_id_apply, heq_eq_eq, true_and] + generalize_proofs + have := F.map_id Γ + generalize (eq_lhs% this) = x at * + cases this + simp [FunctorToTypes.naturality]) + +@[simps] +def bifunctor_comp_snd {𝒟' : Type*} [Category 𝒟'] (F : 𝒟' ⥤ 𝒟) (P : 𝒞 ⥤ 𝒟 ⥤ ℰ) : 𝒞 ⥤ 𝒟' ⥤ ℰ where + obj Γ := F ⋙ P.obj Γ + map σ := whiskerLeft F (P.map σ) + +end CategoryTheory diff --git a/Poly/Tactic/BanishCasts.lean b/Poly/Tactic/BanishCasts.lean new file mode 100644 index 0000000..b4f8c98 --- /dev/null +++ b/Poly/Tactic/BanishCasts.lean @@ -0,0 +1,48 @@ +import Mathlib.Tactic.Basic + +/-! Try to remove cast-like terms from the goal +by turning their equality argument into `refl`. + +Supported cast-like terms: +- `cast` +- `Eq.rec` +- `Eq.mpr` +- `Eq.mp` +- `CategoryTheory.eqToHom` +- `CategoryTheory.eqToIso` + +1. Identify all cast-like terms. +2. For each equality there, identify the differences using `congr`-like operation. +2a. For each difference, try to _prove_ it. + Very often a proof term for the difference will already appear in the goal somewhere: + use a generalized `assumption` tactic that finds such terms. +3. `generalize_proofs` +4. For each difference, generalize the RHS or LHS. + If RHS appears in LHS, generalize LHS; if vice-verse, generalize RHS; + otherwise generalize LHS. +5. Case on the difference with generalized LHS. -/ + +-- assumption' : like assumption but can find proof terms in the goal type +-- or one of the target types + +open Lean Meta Elab Term in +/-- If `h : a = b` (`h : HEq a b`) proves an equality (resp. heterogeneous equality), +`eq_lhs% h` is the left-hand-side `a`. -/ +elab "eq_lhs%" h:term : term => do + let A ← mkFreshTypeMVar + let l ← mkFreshExprMVar A + let r ← mkFreshExprMVar A + let _ ← elabTerm h (← mkAppOptM ``Eq #[A, l, r]) + -- TODO HEq + instantiateMVars l + +open Lean Meta Elab Term in +/-- If `h : a = b` (`h : HEq a b`) proves an equality (resp. heterogeneous equality), +`eq_rhs% h` is the right-hand-side `b`. -/ +elab "eq_rhs%" t:term : term => do + let A ← mkFreshTypeMVar + let l ← mkFreshExprMVar A + let r ← mkFreshExprMVar A + let _ ← elabTerm t (← mkAppOptM ``Eq #[A, l, r]) + -- TODO HEq + instantiateMVars r From a49187e89eb96dcb4270da3736af8e61ab014d0c Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Sun, 24 Nov 2024 00:21:49 -0500 Subject: [PATCH 03/18] feat: more bifunctors --- Poly/Bifunctor.lean | 183 ++++++++++++++++++++++++-------------------- 1 file changed, 102 insertions(+), 81 deletions(-) diff --git a/Poly/Bifunctor.lean b/Poly/Bifunctor.lean index ff27ba9..b46320d 100644 --- a/Poly/Bifunctor.lean +++ b/Poly/Bifunctor.lean @@ -34,38 +34,20 @@ def NatIso.ofComponents₂ {F G : 𝒞 ⥤ 𝒟 ⥤ ℰ} (fun Γ => NatIso.ofComponents (app Γ) (fun f => by simpa using naturality_right Γ f)) (fun σ => by ext X : 2; simpa using naturality_left X σ) --- /-- The bifunctor `(Γ, X) ↦ (b : Γ.unop ⟶ B) × (P.obj (Over.mk b) ⟶ X)`. -/ --- @[simps!] --- def Functor.Sigma_Over.{v} [Category.{v} 𝒟] {B : 𝒞} (P : Over B ⥤ 𝒟) : 𝒞ᵒᵖ ⥤ 𝒟 ⥤ Type v := --- curry.obj { --- obj := fun (Γ, X) => (b : Γ.unop ⟶ B) × (P.obj (Over.mk b) ⟶ X) --- map := fun (σ, f) ⟨b, e⟩ => --- ⟨σ.unop ≫ b, --- P.map (Over.homMk (V := Over.mk b) σ.unop (by simp)) ≫ e ≫ f⟩ --- map_id := fun (Γ, X) => by --- refine funext fun _ => ?_ --- apply Sigma_hom_ext --- . simp [eqToHom_map] --- . dsimp --- intro h --- rw [← Over.eqToHom_eq_homMk (eq := h)] --- simp [eqToHom_map] --- map_comp := fun {_} {_} {Y} (σ, f) (τ, g) => by --- refine funext fun ⟨b, e⟩ => ?_ --- apply Sigma_hom_ext --- . simp --- . dsimp --- intro h --- rw [Over.homMk_comp (U := Over.mk ((τ.unop ≫ σ.unop) ≫ b)) (V := Over.mk (σ.unop ≫ b)) --- (f_comp := by simp) (g_comp := by simp)] --- generalize_proofs -- I <3 generalize_proofs --- generalize (τ.unop ≫ σ.unop) ≫ b = x at * --- cases h --- simp --- } - -/-- A functor into `𝒟` that depends on `F`. -/ --- TODO: does this correspond to a known construction? +/-! ## Dependent functors -/ + +/-- A functor into `𝒟` that depends on `F`. + +This is a functor `G : ∫F ⥤ 𝒟` where all the `F(Γ)` are discrete, +spelled out in elementary terms. +In the general case, we would have +`map : ∀ ⦃Γ Δ⦄ ⦃b : F.obj Γ⦄ ⦃c : F.obj Δ⦄ + (σ : Γ ⟶ Δ) (f : (F.map σ).obj b ⟶ c), obj b ⟶ obj c`. + +Equivalently, it is a (lax or strict or something) transformation `F ⟶ const 𝒟`. -/ +-- NOTE: A more mathlib-ready, general approach might use `∫F ⥤ 𝒟`, +-- and introduce a special-case constructor for discrete `F(Γ)` +-- with an argument for each field of this structure. -/ structure DepFunctor (F : 𝒞 ⥤ Type*) (𝒟 : Type*) [Category 𝒟] where obj : ∀ ⦃Γ⦄, F.obj Γ → 𝒟 map : ∀ ⦃Γ Δ⦄ (σ : Γ ⟶ Δ) (b : F.obj Γ), obj b ⟶ obj (F.map σ b) @@ -86,32 +68,84 @@ def DepFunctor.isoLeft.{v} {F₁ F₂ : 𝒞 ⥤ Type v} {𝒟 : Type*} [Categor slice_rhs 2 3 => rw [← eqToHom_naturality _ (by simp [FunctorToTypes.naturality])] simp +@[ext] structure DepNatTrans {F : 𝒞 ⥤ Type*} {𝒟 : Type*} [Category 𝒟] (G₁ G₂ : DepFunctor F 𝒟) where - app : ∀ {Γ} (b : F.obj Γ), G₁.obj b ⟶ G₂.obj b - naturality : ∀ {Γ Δ} (σ : Γ ⟶ Δ) (b : F.obj Γ), - app b ≫ G₂.map σ b = G₁.map σ b ≫ app (F.map σ b) + app : ∀ ⦃Γ⦄ (b : F.obj Γ), G₁.obj b ⟶ G₂.obj b + naturality : ∀ ⦃Γ Δ⦄ (σ : Γ ⟶ Δ) (b : F.obj Γ), + app b ≫ G₂.map σ b = G₁.map σ b ≫ app (F.map σ b) := by aesop_cat attribute [reassoc] DepNatTrans.naturality +@[simps] instance (F : 𝒞 ⥤ Type*) (𝒟 : Type*) [Category 𝒟] : Category (DepFunctor F 𝒟) where Hom := DepNatTrans - id G := { - app := fun _ => 𝟙 _ - naturality := by simp - } + id G := { app := fun _ _ => 𝟙 _ } comp η ν := { - app := fun b => η.app b ≫ ν.app b + app := fun _ b => η.app b ≫ ν.app b naturality := by simp [η.naturality_assoc, ν.naturality] } - id_comp := by simp - comp_id := by simp - assoc := by simp --- TODO: characterize isos in the above category as these things -structure DepNatIso (F : 𝒞 ⥤ Type*) {𝒟 : Type*} [Category 𝒟] (G₁ G₂ : DepFunctor F 𝒟) where - i : ∀ {Γ} (b : F.obj Γ), G₁.obj b ≅ G₂.obj b - i_naturality : ∀ {Γ Δ} (σ : Γ ⟶ Δ) (b : F.obj Γ), - (i b).hom ≫ G₂.map σ b = G₁.map σ b ≫ (i (F.map σ b)).hom +namespace DepNatTrans + +variable {F : 𝒞 ⥤ Type*} {𝒟 : Type*} [Category 𝒟] {Γ : 𝒞} (b : F.obj Γ) + +@[ext] +theorem ext' {G₁ G₂ : DepFunctor F 𝒟} {α β : G₁ ⟶ G₂} (w : α.app = β.app) : α = β := + DepNatTrans.ext w + +@[simp] +theorem id_app (G₁ : DepFunctor F 𝒟) : (𝟙 G₁ : G₁ ⟶ G₁).app b = 𝟙 (G₁.obj b) := rfl + +@[reassoc (attr := simp)] +theorem comp_app {G₁ G₂ G₃ : DepFunctor F 𝒟} (α : G₁ ⟶ G₂) (β : G₂ ⟶ G₃) : + (α ≫ β).app b = α.app b ≫ β.app b := rfl + +@[reassoc] +theorem naturality_app {ℰ : Type*} [Category ℰ] {G₁ G₂ : DepFunctor F (𝒟 ⥤ ℰ)} (α : G₁ ⟶ G₂) + {Γ Δ : 𝒞} (σ : Γ ⟶ Δ) (b : F.obj Γ) (X : 𝒟) : + (G₁.map σ b).app X ≫ (α.app (F.map σ b)).app X = (α.app b).app X ≫ (G₂.map σ b).app X := + (congr_fun (congr_arg NatTrans.app (α.naturality σ b)) X).symm + +end DepNatTrans + +namespace DepNatIso + +variable {F : 𝒞 ⥤ Type*} {𝒟 : Type*} [Category 𝒟] {G₁ G₂ : DepFunctor F 𝒟} + +@[reassoc (attr := simp)] +theorem hom_inv_id_app {Γ : 𝒞} (α : G₁ ≅ G₂) (b : F.obj Γ) : + α.hom.app b ≫ α.inv.app b = 𝟙 (G₁.obj b) := by + simp [← DepNatTrans.comp_app] + +@[reassoc (attr := simp)] +theorem inv_hom_id_app {Γ : 𝒞} (α : G₁ ≅ G₂) (b : F.obj Γ) : + α.inv.app b ≫ α.hom.app b = 𝟙 (G₂.obj b) := by + simp [← DepNatTrans.comp_app] + +instance hom_app_isIso {Γ : 𝒞} (α : G₁ ≅ G₂) (b : F.obj Γ) : IsIso (α.hom.app b) := + ⟨α.inv.app b, by simp⟩ + +instance inv_app_isIso {Γ : 𝒞} (α : G₁ ≅ G₂) (b : F.obj Γ) : IsIso (α.inv.app b) := + ⟨α.hom.app b, by simp⟩ + +def ofComponents + (app : ∀ {Γ} (b : F.obj Γ), G₁.obj b ≅ G₂.obj b) + (naturality : ∀ {Γ Δ} (σ : Γ ⟶ Δ) (b : F.obj Γ), + (app b).hom ≫ G₂.map σ b = G₁.map σ b ≫ (app (F.map σ b)).hom) : + G₁ ≅ G₂ where + hom := { app := fun _ b => (app b).hom } + inv := { + app := fun _ b => (app b).inv + naturality := fun _ _ σ b => by + have : (app b).inv ≫ (app b).hom ≫ G₂.map σ b ≫ (app (F.map σ b)).inv = + (app b).inv ≫ G₁.map σ b ≫ (app (F.map σ b)).hom ≫ (app (F.map σ b)).inv := by + simp [reassoc_of% naturality] + simpa using this.symm + } + +end DepNatIso + +/-! ## Dependent sum functors -/ /-- Dependent sum over a type-valued functor. This serves to encapsulate dependent sums that vary naturally in their parameters. -/ @@ -129,8 +163,7 @@ def Functor.Sigma.{v} (F : 𝒞 ⥤ Type v) (G : DepFunctor F (𝒟 ⥤ Type v)) . simp . simp only [FunctorToTypes.map_id_apply, DepFunctor.map_id] generalize_proofs - generalize (eq_lhs% h) = x at * - cases h + generalize (eq_lhs% h) = x at *; cases h simp map_comp := fun {_} {_} {Y} (σ, f) (τ, g) => by refine funext fun ⟨b, e⟩ => ?_ @@ -139,30 +172,15 @@ def Functor.Sigma.{v} (F : 𝒞 ⥤ Type v) (G : DepFunctor F (𝒟 ⥤ Type v)) . simp . simp only [FunctorToTypes.map_comp_apply, DepFunctor.map_comp] generalize_proofs - generalize (eq_lhs% h) = x at * - cases h + generalize (eq_lhs% h) = x at *; cases h simp [FunctorToTypes.naturality] } --- Not super important, we don't need to treat b as an over-category element ever. --- @[simps!] --- def Functor.Sigma_Over'.{v} [Category.{v} 𝒟] {B : 𝒞} (P : Over B ⥤ 𝒟) : 𝒞ᵒᵖ ⥤ 𝒟 ⥤ Type v := --- Functor.Sigma (yoneda.obj B) (fun b => coyoneda.obj $ Opposite.op $ P.obj $ Over.mk b) --- (fun σ b => { app := fun _ e => P.map (Over.homMk (V := Over.mk b) σ.unop (by simp)) ≫ e }) --- (fun b => by --- ext X b --- simp only [eqToHom_app, coyoneda_obj_obj, yoneda_obj_map, unop_id] at b ⊢ --- generalize_proofs pf1 pf2 --- sorry --- -- etc --- ) --- (fun σ τ b => sorry) - def Functor.Sigma.isoCongrLeft.{v} (F₁ F₂ : 𝒞 ⥤ Type v) (G : DepFunctor F₁ (𝒟 ⥤ Type v)) (i : F₂ ≅ F₁) : Functor.Sigma F₁ G ≅ Functor.Sigma F₂ (G.isoLeft i) := NatIso.ofComponents₂ (fun Γ X => Equiv.toIso { - toFun := fun ⟨b, e⟩ => ⟨i.inv.app Γ b, cast (by simp) e⟩ + toFun := fun ⟨b, e⟩ => ⟨i.inv.app Γ b, cast (by simp) e⟩ -- `dcast` could be better here invFun := fun ⟨b, e⟩ => ⟨i.hom.app Γ b, e⟩ left_inv := fun ⟨_, _⟩ => by simp right_inv := fun ⟨_, _⟩ => by simp @@ -201,24 +219,28 @@ def Functor.Sigma.isoCongrLeft.{v} (F₁ F₂ : 𝒞 ⥤ Type v) (G : DepFunctor simp) def Functor.Sigma.isoCongrRight.{v} (F : 𝒞 ⥤ Type v) (G₁ G₂ : DepFunctor F (𝒟 ⥤ Type v)) - (i : ∀ {Γ} (b : F.obj Γ), G₁.obj b ≅ G₂.obj b) - (i_naturality : ∀ {Γ Δ} (σ : Γ ⟶ Δ) (b : F.obj Γ), - (i b).hom ≫ G₂.map σ b = G₁.map σ b ≫ (i (F.map σ b)).hom) : + (i : G₁ ≅ G₂) : Functor.Sigma F G₁ ≅ Functor.Sigma F G₂ := NatIso.ofComponents₂ (fun Γ X => Equiv.toIso { - toFun := fun ⟨b, e⟩ => ⟨b, (i b).hom.app X e⟩ - invFun := fun ⟨b, e⟩ => ⟨b, (i b).inv.app X e⟩ - left_inv := fun ⟨_, _⟩ => by simp - right_inv := fun ⟨_, _⟩ => by simp + toFun := fun ⟨b, e⟩ => ⟨b, (i.hom.app b).app X e⟩ + invFun := fun ⟨b, e⟩ => ⟨b, (i.inv.app b).app X e⟩ + left_inv := fun ⟨b, e⟩ => by + -- simp doesn't finish this. missing simp lemma? + have := congr_fun (congr_fun (congr_arg NatTrans.app (DepNatIso.hom_inv_id_app i b)) X) e + simp + simp only [NatTrans.comp_app] at this + simpa using this + right_inv := fun ⟨b, e⟩ => by + have := congr_fun (congr_fun (congr_arg NatTrans.app (DepNatIso.inv_hom_id_app i b)) X) e + simp only [NatTrans.comp_app] at this + simpa using this }) (fun X σ => by ext ⟨b, e⟩ - dsimp - have := congrFun (congrFun (congrArg NatTrans.app (i_naturality σ b)) X) e - simp at this - simp [Sigma, this] - ) + have := congr_fun (DepNatTrans.naturality_app i.hom σ b X) e + dsimp at this + simp [Sigma, this]) (fun Γ f => by ext ⟨b, e⟩ simp only [Sigma, prod_Hom, curry_obj_obj_obj, curry_obj_obj_map, DepFunctor.map_id, @@ -226,8 +248,7 @@ def Functor.Sigma.isoCongrRight.{v} (F : 𝒞 ⥤ Type v) (G₁ G₂ : DepFuncto Sigma.mk.inj_iff, FunctorToTypes.map_id_apply, heq_eq_eq, true_and] generalize_proofs have := F.map_id Γ - generalize (eq_lhs% this) = x at * - cases this + generalize (eq_lhs% this) = x at *; cases this simp [FunctorToTypes.naturality]) @[simps] From c03c0ff529374db03bb232fdf71ded705fcb2f68 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Fri, 29 Nov 2024 22:05:20 -0500 Subject: [PATCH 04/18] feat: pullback functor --- Poly/Bifunctor.lean | 28 ++++++++++++++++++++++++++-- 1 file changed, 26 insertions(+), 2 deletions(-) diff --git a/Poly/Bifunctor.lean b/Poly/Bifunctor.lean index b46320d..e156baa 100644 --- a/Poly/Bifunctor.lean +++ b/Poly/Bifunctor.lean @@ -51,9 +51,9 @@ Equivalently, it is a (lax or strict or something) transformation `F ⟶ const structure DepFunctor (F : 𝒞 ⥤ Type*) (𝒟 : Type*) [Category 𝒟] where obj : ∀ ⦃Γ⦄, F.obj Γ → 𝒟 map : ∀ ⦃Γ Δ⦄ (σ : Γ ⟶ Δ) (b : F.obj Γ), obj b ⟶ obj (F.map σ b) - map_id : ∀ ⦃Γ⦄ (b : F.obj Γ), map (𝟙 Γ) b = eqToHom (F.map_id _ ▸ rfl) + map_id : ∀ ⦃Γ⦄ (b : F.obj Γ), map (𝟙 Γ) b = eqToHom (F.map_id _ ▸ rfl) := by aesop_cat map_comp : ∀ ⦃Γ Δ Θ⦄ (σ : Γ ⟶ Δ) (τ : Δ ⟶ Θ) (b : F.obj Γ), - map (σ ≫ τ) b = map σ b ≫ map τ (F.map σ b) ≫ eqToHom (F.map_comp .. ▸ rfl) + map (σ ≫ τ) b = map σ b ≫ map τ (F.map σ b) ≫ eqToHom (F.map_comp .. ▸ rfl) := by aesop_cat attribute [reassoc] DepFunctor.map_comp attribute [simp] DepFunctor.map_id DepFunctor.map_comp DepFunctor.map_comp_assoc @@ -251,6 +251,30 @@ def Functor.Sigma.isoCongrRight.{v} (F : 𝒞 ⥤ Type v) (G₁ G₂ : DepFuncto generalize (eq_lhs% this) = x at *; cases this simp [FunctorToTypes.naturality]) +open Limits in +/-- The functor `(b : Γ ⟶ B) ↦ b*σ`. -/ +noncomputable def pullbackDep.{v} {𝒞 : Type*} [Category.{v} 𝒞] [HasPullbacks 𝒞] {E B : 𝒞} (p : E ⟶ B) : + DepFunctor (yoneda.obj B) (𝒞 ⥤ Type v) where + obj _ b := coyoneda.obj <| Opposite.op <| pullback b p + map _ _ σ _ := + coyoneda.map <| Quiver.Hom.op <| + pullback.lift (pullback.fst .. ≫ σ.unop) (pullback.snd ..) (by simp [pullback.condition]) + map_id _ b := by + dsimp + -- More `eqToHom` nonsense + generalize_proofs + have : 𝟙 _ ≫ b = b := by simp + generalize (eq_lhs% this) = x at *; cases this + simp + map_comp _ _ _ σ τ b := by + dsimp + generalize_proofs + have : τ.unop ≫ σ.unop ≫ b = (τ.unop ≫ σ.unop) ≫ b := by simp + generalize (eq_lhs% this) = x at *; cases this + simp [← Functor.map_comp, ← op_comp] + congr 2 + ext <;> simp + @[simps] def bifunctor_comp_snd {𝒟' : Type*} [Category 𝒟'] (F : 𝒟' ⥤ 𝒟) (P : 𝒞 ⥤ 𝒟 ⥤ ℰ) : 𝒞 ⥤ 𝒟' ⥤ ℰ where obj Γ := F ⋙ P.obj Γ From bec4828683b64544e279a728e1b763ac9a5ee215 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Fri, 7 Mar 2025 01:11:34 -0500 Subject: [PATCH 05/18] feat: use rw! --- Poly/Bifunctor.lean | 82 ++++++++++++++++++--------------------------- lake-manifest.json | 12 ++++++- lakefile.lean | 2 ++ 3 files changed, 46 insertions(+), 50 deletions(-) diff --git a/Poly/Bifunctor.lean b/Poly/Bifunctor.lean index e156baa..31fcdee 100644 --- a/Poly/Bifunctor.lean +++ b/Poly/Bifunctor.lean @@ -3,6 +3,8 @@ import Mathlib.CategoryTheory.Functor.Currying import Poly.Util import Poly.Tactic.BanishCasts +import SEq.Tactic.DepRewrite + /-! # Bifunctors We define some constructions on bifunctors (aka profunctors), @@ -16,7 +18,7 @@ F(X) ⟶ G(Y) H(X) ⟶ I(Y) ``` would be a natural isomorphism of bifunctors `𝒞ᵒᵖ ⥤ 𝒟 ⥤ Type v` -given by `(X,Y) ↦ F(X) ⟶ G(Y)` and `(X, Y) ↦ H(X) ⟶ I(Y)`. -/ +given by `(X, Y) ↦ F(X) ⟶ G(Y)` and `(X, Y) ↦ H(X) ⟶ I(Y)`. -/ namespace CategoryTheory @@ -36,13 +38,13 @@ def NatIso.ofComponents₂ {F G : 𝒞 ⥤ 𝒟 ⥤ ℰ} /-! ## Dependent functors -/ -/-- A functor into `𝒟` that depends on `F`. - -This is a functor `G : ∫F ⥤ 𝒟` where all the `F(Γ)` are discrete, +/-- A functor into `𝒟` that depends on `F`, +in other words `∫F ⥤ 𝒟` where all the `F(Γ)` are discrete, spelled out in elementary terms. -In the general case, we would have + +(In the general case, we would have `map : ∀ ⦃Γ Δ⦄ ⦃b : F.obj Γ⦄ ⦃c : F.obj Δ⦄ - (σ : Γ ⟶ Δ) (f : (F.map σ).obj b ⟶ c), obj b ⟶ obj c`. + (σ : Γ ⟶ Δ) (f : F.map σ b ⟶ c), obj b ⟶ obj c`.) Equivalently, it is a (lax or strict or something) transformation `F ⟶ const 𝒟`. -/ -- NOTE: A more mathlib-ready, general approach might use `∫F ⥤ 𝒟`, @@ -147,40 +149,39 @@ end DepNatIso /-! ## Dependent sum functors -/ -/-- Dependent sum over a type-valued functor. -This serves to encapsulate dependent sums that vary naturally in their parameters. -/ + +/-- Given functors `F : 𝒞 ⥤ Type v` and `G : ∫F ⥤ 𝒟 ⥤ Type v`, +produce the functor `(X, Y) ↦ (b : F(X)) × G((X, b))(Y)`. +This is a dependent sum that varies naturally in its parameters `X, Y`. -/ @[simps!] -def Functor.Sigma.{v} (F : 𝒞 ⥤ Type v) (G : DepFunctor F (𝒟 ⥤ Type v)) : 𝒞 ⥤ 𝒟 ⥤ Type v := +def Functor.Sigma.{v} {F : 𝒞 ⥤ Type v} (G : DepFunctor F (𝒟 ⥤ Type v)) : 𝒞 ⥤ 𝒟 ⥤ Type v := curry.obj { obj := fun (Γ, X) => (b : F.obj Γ) × ((G.obj b).obj X) map := fun (σ, f) ⟨b, e⟩ => ⟨F.map σ b, (G.map σ b).app _ ((G.obj b).map f e)⟩ map_id := fun (Γ, X) => by - dsimp refine funext fun ⟨b, e⟩ => ?_ - dsimp at * + dsimp congr! 1 with h . simp . simp only [FunctorToTypes.map_id_apply, DepFunctor.map_id] - generalize_proofs - generalize (eq_lhs% h) = x at *; cases h + rw! [h] simp map_comp := fun {_} {_} {Y} (σ, f) (τ, g) => by refine funext fun ⟨b, e⟩ => ?_ - dsimp at * + dsimp congr! 1 with h . simp . simp only [FunctorToTypes.map_comp_apply, DepFunctor.map_comp] - generalize_proofs - generalize (eq_lhs% h) = x at *; cases h + rw! [h] simp [FunctorToTypes.naturality] } def Functor.Sigma.isoCongrLeft.{v} (F₁ F₂ : 𝒞 ⥤ Type v) (G : DepFunctor F₁ (𝒟 ⥤ Type v)) - (i : F₂ ≅ F₁) : Functor.Sigma F₁ G ≅ Functor.Sigma F₂ (G.isoLeft i) := + (i : F₂ ≅ F₁) : Functor.Sigma G ≅ Functor.Sigma (G.isoLeft i) := NatIso.ofComponents₂ (fun Γ X => Equiv.toIso { - toFun := fun ⟨b, e⟩ => ⟨i.inv.app Γ b, cast (by simp) e⟩ -- `dcast` could be better here + toFun := fun ⟨b, e⟩ => ⟨i.inv.app Γ b, cast (by simp) e⟩ invFun := fun ⟨b, e⟩ => ⟨i.hom.app Γ b, e⟩ left_inv := fun ⟨_, _⟩ => by simp right_inv := fun ⟨_, _⟩ => by simp @@ -191,14 +192,10 @@ def Functor.Sigma.isoCongrLeft.{v} (F₁ F₂ : 𝒞 ⥤ Type v) (G : DepFunctor FunctorToTypes.comp, curry_obj_obj_obj, curry_obj_map_app, FunctorToTypes.map_id_apply, Equiv.toIso_hom, Equiv.coe_fn_mk, types_comp_apply, eqToHom_app, Sigma.mk.inj_iff, FunctorToTypes.naturality, true_and] - generalize_proofs -- TODO: banish_casts tactic have : (i.hom.app _ (F₂.map σ (i.inv.app _ b))) = F₁.map σ b := by simp [FunctorToTypes.naturality] - generalize (eq_lhs% this) = x at *; cases this - have := FunctorToTypes.inv_hom_id_app_apply _ _ i _ (F₁.map σ b) - generalize (eq_lhs% this) = x at *; cases this - have := FunctorToTypes.inv_hom_id_app_apply _ _ i _ b - generalize (eq_lhs% this) = x at *; cases this + rw! (castMode := .all) [this, FunctorToTypes.inv_hom_id_app_apply _ _ i _ (F₁.map σ b), + FunctorToTypes.inv_hom_id_app_apply _ _ i _ b] simp) (fun Γ f => by ext ⟨b,e⟩ @@ -206,21 +203,15 @@ def Functor.Sigma.isoCongrLeft.{v} (F₁ F₂ : 𝒞 ⥤ Type v) (G : DepFunctor FunctorToTypes.comp, curry_obj_obj_obj, curry_obj_obj_map, DepFunctor.map_id, eqToHom_app, Equiv.toIso_hom, Equiv.coe_fn_mk, types_comp_apply, Sigma.mk.inj_iff, FunctorToTypes.map_id_apply, true_and] - generalize_proofs - have : F₁.map (𝟙 Γ) b = b := by simp - generalize (eq_lhs% this) = x at *; cases this - have : i.hom.app Γ (i.inv.app Γ b) = b := by simp - generalize (eq_lhs% this) = x at *; cases this - have : i.hom.app Γ (F₂.map (𝟙 Γ) (i.inv.app Γ b)) = b := - by simp [FunctorToTypes.naturality] - generalize (eq_lhs% this) = x at *; cases this - have : F₁.map (𝟙 Γ) b = b := by simp - generalize (eq_lhs% this) = x at *; cases this + rw! (castMode := .all) [show F₁.map (𝟙 Γ) b = b by simp, + show i.hom.app Γ (i.inv.app Γ b) = b by simp, + show i.hom.app Γ (F₂.map (𝟙 Γ) (i.inv.app Γ b)) = b by simp [FunctorToTypes.naturality], + show F₁.map (𝟙 Γ) b = b by simp] simp) def Functor.Sigma.isoCongrRight.{v} (F : 𝒞 ⥤ Type v) (G₁ G₂ : DepFunctor F (𝒟 ⥤ Type v)) (i : G₁ ≅ G₂) : - Functor.Sigma F G₁ ≅ Functor.Sigma F G₂ := + Functor.Sigma G₁ ≅ Functor.Sigma G₂ := NatIso.ofComponents₂ (fun Γ X => Equiv.toIso { toFun := fun ⟨b, e⟩ => ⟨b, (i.hom.app b).app X e⟩ @@ -228,7 +219,6 @@ def Functor.Sigma.isoCongrRight.{v} (F : 𝒞 ⥤ Type v) (G₁ G₂ : DepFuncto left_inv := fun ⟨b, e⟩ => by -- simp doesn't finish this. missing simp lemma? have := congr_fun (congr_fun (congr_arg NatTrans.app (DepNatIso.hom_inv_id_app i b)) X) e - simp simp only [NatTrans.comp_app] at this simpa using this right_inv := fun ⟨b, e⟩ => by @@ -246,13 +236,11 @@ def Functor.Sigma.isoCongrRight.{v} (F : 𝒞 ⥤ Type v) (G₁ G₂ : DepFuncto simp only [Sigma, prod_Hom, curry_obj_obj_obj, curry_obj_obj_map, DepFunctor.map_id, eqToHom_app, Iso.app_hom, Iso.app_inv, Equiv.toIso_hom, Equiv.coe_fn_mk, types_comp_apply, Sigma.mk.inj_iff, FunctorToTypes.map_id_apply, heq_eq_eq, true_and] - generalize_proofs - have := F.map_id Γ - generalize (eq_lhs% this) = x at *; cases this + rw! [F.map_id Γ] simp [FunctorToTypes.naturality]) open Limits in -/-- The functor `(b : Γ ⟶ B) ↦ b*σ`. -/ +/-- The functor `(b : Γ ⟶ B) ↦ Hom(dom(b*p), -)`. -/ noncomputable def pullbackDep.{v} {𝒞 : Type*} [Category.{v} 𝒞] [HasPullbacks 𝒞] {E B : 𝒞} (p : E ⟶ B) : DepFunctor (yoneda.obj B) (𝒞 ⥤ Type v) where obj _ b := coyoneda.obj <| Opposite.op <| pullback b p @@ -261,18 +249,14 @@ noncomputable def pullbackDep.{v} {𝒞 : Type*} [Category.{v} 𝒞] [HasPullbac pullback.lift (pullback.fst .. ≫ σ.unop) (pullback.snd ..) (by simp [pullback.condition]) map_id _ b := by dsimp - -- More `eqToHom` nonsense - generalize_proofs - have : 𝟙 _ ≫ b = b := by simp - generalize (eq_lhs% this) = x at *; cases this + rw! [show 𝟙 _ ≫ b = b by simp] simp map_comp _ _ _ σ τ b := by + ext dsimp - generalize_proofs - have : τ.unop ≫ σ.unop ≫ b = (τ.unop ≫ σ.unop) ≫ b := by simp - generalize (eq_lhs% this) = x at *; cases this - simp [← Functor.map_comp, ← op_comp] - congr 2 + rw! [show τ.unop ≫ σ.unop ≫ b = (τ.unop ≫ σ.unop) ≫ b by simp] + simp only [← Category.assoc] + congr 1 ext <;> simp @[simps] diff --git a/lake-manifest.json b/lake-manifest.json index c855062..746537a 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -1,7 +1,17 @@ {"version": "1.1.0", "packagesDir": ".lake/packages", "packages": - [{"url": "https://github.com/leanprover-community/mathlib4.git", + [{"url": "https://github.com/Vtec234/lean4-seq", + "type": "git", + "subDir": null, + "scope": "", + "rev": "b6b76a5d7cc1c8b11c52f12a7bd90c460b7cba5a", + "name": "seq", + "manifestFile": "lake-manifest.json", + "inputRev": null, + "inherited": false, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/mathlib4.git", "type": "git", "subDir": null, "scope": "", diff --git a/lakefile.lean b/lakefile.lean index d49f5c4..c6f3ad7 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -11,6 +11,8 @@ package «Poly» where require mathlib from git "https://github.com/leanprover-community/mathlib4.git" +require seq from git "https://github.com/Vtec234/lean4-seq" + @[default_target] lean_lib «Poly» where -- add any library configuration options here From 2cda39f3307a827655cd560c216a300184562404 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Tue, 11 Mar 2025 15:53:13 -0400 Subject: [PATCH 06/18] feat: fording & Over equivalence --- Poly/Bifunctor.lean | 235 +++++++++++++++++++++-------------- Poly/Tactic/BanishCasts.lean | 48 ------- 2 files changed, 142 insertions(+), 141 deletions(-) delete mode 100644 Poly/Tactic/BanishCasts.lean diff --git a/Poly/Bifunctor.lean b/Poly/Bifunctor.lean index 31fcdee..31da129 100644 --- a/Poly/Bifunctor.lean +++ b/Poly/Bifunctor.lean @@ -1,7 +1,6 @@ import Mathlib.CategoryTheory.Functor.Currying import Poly.Util -import Poly.Tactic.BanishCasts import SEq.Tactic.DepRewrite @@ -52,29 +51,40 @@ Equivalently, it is a (lax or strict or something) transformation `F ⟶ const -- with an argument for each field of this structure. -/ structure DepFunctor (F : 𝒞 ⥤ Type*) (𝒟 : Type*) [Category 𝒟] where obj : ∀ ⦃Γ⦄, F.obj Γ → 𝒟 - map : ∀ ⦃Γ Δ⦄ (σ : Γ ⟶ Δ) (b : F.obj Γ), obj b ⟶ obj (F.map σ b) - map_id : ∀ ⦃Γ⦄ (b : F.obj Γ), map (𝟙 Γ) b = eqToHom (F.map_id _ ▸ rfl) := by aesop_cat - map_comp : ∀ ⦃Γ Δ Θ⦄ (σ : Γ ⟶ Δ) (τ : Δ ⟶ Θ) (b : F.obj Γ), - map (σ ≫ τ) b = map σ b ≫ map τ (F.map σ b) ≫ eqToHom (F.map_comp .. ▸ rfl) := by aesop_cat - -attribute [reassoc] DepFunctor.map_comp -attribute [simp] DepFunctor.map_id DepFunctor.map_comp DepFunctor.map_comp_assoc + -- Forded to avoid `eqToHom` in the axioms. + map : ∀ ⦃Γ Δ⦄ (σ : Γ ⟶ Δ) (b : F.obj Γ) (c : F.obj Δ), c = F.map σ b → (obj b ⟶ obj c) + map_id : ∀ ⦃Γ⦄ b h, map (𝟙 Γ) b b h = 𝟙 (obj b) := by aesop_cat + /-- ### `simp` + The two `map` equalities in the LHS imply the one in the RHS, but not vice-versa. + This axiom is thus stated in a "packing" rather than an "unpacking" direction, + so that `simp` can apply it automatically by matching `h₁` and `h₂`. + However, we do not mark it `simp`; + instead, a special case in the "unpacking" direction is `simp`. -/ + map_comp : ∀ ⦃Γ Δ Θ⦄ (σ : Γ ⟶ Δ) (τ : Δ ⟶ Θ) b c d h₁ h₂, + map σ b c h₁ ≫ map τ c d h₂ = map (σ ≫ τ) b d (by simp [h₁, h₂]) := by aesop_cat + +attribute [simp] DepFunctor.map_id + +/-- Specialized variant of `map_comp` that `simp` can match against. -/ +@[simp] +theorem DepFunctor.map_comp' {F : 𝒞 ⥤ Type*} {G : DepFunctor F 𝒟} + ⦃Γ Δ Θ⦄ (σ : Γ ⟶ Δ) (τ : Δ ⟶ Θ) b h : + G.map (σ ≫ τ) b (F.map τ (F.map σ b)) h = G.map σ b (F.map σ b) rfl ≫ G.map τ _ _ rfl := + (G.map_comp σ τ ..).symm @[simps] def DepFunctor.isoLeft.{v} {F₁ F₂ : 𝒞 ⥤ Type v} {𝒟 : Type*} [Category 𝒟] - (F : DepFunctor F₁ 𝒟) (i : F₂ ≅ F₁) : DepFunctor F₂ 𝒟 where - obj Γ b := F.obj (i.hom.app Γ b) - map Γ _ σ b := F.map σ (i.hom.app Γ b) ≫ eqToHom (FunctorToTypes.naturality F₂ F₁ i.hom .. ▸ rfl) - map_id _ b := by simp - map_comp _ _ _ σ τ b := by - slice_rhs 2 3 => rw [← eqToHom_naturality _ (by simp [FunctorToTypes.naturality])] - simp + (G : DepFunctor F₁ 𝒟) (i : F₂ ≅ F₁) : DepFunctor F₂ 𝒟 where + obj Γ b := G.obj (i.hom.app Γ b) + map Γ _ σ _ _ eq := G.map σ _ _ (by simp [eq, FunctorToTypes.naturality]) + map_id := by simp + map_comp := by simp [G.map_comp] @[ext] structure DepNatTrans {F : 𝒞 ⥤ Type*} {𝒟 : Type*} [Category 𝒟] (G₁ G₂ : DepFunctor F 𝒟) where app : ∀ ⦃Γ⦄ (b : F.obj Γ), G₁.obj b ⟶ G₂.obj b - naturality : ∀ ⦃Γ Δ⦄ (σ : Γ ⟶ Δ) (b : F.obj Γ), - app b ≫ G₂.map σ b = G₁.map σ b ≫ app (F.map σ b) := by aesop_cat + naturality : ∀ ⦃Γ Δ⦄ (σ : Γ ⟶ Δ) (b : F.obj Γ) (c : F.obj Δ) h, + app b ≫ G₂.map σ b c h = G₁.map σ b c h ≫ app c := by aesop_cat attribute [reassoc] DepNatTrans.naturality @@ -104,9 +114,9 @@ theorem comp_app {G₁ G₂ G₃ : DepFunctor F 𝒟} (α : G₁ ⟶ G₂) (β : @[reassoc] theorem naturality_app {ℰ : Type*} [Category ℰ] {G₁ G₂ : DepFunctor F (𝒟 ⥤ ℰ)} (α : G₁ ⟶ G₂) - {Γ Δ : 𝒞} (σ : Γ ⟶ Δ) (b : F.obj Γ) (X : 𝒟) : - (G₁.map σ b).app X ≫ (α.app (F.map σ b)).app X = (α.app b).app X ≫ (G₂.map σ b).app X := - (congr_fun (congr_arg NatTrans.app (α.naturality σ b)) X).symm + {Γ Δ : 𝒞} (σ : Γ ⟶ Δ) (b : F.obj Γ) (c : F.obj Δ) h (X : 𝒟) : + (G₁.map σ b c h).app X ≫ (α.app c).app X = (α.app b).app X ≫ (G₂.map σ b c h).app X := + (congr_fun (congr_arg NatTrans.app (α.naturality σ b c h)) X).symm end DepNatTrans @@ -132,82 +142,89 @@ instance inv_app_isIso {Γ : 𝒞} (α : G₁ ≅ G₂) (b : F.obj Γ) : IsIso ( def ofComponents (app : ∀ {Γ} (b : F.obj Γ), G₁.obj b ≅ G₂.obj b) - (naturality : ∀ {Γ Δ} (σ : Γ ⟶ Δ) (b : F.obj Γ), - (app b).hom ≫ G₂.map σ b = G₁.map σ b ≫ (app (F.map σ b)).hom) : + (naturality : ∀ {Γ Δ} (σ : Γ ⟶ Δ) (b : F.obj Γ) (c : F.obj Δ) h, + (app b).hom ≫ G₂.map σ b c h = G₁.map σ b c h ≫ (app c).hom) : G₁ ≅ G₂ where hom := { app := fun _ b => (app b).hom } inv := { app := fun _ b => (app b).inv - naturality := fun _ _ σ b => by - have : (app b).inv ≫ (app b).hom ≫ G₂.map σ b ≫ (app (F.map σ b)).inv = - (app b).inv ≫ G₁.map σ b ≫ (app (F.map σ b)).hom ≫ (app (F.map σ b)).inv := by + naturality := fun _ _ σ b c h => by + have : (app b).inv ≫ (app b).hom ≫ G₂.map σ b c h ≫ (app c).inv = + (app b).inv ≫ G₁.map σ b c h ≫ (app c).hom ≫ (app c).inv := by simp [reassoc_of% naturality] simpa using this.symm } +variable {G₁ G₂ : DepFunctor F (Type v)} + +@[simp] +theorem hom_inv_id_app_apply {Γ : 𝒞} (α : G₁ ≅ G₂) (X : F.obj Γ) (x) : + α.inv.app X (α.hom.app X x) = x := + congr_fun (hom_inv_id_app α X) x + +@[simp] +theorem inv_hom_id_app_apply {Γ : 𝒞} (α : G₁ ≅ G₂) (X : F.obj Γ) (x) : + α.hom.app X (α.inv.app X x) = x := + congr_fun (inv_hom_id_app α X) x + +variable {G₁ G₂ : DepFunctor F (𝒟 ⥤ Type v)} + +@[simp] +theorem hom_inv_id_app_app_apply {Γ : 𝒞} (α : G₁ ≅ G₂) (b : F.obj Γ) (X : 𝒟) (x) : + (α.inv.app b).app X ((α.hom.app b).app X x) = x := + congr_fun (congr_fun (congr_arg NatTrans.app (hom_inv_id_app α b)) X) x + +@[simp] +theorem inv_hom_id_app_app_apply {Γ : 𝒞} (α : G₁ ≅ G₂) (b : F.obj Γ) (X : 𝒟) (x) : + (α.hom.app b).app X ((α.inv.app b).app X x) = x := + congr_fun (congr_fun (congr_arg NatTrans.app (inv_hom_id_app α b)) X) x + end DepNatIso /-! ## Dependent sum functors -/ - /-- Given functors `F : 𝒞 ⥤ Type v` and `G : ∫F ⥤ 𝒟 ⥤ Type v`, produce the functor `(X, Y) ↦ (b : F(X)) × G((X, b))(Y)`. This is a dependent sum that varies naturally in its parameters `X, Y`. -/ @[simps!] -def Functor.Sigma.{v} {F : 𝒞 ⥤ Type v} (G : DepFunctor F (𝒟 ⥤ Type v)) : 𝒞 ⥤ 𝒟 ⥤ Type v := - curry.obj { +def Functor.Sigma.{v} {F : 𝒞 ⥤ Type v} (G : DepFunctor F (𝒟 ⥤ Type v)) : 𝒞 ⥤ 𝒟 ⥤ Type v := by + refine curry.obj { obj := fun (Γ, X) => (b : F.obj Γ) × ((G.obj b).obj X) map := fun (σ, f) ⟨b, e⟩ => - ⟨F.map σ b, (G.map σ b).app _ ((G.obj b).map f e)⟩ - map_id := fun (Γ, X) => by - refine funext fun ⟨b, e⟩ => ?_ - dsimp - congr! 1 with h - . simp - . simp only [FunctorToTypes.map_id_apply, DepFunctor.map_id] - rw! [h] - simp - map_comp := fun {_} {_} {Y} (σ, f) (τ, g) => by - refine funext fun ⟨b, e⟩ => ?_ - dsimp - congr! 1 with h - . simp - . simp only [FunctorToTypes.map_comp_apply, DepFunctor.map_comp] - rw! [h] - simp [FunctorToTypes.naturality] - } + ⟨F.map σ b, (G.map σ b _ rfl).app _ ((G.obj b).map f e)⟩ + map_id := ?_ + map_comp := ?_ + } <;> ( + intros + ext ⟨b, e⟩ : 1 + dsimp + congr! 1 with h + . simp + . rw! [h]; simp [FunctorToTypes.naturality] + ) def Functor.Sigma.isoCongrLeft.{v} (F₁ F₂ : 𝒞 ⥤ Type v) (G : DepFunctor F₁ (𝒟 ⥤ Type v)) - (i : F₂ ≅ F₁) : Functor.Sigma G ≅ Functor.Sigma (G.isoLeft i) := - NatIso.ofComponents₂ + (i : F₂ ≅ F₁) : Functor.Sigma G ≅ Functor.Sigma (G.isoLeft i) := by + refine NatIso.ofComponents₂ (fun Γ X => Equiv.toIso { toFun := fun ⟨b, e⟩ => ⟨i.inv.app Γ b, cast (by simp) e⟩ invFun := fun ⟨b, e⟩ => ⟨i.hom.app Γ b, e⟩ left_inv := fun ⟨_, _⟩ => by simp right_inv := fun ⟨_, _⟩ => by simp - }) - (fun X σ => by - ext ⟨b, e⟩ - simp only [Sigma, DepFunctor.isoLeft_obj, prod_Hom, DepFunctor.isoLeft_map, - FunctorToTypes.comp, curry_obj_obj_obj, curry_obj_map_app, FunctorToTypes.map_id_apply, - Equiv.toIso_hom, Equiv.coe_fn_mk, types_comp_apply, eqToHom_app, Sigma.mk.inj_iff, - FunctorToTypes.naturality, true_and] - have : (i.hom.app _ (F₂.map σ (i.inv.app _ b))) = F₁.map σ b := by - simp [FunctorToTypes.naturality] - rw! (castMode := .all) [this, FunctorToTypes.inv_hom_id_app_apply _ _ i _ (F₁.map σ b), - FunctorToTypes.inv_hom_id_app_apply _ _ i _ b] - simp) - (fun Γ f => by - ext ⟨b,e⟩ - simp only [Sigma, DepFunctor.isoLeft_obj, prod_Hom, DepFunctor.isoLeft_map, - FunctorToTypes.comp, curry_obj_obj_obj, curry_obj_obj_map, DepFunctor.map_id, eqToHom_app, - Equiv.toIso_hom, Equiv.coe_fn_mk, types_comp_apply, Sigma.mk.inj_iff, - FunctorToTypes.map_id_apply, true_and] - rw! (castMode := .all) [show F₁.map (𝟙 Γ) b = b by simp, - show i.hom.app Γ (i.inv.app Γ b) = b by simp, - show i.hom.app Γ (F₂.map (𝟙 Γ) (i.inv.app Γ b)) = b by simp [FunctorToTypes.naturality], - show F₁.map (𝟙 Γ) b = b by simp] - simp) + }) ?_ ?_ <;> ( + intros + ext : 1 + dsimp + apply let h := ?_; Sigma.ext h ?_ + . simp [FunctorToTypes.naturality] + . dsimp [Sigma] at h ⊢ + rw! [ + ← h, + FunctorToTypes.inv_hom_id_app_apply, + FunctorToTypes.inv_hom_id_app_apply, + ] + simp + ) def Functor.Sigma.isoCongrRight.{v} (F : 𝒞 ⥤ Type v) (G₁ G₂ : DepFunctor F (𝒟 ⥤ Type v)) (i : G₁ ≅ G₂) : @@ -216,26 +233,19 @@ def Functor.Sigma.isoCongrRight.{v} (F : 𝒞 ⥤ Type v) (G₁ G₂ : DepFuncto (fun Γ X => Equiv.toIso { toFun := fun ⟨b, e⟩ => ⟨b, (i.hom.app b).app X e⟩ invFun := fun ⟨b, e⟩ => ⟨b, (i.inv.app b).app X e⟩ - left_inv := fun ⟨b, e⟩ => by - -- simp doesn't finish this. missing simp lemma? - have := congr_fun (congr_fun (congr_arg NatTrans.app (DepNatIso.hom_inv_id_app i b)) X) e - simp only [NatTrans.comp_app] at this - simpa using this - right_inv := fun ⟨b, e⟩ => by - have := congr_fun (congr_fun (congr_arg NatTrans.app (DepNatIso.inv_hom_id_app i b)) X) e - simp only [NatTrans.comp_app] at this - simpa using this + left_inv := fun ⟨b, e⟩ => by simp + right_inv := fun ⟨b, e⟩ => by simp }) (fun X σ => by ext ⟨b, e⟩ - have := congr_fun (DepNatTrans.naturality_app i.hom σ b X) e + have := congr_fun (DepNatTrans.naturality_app i.hom σ b _ rfl X) e dsimp at this simp [Sigma, this]) (fun Γ f => by ext ⟨b, e⟩ - simp only [Sigma, prod_Hom, curry_obj_obj_obj, curry_obj_obj_map, DepFunctor.map_id, - eqToHom_app, Iso.app_hom, Iso.app_inv, Equiv.toIso_hom, Equiv.coe_fn_mk, types_comp_apply, - Sigma.mk.inj_iff, FunctorToTypes.map_id_apply, heq_eq_eq, true_and] + dsimp + simp only [Sigma, prod_Hom, curry_obj_obj_map, Sigma.mk.injEq, FunctorToTypes.map_id_apply, + heq_eq_eq, true_and] rw! [F.map_id Γ] simp [FunctorToTypes.naturality]) @@ -244,17 +254,15 @@ open Limits in noncomputable def pullbackDep.{v} {𝒞 : Type*} [Category.{v} 𝒞] [HasPullbacks 𝒞] {E B : 𝒞} (p : E ⟶ B) : DepFunctor (yoneda.obj B) (𝒞 ⥤ Type v) where obj _ b := coyoneda.obj <| Opposite.op <| pullback b p - map _ _ σ _ := + map _ _ σ _ _ eq := coyoneda.map <| Quiver.Hom.op <| - pullback.lift (pullback.fst .. ≫ σ.unop) (pullback.snd ..) (by simp [pullback.condition]) - map_id _ b := by + pullback.lift (pullback.fst .. ≫ σ.unop) (pullback.snd ..) + (by rw [eq]; simp [pullback.condition]) + map_id := by simp + map_comp := by + intros + ext : 3 dsimp - rw! [show 𝟙 _ ≫ b = b by simp] - simp - map_comp _ _ _ σ τ b := by - ext - dsimp - rw! [show τ.unop ≫ σ.unop ≫ b = (τ.unop ≫ σ.unop) ≫ b by simp] simp only [← Category.assoc] congr 1 ext <;> simp @@ -264,4 +272,45 @@ def bifunctor_comp_snd {𝒟' : Type*} [Category 𝒟'] (F : 𝒟' ⥤ 𝒟) (P obj Γ := F ⋙ P.obj Γ map σ := whiskerLeft F (P.map σ) +/-- The functor `(g : X ⟶ A) ↦ 𝒞/A(g, f)`. -/ +@[simps] +def overDep (A : 𝒞) : DepFunctor (yoneda.obj A) (Over A ⥤ Type) where + obj _ g := coyoneda.obj <| Opposite.op <| Over.mk g + map _ _ σ f g eq := coyoneda.map <| Quiver.Hom.op <| Over.homMk σ.unop (by simp [eq]) + map_id := by simp + map_comp := by + intros + ext : 3 + dsimp + ext : 1 + simp + +-- TODO: this in mathlib? +@[simps] +def Over_equiv {A : 𝒞} (X : 𝒞) (f : Over A) : (X ⟶ f.left) ≃ (b : X ⟶ A) × (Over.mk b ⟶ f) where + toFun g := ⟨g ≫ f.hom, Over.homMk g rfl⟩ + invFun g := g.2.left + left_inv _ := by simp + right_inv := fun x => by + dsimp; congr! 1 with h + . simp + . rw! [h] + simp + +/-- `𝒞(X, Over.forget f) ≅ Σ(g: X ⟶ A), 𝒞/A(g, f)` -/ +def Over_iso (A : 𝒞) : + bifunctor_comp_snd (Over.forget A) (coyoneda (C := 𝒞)) ≅ Functor.Sigma (overDep A) := by + refine NatIso.ofComponents₂ (fun Γ U => Equiv.toIso <| Over_equiv Γ.unop U) ?_ ?_ <;> ( + intros + dsimp + ext : 1 + apply let h := ?_; Sigma.ext h ?_ + . simp + . dsimp at h ⊢ + rw! [h] + apply heq_of_eq + ext + simp + ) + end CategoryTheory diff --git a/Poly/Tactic/BanishCasts.lean b/Poly/Tactic/BanishCasts.lean deleted file mode 100644 index b4f8c98..0000000 --- a/Poly/Tactic/BanishCasts.lean +++ /dev/null @@ -1,48 +0,0 @@ -import Mathlib.Tactic.Basic - -/-! Try to remove cast-like terms from the goal -by turning their equality argument into `refl`. - -Supported cast-like terms: -- `cast` -- `Eq.rec` -- `Eq.mpr` -- `Eq.mp` -- `CategoryTheory.eqToHom` -- `CategoryTheory.eqToIso` - -1. Identify all cast-like terms. -2. For each equality there, identify the differences using `congr`-like operation. -2a. For each difference, try to _prove_ it. - Very often a proof term for the difference will already appear in the goal somewhere: - use a generalized `assumption` tactic that finds such terms. -3. `generalize_proofs` -4. For each difference, generalize the RHS or LHS. - If RHS appears in LHS, generalize LHS; if vice-verse, generalize RHS; - otherwise generalize LHS. -5. Case on the difference with generalized LHS. -/ - --- assumption' : like assumption but can find proof terms in the goal type --- or one of the target types - -open Lean Meta Elab Term in -/-- If `h : a = b` (`h : HEq a b`) proves an equality (resp. heterogeneous equality), -`eq_lhs% h` is the left-hand-side `a`. -/ -elab "eq_lhs%" h:term : term => do - let A ← mkFreshTypeMVar - let l ← mkFreshExprMVar A - let r ← mkFreshExprMVar A - let _ ← elabTerm h (← mkAppOptM ``Eq #[A, l, r]) - -- TODO HEq - instantiateMVars l - -open Lean Meta Elab Term in -/-- If `h : a = b` (`h : HEq a b`) proves an equality (resp. heterogeneous equality), -`eq_rhs% h` is the right-hand-side `b`. -/ -elab "eq_rhs%" t:term : term => do - let A ← mkFreshTypeMVar - let l ← mkFreshExprMVar A - let r ← mkFreshExprMVar A - let _ ← elabTerm t (← mkAppOptM ``Eq #[A, l, r]) - -- TODO HEq - instantiateMVars r From 4effca61156bfc114f40435914d16d4f1cc6247e Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Tue, 11 Mar 2025 16:29:54 -0400 Subject: [PATCH 07/18] feat: util --- Poly/Util.lean | 24 ++++++++++++++++++++---- 1 file changed, 20 insertions(+), 4 deletions(-) diff --git a/Poly/Util.lean b/Poly/Util.lean index b29cc35..26125fb 100644 --- a/Poly/Util.lean +++ b/Poly/Util.lean @@ -56,19 +56,35 @@ lemma Over.eqToHom_eq_homMk {E B : 𝒞} (f g : E ⟶ B) (eq : f = g) : namespace Over +@[simp] +lemma homMk_comp {X Y Z W : 𝒞} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) (fgh_comp) : + homMk (U := mk (f ≫ g ≫ h)) (f ≫ g) fgh_comp = + homMk f ≫ homMk (U := mk (g ≫ h)) (V := mk h) g := + rfl + +@[simp] +lemma homMk_comp_assoc {X Y Z W : 𝒞} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) (fgh_comp) : + homMk (U := mk ((f ≫ g) ≫ h)) (f ≫ g) fgh_comp = + homMk f ≫ homMk (U := mk (g ≫ h)) (V := mk h) g := + rfl + /-- This is useful when `homMk (· ≫ ·)` appears under `Functor.map` or a natural equivalence. -/ -lemma homMk_comp {B : 𝒞} {U V W : Over B} (f : U.left ⟶ V.left) (g : V.left ⟶ W.left) +lemma homMk_comp' {B : 𝒞} {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 := rfl @[simp] -lemma left_homMk {B : 𝒞} {U V : Over B} (f : U ⟶ V) (h) : - homMk f.left h = f := +lemma left_homMk {B : 𝒞} {U V : Over B} (f : U ⟶ V) (h) : homMk f.left h = f := + rfl + +@[simp] +lemma homMk_id {B : 𝒞} (U : Over B) (h) : homMk (𝟙 U.left) h = 𝟙 U := rfl @[simp] -lemma homMk_id {B : 𝒞} {U : Over B} (h) : homMk (𝟙 U.left) h = 𝟙 U := +-- `homMk_id` does not trigger if `X ≢ U.left` syntactically +lemma homMk_id' {B : 𝒞} (f : X ⟶ B) (h) : homMk (𝟙 X) h = 𝟙 (mk f) := rfl -- -- Probably bad as a simp lemma? From 46ab3f41bc2a41e0c7fedd6d391b8cfcddd77e93 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Tue, 11 Mar 2025 18:37:25 -0400 Subject: [PATCH 08/18] chore: update to new mathlib and reorganize --- Poly/Bifunctor.lean | 316 --------------------- Poly/DepFunctor/Basic.lean | 156 ++++++++++ Poly/DepFunctor/Sigma.lean | 170 +++++++++++ Poly/ForMathlib/CategoryTheory/NatIso.lean | 25 ++ Poly/Util.lean | 32 +-- 5 files changed, 356 insertions(+), 343 deletions(-) delete mode 100644 Poly/Bifunctor.lean create mode 100644 Poly/DepFunctor/Basic.lean create mode 100644 Poly/DepFunctor/Sigma.lean create mode 100644 Poly/ForMathlib/CategoryTheory/NatIso.lean diff --git a/Poly/Bifunctor.lean b/Poly/Bifunctor.lean deleted file mode 100644 index 31da129..0000000 --- a/Poly/Bifunctor.lean +++ /dev/null @@ -1,316 +0,0 @@ -import Mathlib.CategoryTheory.Functor.Currying - -import Poly.Util - -import SEq.Tactic.DepRewrite - -/-! # Bifunctors - -We define some constructions on bifunctors (aka profunctors), -that is functors in two arguments. - -Their utility in Poly is as a tool for packaging and composing natural equivalences. -For example, given `F,H : 𝒞 ⟶ ℰ` and `G,I : 𝒟 ⟶ ℰ`, -``` -F(X) ⟶ G(Y) -============ -H(X) ⟶ I(Y) -``` -would be a natural isomorphism of bifunctors `𝒞ᵒᵖ ⥤ 𝒟 ⥤ Type v` -given by `(X, Y) ↦ F(X) ⟶ G(Y)` and `(X, Y) ↦ H(X) ⟶ I(Y)`. -/ - -namespace CategoryTheory - -variable {𝒞 𝒟 ℰ : Type*} [Category 𝒞] [Category 𝒟] [Category ℰ] - -/-- Natural isomorphism of bifunctors from naturality in both arguments. -/ -def NatIso.ofComponents₂ {F G : 𝒞 ⥤ 𝒟 ⥤ ℰ} - (app : ∀ Γ X, (F.obj Γ).obj X ≅ (G.obj Γ).obj X) - (naturality_left : ∀ {Γ Δ : 𝒞} (X : 𝒟) (σ : Γ ⟶ Δ), - (F.map σ).app X ≫ (app Δ X).hom = (app Γ X).hom ≫ (G.map σ).app X := by aesop_cat) - (naturality_right : ∀ {X Y : 𝒟} (Γ : 𝒞) (f : X ⟶ Y), - (F.obj Γ).map f ≫ (app Γ Y).hom = (app Γ X).hom ≫ (G.obj Γ).map f := by aesop_cat) : - F ≅ G := - NatIso.ofComponents - (fun Γ => NatIso.ofComponents (app Γ) (fun f => by simpa using naturality_right Γ f)) - (fun σ => by ext X : 2; simpa using naturality_left X σ) - -/-! ## Dependent functors -/ - -/-- A functor into `𝒟` that depends on `F`, -in other words `∫F ⥤ 𝒟` where all the `F(Γ)` are discrete, -spelled out in elementary terms. - -(In the general case, we would have -`map : ∀ ⦃Γ Δ⦄ ⦃b : F.obj Γ⦄ ⦃c : F.obj Δ⦄ - (σ : Γ ⟶ Δ) (f : F.map σ b ⟶ c), obj b ⟶ obj c`.) - -Equivalently, it is a (lax or strict or something) transformation `F ⟶ const 𝒟`. -/ --- NOTE: A more mathlib-ready, general approach might use `∫F ⥤ 𝒟`, --- and introduce a special-case constructor for discrete `F(Γ)` --- with an argument for each field of this structure. -/ -structure DepFunctor (F : 𝒞 ⥤ Type*) (𝒟 : Type*) [Category 𝒟] where - obj : ∀ ⦃Γ⦄, F.obj Γ → 𝒟 - -- Forded to avoid `eqToHom` in the axioms. - map : ∀ ⦃Γ Δ⦄ (σ : Γ ⟶ Δ) (b : F.obj Γ) (c : F.obj Δ), c = F.map σ b → (obj b ⟶ obj c) - map_id : ∀ ⦃Γ⦄ b h, map (𝟙 Γ) b b h = 𝟙 (obj b) := by aesop_cat - /-- ### `simp` - The two `map` equalities in the LHS imply the one in the RHS, but not vice-versa. - This axiom is thus stated in a "packing" rather than an "unpacking" direction, - so that `simp` can apply it automatically by matching `h₁` and `h₂`. - However, we do not mark it `simp`; - instead, a special case in the "unpacking" direction is `simp`. -/ - map_comp : ∀ ⦃Γ Δ Θ⦄ (σ : Γ ⟶ Δ) (τ : Δ ⟶ Θ) b c d h₁ h₂, - map σ b c h₁ ≫ map τ c d h₂ = map (σ ≫ τ) b d (by simp [h₁, h₂]) := by aesop_cat - -attribute [simp] DepFunctor.map_id - -/-- Specialized variant of `map_comp` that `simp` can match against. -/ -@[simp] -theorem DepFunctor.map_comp' {F : 𝒞 ⥤ Type*} {G : DepFunctor F 𝒟} - ⦃Γ Δ Θ⦄ (σ : Γ ⟶ Δ) (τ : Δ ⟶ Θ) b h : - G.map (σ ≫ τ) b (F.map τ (F.map σ b)) h = G.map σ b (F.map σ b) rfl ≫ G.map τ _ _ rfl := - (G.map_comp σ τ ..).symm - -@[simps] -def DepFunctor.isoLeft.{v} {F₁ F₂ : 𝒞 ⥤ Type v} {𝒟 : Type*} [Category 𝒟] - (G : DepFunctor F₁ 𝒟) (i : F₂ ≅ F₁) : DepFunctor F₂ 𝒟 where - obj Γ b := G.obj (i.hom.app Γ b) - map Γ _ σ _ _ eq := G.map σ _ _ (by simp [eq, FunctorToTypes.naturality]) - map_id := by simp - map_comp := by simp [G.map_comp] - -@[ext] -structure DepNatTrans {F : 𝒞 ⥤ Type*} {𝒟 : Type*} [Category 𝒟] (G₁ G₂ : DepFunctor F 𝒟) where - app : ∀ ⦃Γ⦄ (b : F.obj Γ), G₁.obj b ⟶ G₂.obj b - naturality : ∀ ⦃Γ Δ⦄ (σ : Γ ⟶ Δ) (b : F.obj Γ) (c : F.obj Δ) h, - app b ≫ G₂.map σ b c h = G₁.map σ b c h ≫ app c := by aesop_cat - -attribute [reassoc] DepNatTrans.naturality - -@[simps] -instance (F : 𝒞 ⥤ Type*) (𝒟 : Type*) [Category 𝒟] : Category (DepFunctor F 𝒟) where - Hom := DepNatTrans - id G := { app := fun _ _ => 𝟙 _ } - comp η ν := { - app := fun _ b => η.app b ≫ ν.app b - naturality := by simp [η.naturality_assoc, ν.naturality] - } - -namespace DepNatTrans - -variable {F : 𝒞 ⥤ Type*} {𝒟 : Type*} [Category 𝒟] {Γ : 𝒞} (b : F.obj Γ) - -@[ext] -theorem ext' {G₁ G₂ : DepFunctor F 𝒟} {α β : G₁ ⟶ G₂} (w : α.app = β.app) : α = β := - DepNatTrans.ext w - -@[simp] -theorem id_app (G₁ : DepFunctor F 𝒟) : (𝟙 G₁ : G₁ ⟶ G₁).app b = 𝟙 (G₁.obj b) := rfl - -@[reassoc (attr := simp)] -theorem comp_app {G₁ G₂ G₃ : DepFunctor F 𝒟} (α : G₁ ⟶ G₂) (β : G₂ ⟶ G₃) : - (α ≫ β).app b = α.app b ≫ β.app b := rfl - -@[reassoc] -theorem naturality_app {ℰ : Type*} [Category ℰ] {G₁ G₂ : DepFunctor F (𝒟 ⥤ ℰ)} (α : G₁ ⟶ G₂) - {Γ Δ : 𝒞} (σ : Γ ⟶ Δ) (b : F.obj Γ) (c : F.obj Δ) h (X : 𝒟) : - (G₁.map σ b c h).app X ≫ (α.app c).app X = (α.app b).app X ≫ (G₂.map σ b c h).app X := - (congr_fun (congr_arg NatTrans.app (α.naturality σ b c h)) X).symm - -end DepNatTrans - -namespace DepNatIso - -variable {F : 𝒞 ⥤ Type*} {𝒟 : Type*} [Category 𝒟] {G₁ G₂ : DepFunctor F 𝒟} - -@[reassoc (attr := simp)] -theorem hom_inv_id_app {Γ : 𝒞} (α : G₁ ≅ G₂) (b : F.obj Γ) : - α.hom.app b ≫ α.inv.app b = 𝟙 (G₁.obj b) := by - simp [← DepNatTrans.comp_app] - -@[reassoc (attr := simp)] -theorem inv_hom_id_app {Γ : 𝒞} (α : G₁ ≅ G₂) (b : F.obj Γ) : - α.inv.app b ≫ α.hom.app b = 𝟙 (G₂.obj b) := by - simp [← DepNatTrans.comp_app] - -instance hom_app_isIso {Γ : 𝒞} (α : G₁ ≅ G₂) (b : F.obj Γ) : IsIso (α.hom.app b) := - ⟨α.inv.app b, by simp⟩ - -instance inv_app_isIso {Γ : 𝒞} (α : G₁ ≅ G₂) (b : F.obj Γ) : IsIso (α.inv.app b) := - ⟨α.hom.app b, by simp⟩ - -def ofComponents - (app : ∀ {Γ} (b : F.obj Γ), G₁.obj b ≅ G₂.obj b) - (naturality : ∀ {Γ Δ} (σ : Γ ⟶ Δ) (b : F.obj Γ) (c : F.obj Δ) h, - (app b).hom ≫ G₂.map σ b c h = G₁.map σ b c h ≫ (app c).hom) : - G₁ ≅ G₂ where - hom := { app := fun _ b => (app b).hom } - inv := { - app := fun _ b => (app b).inv - naturality := fun _ _ σ b c h => by - have : (app b).inv ≫ (app b).hom ≫ G₂.map σ b c h ≫ (app c).inv = - (app b).inv ≫ G₁.map σ b c h ≫ (app c).hom ≫ (app c).inv := by - simp [reassoc_of% naturality] - simpa using this.symm - } - -variable {G₁ G₂ : DepFunctor F (Type v)} - -@[simp] -theorem hom_inv_id_app_apply {Γ : 𝒞} (α : G₁ ≅ G₂) (X : F.obj Γ) (x) : - α.inv.app X (α.hom.app X x) = x := - congr_fun (hom_inv_id_app α X) x - -@[simp] -theorem inv_hom_id_app_apply {Γ : 𝒞} (α : G₁ ≅ G₂) (X : F.obj Γ) (x) : - α.hom.app X (α.inv.app X x) = x := - congr_fun (inv_hom_id_app α X) x - -variable {G₁ G₂ : DepFunctor F (𝒟 ⥤ Type v)} - -@[simp] -theorem hom_inv_id_app_app_apply {Γ : 𝒞} (α : G₁ ≅ G₂) (b : F.obj Γ) (X : 𝒟) (x) : - (α.inv.app b).app X ((α.hom.app b).app X x) = x := - congr_fun (congr_fun (congr_arg NatTrans.app (hom_inv_id_app α b)) X) x - -@[simp] -theorem inv_hom_id_app_app_apply {Γ : 𝒞} (α : G₁ ≅ G₂) (b : F.obj Γ) (X : 𝒟) (x) : - (α.hom.app b).app X ((α.inv.app b).app X x) = x := - congr_fun (congr_fun (congr_arg NatTrans.app (inv_hom_id_app α b)) X) x - -end DepNatIso - -/-! ## Dependent sum functors -/ - -/-- Given functors `F : 𝒞 ⥤ Type v` and `G : ∫F ⥤ 𝒟 ⥤ Type v`, -produce the functor `(X, Y) ↦ (b : F(X)) × G((X, b))(Y)`. -This is a dependent sum that varies naturally in its parameters `X, Y`. -/ -@[simps!] -def Functor.Sigma.{v} {F : 𝒞 ⥤ Type v} (G : DepFunctor F (𝒟 ⥤ Type v)) : 𝒞 ⥤ 𝒟 ⥤ Type v := by - refine curry.obj { - obj := fun (Γ, X) => (b : F.obj Γ) × ((G.obj b).obj X) - map := fun (σ, f) ⟨b, e⟩ => - ⟨F.map σ b, (G.map σ b _ rfl).app _ ((G.obj b).map f e)⟩ - map_id := ?_ - map_comp := ?_ - } <;> ( - intros - ext ⟨b, e⟩ : 1 - dsimp - congr! 1 with h - . simp - . rw! [h]; simp [FunctorToTypes.naturality] - ) - -def Functor.Sigma.isoCongrLeft.{v} (F₁ F₂ : 𝒞 ⥤ Type v) (G : DepFunctor F₁ (𝒟 ⥤ Type v)) - (i : F₂ ≅ F₁) : Functor.Sigma G ≅ Functor.Sigma (G.isoLeft i) := by - refine NatIso.ofComponents₂ - (fun Γ X => Equiv.toIso { - toFun := fun ⟨b, e⟩ => ⟨i.inv.app Γ b, cast (by simp) e⟩ - invFun := fun ⟨b, e⟩ => ⟨i.hom.app Γ b, e⟩ - left_inv := fun ⟨_, _⟩ => by simp - right_inv := fun ⟨_, _⟩ => by simp - }) ?_ ?_ <;> ( - intros - ext : 1 - dsimp - apply let h := ?_; Sigma.ext h ?_ - . simp [FunctorToTypes.naturality] - . dsimp [Sigma] at h ⊢ - rw! [ - ← h, - FunctorToTypes.inv_hom_id_app_apply, - FunctorToTypes.inv_hom_id_app_apply, - ] - simp - ) - -def Functor.Sigma.isoCongrRight.{v} (F : 𝒞 ⥤ Type v) (G₁ G₂ : DepFunctor F (𝒟 ⥤ Type v)) - (i : G₁ ≅ G₂) : - Functor.Sigma G₁ ≅ Functor.Sigma G₂ := - NatIso.ofComponents₂ - (fun Γ X => Equiv.toIso { - toFun := fun ⟨b, e⟩ => ⟨b, (i.hom.app b).app X e⟩ - invFun := fun ⟨b, e⟩ => ⟨b, (i.inv.app b).app X e⟩ - left_inv := fun ⟨b, e⟩ => by simp - right_inv := fun ⟨b, e⟩ => by simp - }) - (fun X σ => by - ext ⟨b, e⟩ - have := congr_fun (DepNatTrans.naturality_app i.hom σ b _ rfl X) e - dsimp at this - simp [Sigma, this]) - (fun Γ f => by - ext ⟨b, e⟩ - dsimp - simp only [Sigma, prod_Hom, curry_obj_obj_map, Sigma.mk.injEq, FunctorToTypes.map_id_apply, - heq_eq_eq, true_and] - rw! [F.map_id Γ] - simp [FunctorToTypes.naturality]) - -open Limits in -/-- The functor `(b : Γ ⟶ B) ↦ Hom(dom(b*p), -)`. -/ -noncomputable def pullbackDep.{v} {𝒞 : Type*} [Category.{v} 𝒞] [HasPullbacks 𝒞] {E B : 𝒞} (p : E ⟶ B) : - DepFunctor (yoneda.obj B) (𝒞 ⥤ Type v) where - obj _ b := coyoneda.obj <| Opposite.op <| pullback b p - map _ _ σ _ _ eq := - coyoneda.map <| Quiver.Hom.op <| - pullback.lift (pullback.fst .. ≫ σ.unop) (pullback.snd ..) - (by rw [eq]; simp [pullback.condition]) - map_id := by simp - map_comp := by - intros - ext : 3 - dsimp - simp only [← Category.assoc] - congr 1 - ext <;> simp - -@[simps] -def bifunctor_comp_snd {𝒟' : Type*} [Category 𝒟'] (F : 𝒟' ⥤ 𝒟) (P : 𝒞 ⥤ 𝒟 ⥤ ℰ) : 𝒞 ⥤ 𝒟' ⥤ ℰ where - obj Γ := F ⋙ P.obj Γ - map σ := whiskerLeft F (P.map σ) - -/-- The functor `(g : X ⟶ A) ↦ 𝒞/A(g, f)`. -/ -@[simps] -def overDep (A : 𝒞) : DepFunctor (yoneda.obj A) (Over A ⥤ Type) where - obj _ g := coyoneda.obj <| Opposite.op <| Over.mk g - map _ _ σ f g eq := coyoneda.map <| Quiver.Hom.op <| Over.homMk σ.unop (by simp [eq]) - map_id := by simp - map_comp := by - intros - ext : 3 - dsimp - ext : 1 - simp - --- TODO: this in mathlib? -@[simps] -def Over_equiv {A : 𝒞} (X : 𝒞) (f : Over A) : (X ⟶ f.left) ≃ (b : X ⟶ A) × (Over.mk b ⟶ f) where - toFun g := ⟨g ≫ f.hom, Over.homMk g rfl⟩ - invFun g := g.2.left - left_inv _ := by simp - right_inv := fun x => by - dsimp; congr! 1 with h - . simp - . rw! [h] - simp - -/-- `𝒞(X, Over.forget f) ≅ Σ(g: X ⟶ A), 𝒞/A(g, f)` -/ -def Over_iso (A : 𝒞) : - bifunctor_comp_snd (Over.forget A) (coyoneda (C := 𝒞)) ≅ Functor.Sigma (overDep A) := by - refine NatIso.ofComponents₂ (fun Γ U => Equiv.toIso <| Over_equiv Γ.unop U) ?_ ?_ <;> ( - intros - dsimp - ext : 1 - apply let h := ?_; Sigma.ext h ?_ - . simp - . dsimp at h ⊢ - rw! [h] - apply heq_of_eq - ext - simp - ) - -end CategoryTheory diff --git a/Poly/DepFunctor/Basic.lean b/Poly/DepFunctor/Basic.lean new file mode 100644 index 0000000..e68033e --- /dev/null +++ b/Poly/DepFunctor/Basic.lean @@ -0,0 +1,156 @@ +/- +Copyright (c) 2025 Wojciech Nawrocki. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Wojciech Nawrocki +-/ + +import Poly.Util + +namespace CategoryTheory + +variable {𝒞 𝒟 ℰ : Type*} [Category 𝒞] [Category 𝒟] [Category ℰ] + +/-! ## Dependent functors -/ + +/-- A functor into `𝒟` that depends on `F` +in other words `∫F ⥤ 𝒟` where all the `F(Γ)` are discrete, +spelled out in elementary terms. + +(In the general case, we would have +`map : ∀ ⦃Γ Δ⦄ ⦃b : F.obj Γ⦄ ⦃c : F.obj Δ⦄ + (σ : Γ ⟶ Δ) (f : F.map σ b ⟶ c), obj b ⟶ obj c`.) + +Equivalently, this is a (lax or strict or something) transformation `F ⟶ const 𝒟`. -/ +-- NOTE: A more mathlib-ready, general approach might use `∫F ⥤ 𝒟`, +-- and introduce a special-case constructor for discrete `F(Γ)` +-- with an argument for each field of this structure. -/ +structure DepFunctor (F : 𝒞 ⥤ Type*) (𝒟 : Type*) [Category 𝒟] where + obj : ∀ ⦃Γ⦄, F.obj Γ → 𝒟 + -- Forded to avoid `eqToHom` in the axioms. + map : ∀ ⦃Γ Δ⦄ (σ : Γ ⟶ Δ) (b : F.obj Γ) (c : F.obj Δ), c = F.map σ b → (obj b ⟶ obj c) + map_id : ∀ ⦃Γ⦄ b h, map (𝟙 Γ) b b h = 𝟙 (obj b) := by aesop_cat + /-- **Note about `simp`.** + The two `map` equalities in the LHS imply the one in the RHS, but not vice-versa. + This axiom is thus stated in a "packing" rather than an "unpacking" direction, + so that `simp` can apply it automatically by matching `h₁` and `h₂`. + However, we do not mark it `simp` globally, + preferring `map_comp'` whenever it applies. -/ + map_comp : ∀ ⦃Γ Δ Θ⦄ (σ : Γ ⟶ Δ) (τ : Δ ⟶ Θ) b c d h₁ h₂, + map σ b c h₁ ≫ map τ c d h₂ = map (σ ≫ τ) b d (by simp [h₁, h₂]) := by aesop_cat + +namespace DepFunctor + +attribute [simp] map_id + +/-- Specialized variant of `(map_comp ..).symm` that `simp` can match against. -/ +@[simp] +theorem map_comp' {F : 𝒞 ⥤ Type*} {G : DepFunctor F 𝒟} ⦃Γ Δ Θ⦄ (σ : Γ ⟶ Δ) (τ : Δ ⟶ Θ) b h : + G.map (σ ≫ τ) b (F.map τ (F.map σ b)) h = G.map σ b (F.map σ b) rfl ≫ G.map τ _ _ rfl := + (G.map_comp σ τ ..).symm + +@[simps] +def isoLeft.{v} {F₁ F₂ : 𝒞 ⥤ Type v} (G : DepFunctor F₁ 𝒟) (i : F₂ ≅ F₁) : DepFunctor F₂ 𝒟 where + obj Γ b := G.obj (i.hom.app Γ b) + map Γ _ σ _ _ eq := G.map σ _ _ (by simp [eq, FunctorToTypes.naturality]) + map_id := by simp + map_comp := by simp [G.map_comp] + +end DepFunctor + +@[ext] +structure DepNatTrans {F : 𝒞 ⥤ Type*} (G₁ G₂ : DepFunctor F 𝒟) where + app : ∀ ⦃Γ⦄ (b : F.obj Γ), G₁.obj b ⟶ G₂.obj b + naturality : ∀ ⦃Γ Δ⦄ (σ : Γ ⟶ Δ) (b : F.obj Γ) (c : F.obj Δ) h, + app b ≫ G₂.map σ b c h = G₁.map σ b c h ≫ app c := by aesop_cat + +@[simps] +instance (F : 𝒞 ⥤ Type*) : Category (DepFunctor F 𝒟) where + Hom := DepNatTrans + id G := { app := fun _ _ => 𝟙 _ } + comp η ν := { + app := fun _ b => η.app b ≫ ν.app b + naturality := by simp [reassoc_of% η.naturality, ν.naturality] + } + +namespace DepNatTrans + +variable {F : 𝒞 ⥤ Type*} {Γ : 𝒞} (b : F.obj Γ) + +@[ext] +theorem ext' {G₁ G₂ : DepFunctor F 𝒟} {α β : G₁ ⟶ G₂} (w : α.app = β.app) : α = β := + DepNatTrans.ext w + +@[simp] +theorem id_app (G₁ : DepFunctor F 𝒟) : (𝟙 G₁ : G₁ ⟶ G₁).app b = 𝟙 (G₁.obj b) := rfl + +@[reassoc (attr := simp)] +theorem comp_app {G₁ G₂ G₃ : DepFunctor F 𝒟} (α : G₁ ⟶ G₂) (β : G₂ ⟶ G₃) : + (α ≫ β).app b = α.app b ≫ β.app b := rfl + +theorem naturality_app {G₁ G₂ : DepFunctor F (𝒟 ⥤ ℰ)} (α : G₁ ⟶ G₂) + {Γ Δ : 𝒞} (σ : Γ ⟶ Δ) (b : F.obj Γ) (c : F.obj Δ) h (X : 𝒟) : + (G₁.map σ b c h).app X ≫ (α.app c).app X = (α.app b).app X ≫ (G₂.map σ b c h).app X := + (congr_fun (congr_arg NatTrans.app (α.naturality σ b c h)) X).symm + +end DepNatTrans + +namespace DepNatIso + +variable {F : 𝒞 ⥤ Type*} {G₁ G₂ : DepFunctor F 𝒟} + +@[reassoc (attr := simp)] +theorem hom_inv_id_app {Γ : 𝒞} (α : G₁ ≅ G₂) (b : F.obj Γ) : + α.hom.app b ≫ α.inv.app b = 𝟙 (G₁.obj b) := by + simp [← DepNatTrans.comp_app] + +@[reassoc (attr := simp)] +theorem inv_hom_id_app {Γ : 𝒞} (α : G₁ ≅ G₂) (b : F.obj Γ) : + α.inv.app b ≫ α.hom.app b = 𝟙 (G₂.obj b) := by + simp [← DepNatTrans.comp_app] + +instance hom_app_isIso {Γ : 𝒞} (α : G₁ ≅ G₂) (b : F.obj Γ) : IsIso (α.hom.app b) := + ⟨α.inv.app b, by simp⟩ + +instance inv_app_isIso {Γ : 𝒞} (α : G₁ ≅ G₂) (b : F.obj Γ) : IsIso (α.inv.app b) := + ⟨α.hom.app b, by simp⟩ + +def ofComponents + (app : ∀ {Γ} (b : F.obj Γ), G₁.obj b ≅ G₂.obj b) + (naturality : ∀ {Γ Δ} (σ : Γ ⟶ Δ) (b : F.obj Γ) (c : F.obj Δ) h, + (app b).hom ≫ G₂.map σ b c h = G₁.map σ b c h ≫ (app c).hom) : + G₁ ≅ G₂ where + hom := { app := fun _ b => (app b).hom } + inv := { + app := fun _ b => (app b).inv + naturality := fun _ _ σ b c h => by + have : (app b).inv ≫ (app b).hom ≫ G₂.map σ b c h ≫ (app c).inv = + (app b).inv ≫ G₁.map σ b c h ≫ (app c).hom ≫ (app c).inv := by + simp [reassoc_of% naturality] + simpa using this.symm + } + +variable {G₁ G₂ : DepFunctor F (Type v)} + +@[simp] +theorem hom_inv_id_app_apply {Γ : 𝒞} (α : G₁ ≅ G₂) (X : F.obj Γ) (x) : + α.inv.app X (α.hom.app X x) = x := + congr_fun (hom_inv_id_app α X) x + +@[simp] +theorem inv_hom_id_app_apply {Γ : 𝒞} (α : G₁ ≅ G₂) (X : F.obj Γ) (x) : + α.hom.app X (α.inv.app X x) = x := + congr_fun (inv_hom_id_app α X) x + +variable {G₁ G₂ : DepFunctor F (𝒟 ⥤ Type v)} + +@[simp] +theorem hom_inv_id_app_app_apply {Γ : 𝒞} (α : G₁ ≅ G₂) (b : F.obj Γ) (X : 𝒟) (x) : + (α.inv.app b).app X ((α.hom.app b).app X x) = x := + congr_fun (congr_fun (congr_arg NatTrans.app (hom_inv_id_app α b)) X) x + +@[simp] +theorem inv_hom_id_app_app_apply {Γ : 𝒞} (α : G₁ ≅ G₂) (b : F.obj Γ) (X : 𝒟) (x) : + (α.hom.app b).app X ((α.inv.app b).app X x) = x := + congr_fun (congr_fun (congr_arg NatTrans.app (inv_hom_id_app α b)) X) x + +end DepNatIso diff --git a/Poly/DepFunctor/Sigma.lean b/Poly/DepFunctor/Sigma.lean new file mode 100644 index 0000000..24b6a51 --- /dev/null +++ b/Poly/DepFunctor/Sigma.lean @@ -0,0 +1,170 @@ +/- +Copyright (c) 2025 Wojciech Nawrocki. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Wojciech Nawrocki +-/ + +import SEq.Tactic.DepRewrite + +import Poly.DepFunctor.Basic +import Poly.ForMathlib.CategoryTheory.NatIso + +namespace CategoryTheory + +variable {𝒞 𝒟 ℰ : Type*} [Category 𝒞] [Category 𝒟] [Category ℰ] + +/-! ## Dependent sum functor -/ + +namespace DepFunctor + +/-- Given functors `F : 𝒞 ⥤ Type v` and `G : ∫F ⥤ 𝒟 ⥤ Type v`, +produce the functor `(X, Y) ↦ (b : F(X)) × G((X, b))(Y)`. + +This is a dependent sum that varies naturally +in a parameter `X` of the first component, +and a parameter `Y` of the second component. + +We use this to package and compose natural equivalences +where one (or both) sides is a dependent sum, e.g. +``` +H(X) ⟶ I(Y) +========================= +(b : F(X)) × (G(X, b)(Y)) +``` +is a natural isomorphism of bifunctors `𝒞ᵒᵖ ⥤ 𝒟 ⥤ Type v` +given by `(X, Y) ↦ H(X) ⟶ I(Y)` and `G.Sigma`. -/ +@[simps!] +def Sigma.{v} {F : 𝒞 ⥤ Type v} (G : DepFunctor F (𝒟 ⥤ Type v)) : 𝒞 ⥤ 𝒟 ⥤ Type v := by + refine curry.obj { + obj := fun (Γ, X) => (b : F.obj Γ) × ((G.obj b).obj X) + map := fun (σ, f) ⟨b, e⟩ => + ⟨F.map σ b, (G.map σ b _ rfl).app _ ((G.obj b).map f e)⟩ + map_id := ?_ + map_comp := ?_ + } <;> ( + intros + ext ⟨b, e⟩ : 1 + dsimp + congr! 1 with h + . simp + . rw! [h]; simp [FunctorToTypes.naturality] + ) + +def Sigma.isoCongrLeft.{v} (F₁ F₂ : 𝒞 ⥤ Type v) (G : DepFunctor F₁ (𝒟 ⥤ Type v)) + (i : F₂ ≅ F₁) : G.Sigma ≅ (G.isoLeft i).Sigma := by + refine NatIso.ofComponents₂ + (fun Γ X => Equiv.toIso { + toFun := fun ⟨b, e⟩ => ⟨i.inv.app Γ b, cast (by simp) e⟩ + invFun := fun ⟨b, e⟩ => ⟨i.hom.app Γ b, e⟩ + left_inv := fun ⟨_, _⟩ => by simp + right_inv := fun ⟨_, _⟩ => by simp + }) ?_ ?_ <;> ( + intros + ext : 1 + dsimp + apply let h := ?_; Sigma.ext h ?_ + . simp [FunctorToTypes.naturality] + . dsimp [Sigma] at h ⊢ + rw! [ + ← h, + FunctorToTypes.inv_hom_id_app_apply, + FunctorToTypes.inv_hom_id_app_apply, + ] + simp + ) + +def Sigma.isoCongrRight.{v} (F : 𝒞 ⥤ Type v) (G₁ G₂ : DepFunctor F (𝒟 ⥤ Type v)) + (i : G₁ ≅ G₂) : + G₁.Sigma ≅ G₂.Sigma := + NatIso.ofComponents₂ + (fun Γ X => Equiv.toIso { + toFun := fun ⟨b, e⟩ => ⟨b, (i.hom.app b).app X e⟩ + invFun := fun ⟨b, e⟩ => ⟨b, (i.inv.app b).app X e⟩ + left_inv := fun ⟨b, e⟩ => by simp + right_inv := fun ⟨b, e⟩ => by simp + }) + (fun X σ => by + ext ⟨b, e⟩ + have := congr_fun (DepNatTrans.naturality_app i.hom σ b _ rfl X) e + dsimp at this + simp [Sigma, this]) + (fun Γ f => by + ext ⟨b, e⟩ + dsimp + simp only [Sigma, prod_Hom, curry_obj_obj_map, Sigma.mk.injEq, FunctorToTypes.map_id_apply, + heq_eq_eq, true_and] + rw! [F.map_id Γ] + simp [FunctorToTypes.naturality]) + +end DepFunctor + +open Limits in +/-- The functor `(b : Γ ⟶ B) ↦ Hom(dom(b*p), -)`. -/ +noncomputable def pullbackDep.{v} {𝒞 : Type*} [Category.{v} 𝒞] [HasPullbacks 𝒞] + {E B : 𝒞} (p : E ⟶ B) : + DepFunctor (yoneda.obj B) (𝒞 ⥤ Type v) where + obj _ b := coyoneda.obj <| Opposite.op <| pullback b p + map _ _ σ _ _ eq := + coyoneda.map <| Quiver.Hom.op <| + pullback.lift (pullback.fst .. ≫ σ.unop) (pullback.snd ..) + (by rw [eq]; simp [pullback.condition]) + map_id := by simp + map_comp := by + intros + ext : 3 + dsimp + simp only [← Category.assoc] + congr 1 + ext <;> simp + +-- TODO: move elsewhere +@[simps] +def bifunctor_comp_snd {𝒟' : Type*} [Category 𝒟'] (F : 𝒟' ⥤ 𝒟) (P : 𝒞 ⥤ 𝒟 ⥤ ℰ) : 𝒞 ⥤ 𝒟' ⥤ ℰ where + obj Γ := F ⋙ P.obj Γ + map σ := whiskerLeft F (P.map σ) + +/-- The hom-functor `𝒞/Aᵒᵖ ⥤ 𝒞/A ⥤ Type` given by +`(X, g : X ⟶ A) (Y, f : Y ⟶ A) ↦ 𝒞/A(g, f)` +written as a dependent functor `∫y(A) ⥤ 𝒞/A ⥤ Type`. +This is to express the dependent sum `Σ(g : X ⟶ A), 𝒞/A(g, f)`. -/ +@[simps] +def overDep (A : 𝒞) : DepFunctor (yoneda.obj A) (Over A ⥤ Type) where + obj _ g := coyoneda.obj <| Opposite.op <| Over.mk g + map _ _ σ f g eq := coyoneda.map <| Quiver.Hom.op <| Over.homMk σ.unop (by simp [eq]) + map_id := by simp + map_comp := by + intros + ext : 3 + dsimp + ext : 1 + simp + +-- TODO: this in mathlib? +@[simps] +def Over_equiv {A : 𝒞} (X : 𝒞) (f : Over A) : (X ⟶ f.left) ≃ (b : X ⟶ A) × (Over.mk b ⟶ f) where + toFun g := ⟨g ≫ f.hom, Over.homMk g rfl⟩ + invFun g := g.2.left + left_inv _ := by simp + right_inv := fun x => by + dsimp; congr! 1 with h + . simp + . rw! [h] + simp + +/-- `𝒞(X, Over.forget f) ≅ Σ(g: X ⟶ A), 𝒞/A(g, f)` -/ +def Over_iso (A : 𝒞) : + bifunctor_comp_snd (Over.forget A) (coyoneda (C := 𝒞)) ≅ (overDep A).Sigma := by + refine NatIso.ofComponents₂ (fun Γ U => Equiv.toIso <| Over_equiv Γ.unop U) ?_ ?_ <;> ( + intros + dsimp + ext : 1 + apply let h := ?_; Sigma.ext h ?_ + . simp + . dsimp at h ⊢ + rw! [h] + apply heq_of_eq + ext + simp + ) + +end CategoryTheory diff --git a/Poly/ForMathlib/CategoryTheory/NatIso.lean b/Poly/ForMathlib/CategoryTheory/NatIso.lean new file mode 100644 index 0000000..104c37b --- /dev/null +++ b/Poly/ForMathlib/CategoryTheory/NatIso.lean @@ -0,0 +1,25 @@ +/- +Copyright (c) 2025 Wojciech Nawrocki. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Wojciech Nawrocki +-/ + +import Mathlib.CategoryTheory.NatIso + +namespace CategoryTheory.NatIso + +variable {𝒞 𝒟 ℰ : Type*} [Category 𝒞] [Category 𝒟] [Category ℰ] + +/-- Natural isomorphism of bifunctors from naturality in both arguments. -/ +def ofComponents₂ {F G : 𝒞 ⥤ 𝒟 ⥤ ℰ} + (app : ∀ Γ X, (F.obj Γ).obj X ≅ (G.obj Γ).obj X) + (naturality_left : ∀ {Γ Δ : 𝒞} (X : 𝒟) (σ : Γ ⟶ Δ), + (F.map σ).app X ≫ (app Δ X).hom = (app Γ X).hom ≫ (G.map σ).app X := by aesop_cat) + (naturality_right : ∀ {X Y : 𝒟} (Γ : 𝒞) (f : X ⟶ Y), + (F.obj Γ).map f ≫ (app Γ Y).hom = (app Γ X).hom ≫ (G.obj Γ).map f := by aesop_cat) : + F ≅ G := + NatIso.ofComponents + (fun Γ => NatIso.ofComponents (app Γ) (fun f => by simpa using naturality_right Γ f)) + (fun σ => by ext X : 2; simpa using naturality_left X σ) + +end CategoryTheory.NatIso diff --git a/Poly/Util.lean b/Poly/Util.lean index 26125fb..6a8b0c0 100644 --- a/Poly/Util.lean +++ b/Poly/Util.lean @@ -1,6 +1,6 @@ import Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq -import Mathlib.CategoryTheory.Comma.Over +import Mathlib.CategoryTheory.Comma.Over.Basic /-! Miscellaneous results that don't fit anywhere else. -/ @@ -8,13 +8,6 @@ namespace CategoryTheory variable {𝒞 𝒟 : Type*} [Category 𝒞] [Category 𝒟] -/-! ## Pullbacks -/ - -@[simp] -lemma Limits.pullback.lift_fst_snd {X Y Z : 𝒞} {f : X ⟶ Z} {g : Y ⟶ Z} [HasPullback f g] (eq) : - pullback.lift (pullback.fst f g) (pullback.snd f g) eq = 𝟙 (pullback f g) := by - ext <;> simp - /-! ## `eqToHom` -/ /-- Note: if possible, @@ -56,42 +49,27 @@ lemma Over.eqToHom_eq_homMk {E B : 𝒞} (f g : E ⟶ B) (eq : f = g) : namespace Over +/-- A variant of `homMk_comp` that can trigger in `simp`. -/ @[simp] -lemma homMk_comp {X Y Z W : 𝒞} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) (fgh_comp) : +lemma homMk_comp' {X Y Z W : 𝒞} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) (fgh_comp) : homMk (U := mk (f ≫ g ≫ h)) (f ≫ g) fgh_comp = homMk f ≫ homMk (U := mk (g ≫ h)) (V := mk h) g := rfl @[simp] -lemma homMk_comp_assoc {X Y Z W : 𝒞} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) (fgh_comp) : +lemma homMk_comp'_assoc {X Y Z W : 𝒞} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) (fgh_comp) : homMk (U := mk ((f ≫ g) ≫ h)) (f ≫ g) fgh_comp = homMk f ≫ homMk (U := mk (g ≫ h)) (V := mk h) g := rfl -/-- This is useful when `homMk (· ≫ ·)` appears under `Functor.map` or a natural equivalence. -/ -lemma homMk_comp' {B : 𝒞} {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 := - rfl - -@[simp] -lemma left_homMk {B : 𝒞} {U V : Over B} (f : U ⟶ V) (h) : homMk f.left h = f := - rfl - @[simp] lemma homMk_id {B : 𝒞} (U : Over B) (h) : homMk (𝟙 U.left) h = 𝟙 U := rfl +/-- A variant of `homMk_id` that `simp` can use when `X ≢ U.left` syntactically. -/ @[simp] --- `homMk_id` does not trigger if `X ≢ U.left` syntactically lemma homMk_id' {B : 𝒞} (f : X ⟶ B) (h) : homMk (𝟙 X) h = 𝟙 (mk f) := rfl --- -- Probably bad as a simp lemma? --- lemma homMk_id' {E B : 𝒞} {f g : E ⟶ B} (h) : --- homMk (U := Over.mk f) (V := Over.mk g) (𝟙 E) h = --- (Over.isoMk (Iso.refl E) (by simpa using h)).hom := by --- ext; simp - end Over end CategoryTheory From 4010c7b7b9e999f3e5e955da10cbbe11cabc4773 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Sat, 15 Mar 2025 23:16:47 -0400 Subject: [PATCH 09/18] feat: use Functor.Elements --- Poly/DepFunctor/Sigma.lean | 216 ++++++++----------- Poly/ForMathlib/CategoryTheory/Elements.lean | 39 ++++ Poly/ForMathlib/CategoryTheory/NatIso.lean | 1 + Poly/ForMathlib/CategoryTheory/Types.lean | 37 ++++ 4 files changed, 161 insertions(+), 132 deletions(-) create mode 100644 Poly/ForMathlib/CategoryTheory/Elements.lean create mode 100644 Poly/ForMathlib/CategoryTheory/Types.lean diff --git a/Poly/DepFunctor/Sigma.lean b/Poly/DepFunctor/Sigma.lean index 24b6a51..cb3bad7 100644 --- a/Poly/DepFunctor/Sigma.lean +++ b/Poly/DepFunctor/Sigma.lean @@ -4,167 +4,119 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Wojciech Nawrocki -/ -import SEq.Tactic.DepRewrite +import Lean.Elab.Tactic.DiscrTreeKey +import Mathlib.CategoryTheory.Elements +import Mathlib.CategoryTheory.Functor.Currying +import Mathlib.CategoryTheory.Functor.Category -import Poly.DepFunctor.Basic +import SEq.Tactic.DepRewrite +import Poly.ForMathlib.CategoryTheory.Elements import Poly.ForMathlib.CategoryTheory.NatIso - -namespace CategoryTheory - -variable {𝒞 𝒟 ℰ : Type*} [Category 𝒞] [Category 𝒟] [Category ℰ] - -/-! ## Dependent sum functor -/ - -namespace DepFunctor +import Poly.ForMathlib.CategoryTheory.Types + +open private mkKey from Lean.Elab.Tactic.DiscrTreeKey in +open Lean Meta Elab Tactic in +/-- Print the `DiscrTree` key of the current `conv` mode target. -/ +macro "discr_tree_key" : conv => + `(conv| tactic => run_tac do + let g ← Conv.getLhs + logInfo <| ← DiscrTree.keysAsPattern <| ← mkKey g false) + +open private mkKey from Lean.Elab.Tactic.DiscrTreeKey in +open Lean Meta Elab Tactic Conv in +/-- Attempt to match the current `conv` mode target +against the LHS of the specified theorem. -/ +elab "discr_tree_match" n:ident : conv => do + let c ← realizeGlobalConstNoOverloadWithInfo n + let ci ← getConstInfo c + let e ← Conv.getLhs + let ciKey ← mkKey ci.type true + let gKey ← mkKey e false + logInfo m!"{ciKey.zip gKey |>.map fun (a, b) => m!"{a} := {b}"}" + logInfo m!"{← DiscrTree.keysAsPattern ciKey} := {← DiscrTree.keysAsPattern gKey}" + +namespace CategoryTheory.Functor + +variable {𝒞 𝒟 : Type*} [Category 𝒞] [Category 𝒟] /-- Given functors `F : 𝒞 ⥤ Type v` and `G : ∫F ⥤ 𝒟 ⥤ Type v`, -produce the functor `(X, Y) ↦ (b : F(X)) × G((X, b))(Y)`. +produce the functor `(C, D) ↦ (a : F(C)) × G((C, a))(D)`. This is a dependent sum that varies naturally -in a parameter `X` of the first component, -and a parameter `Y` of the second component. +in a parameter `C` of the first component, +and a parameter `D` of the second component. We use this to package and compose natural equivalences -where one (or both) sides is a dependent sum, e.g. +where one side (or both) is a dependent sum, e.g. ``` -H(X) ⟶ I(Y) +H(C) ⟶ I(D) ========================= -(b : F(X)) × (G(X, b)(Y)) +(a : F(C)) × (G(C, a)(D)) ``` is a natural isomorphism of bifunctors `𝒞ᵒᵖ ⥤ 𝒟 ⥤ Type v` -given by `(X, Y) ↦ H(X) ⟶ I(Y)` and `G.Sigma`. -/ +given by `(C, D) ↦ H(C) ⟶ I(D)` and `G.Sigma`. -/ @[simps!] -def Sigma.{v} {F : 𝒞 ⥤ Type v} (G : DepFunctor F (𝒟 ⥤ Type v)) : 𝒞 ⥤ 𝒟 ⥤ Type v := by +/- Q: Is it necessary to special-case bifunctors? +(1) General case `G : F.Elements ⥤ Type v` needs +a functor `F'` s.t. `F'.Elements ≅ F.Elements × 𝒟`; very awkward. +(2) General case `F : 𝒞 ⥤ 𝒟`, `G : ∫F ⥤ 𝒟`: +- what conditions are needed on `𝒟` for `∫F` to make sense? +- what about for `ΣF. G : 𝒞 ⥤ 𝒟` to make sense? +- known concrete instances are `𝒟 ∈ {Type, Cat, Grpd}` -/ +def Sigma.{v,u} {F : 𝒞 ⥤ Type v} (G : F.Elements ⥤ 𝒟 ⥤ Type u) : 𝒞 ⥤ 𝒟 ⥤ Type (max v u) := by refine curry.obj { - obj := fun (Γ, X) => (b : F.obj Γ) × ((G.obj b).obj X) - map := fun (σ, f) ⟨b, e⟩ => - ⟨F.map σ b, (G.map σ b _ rfl).app _ ((G.obj b).map f e)⟩ + 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)⟩ map_id := ?_ map_comp := ?_ - } <;> ( + } <;> { intros - ext ⟨b, e⟩ : 1 + ext ⟨a, b⟩ : 1 dsimp congr! 1 with h . simp . rw! [h]; simp [FunctorToTypes.naturality] - ) - -def Sigma.isoCongrLeft.{v} (F₁ F₂ : 𝒞 ⥤ Type v) (G : DepFunctor F₁ (𝒟 ⥤ Type v)) - (i : F₂ ≅ F₁) : G.Sigma ≅ (G.isoLeft i).Sigma := by + } + +def Sigma.isoCongrLeft.{v,u} {F₁ F₂ : 𝒞 ⥤ Type v} + /- Q: What kind of map `F₂.Elements ⥤ F₁.Elements` + could `NatTrans.mapElements i.hom` generalize to? + We need to send `x ∈ F₂(C)` to something in `F₁(C)`; + so maybe the map has to at least be over `𝒞`. -/ + (G : F₁.Elements ⥤ 𝒟 ⥤ Type u) (i : F₂ ≅ F₁) : + Sigma (NatTrans.mapElements i.hom ⋙ G) ≅ Sigma G := by refine NatIso.ofComponents₂ - (fun Γ X => Equiv.toIso { - toFun := fun ⟨b, e⟩ => ⟨i.inv.app Γ b, cast (by simp) e⟩ - invFun := fun ⟨b, e⟩ => ⟨i.hom.app Γ b, e⟩ + (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 - }) ?_ ?_ <;> ( + }) ?_ ?_ <;> { intros ext : 1 dsimp apply let h := ?_; Sigma.ext h ?_ . simp [FunctorToTypes.naturality] . dsimp [Sigma] at h ⊢ - rw! [ - ← h, - FunctorToTypes.inv_hom_id_app_apply, - FunctorToTypes.inv_hom_id_app_apply, - ] - simp - ) + rw! [← h] + simp [NatTrans.mapElements] + } -def Sigma.isoCongrRight.{v} (F : 𝒞 ⥤ Type v) (G₁ G₂ : DepFunctor F (𝒟 ⥤ Type v)) - (i : G₁ ≅ G₂) : - G₁.Sigma ≅ G₂.Sigma := - NatIso.ofComponents₂ - (fun Γ X => Equiv.toIso { - toFun := fun ⟨b, e⟩ => ⟨b, (i.hom.app b).app X e⟩ - invFun := fun ⟨b, e⟩ => ⟨b, (i.inv.app b).app X e⟩ - left_inv := fun ⟨b, e⟩ => by simp - right_inv := fun ⟨b, e⟩ => by simp - }) - (fun X σ => by - ext ⟨b, e⟩ - have := congr_fun (DepNatTrans.naturality_app i.hom σ b _ rfl X) e - dsimp at this - simp [Sigma, this]) - (fun Γ f => by - ext ⟨b, e⟩ +def Sigma.isoCongrRight.{v,u} {F : 𝒞 ⥤ Type v} {G₁ G₂ : F.Elements ⥤ 𝒟 ⥤ Type u} (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 + }) ?_ ?_ <;> { + intros + ext : 1 dsimp - simp only [Sigma, prod_Hom, curry_obj_obj_map, Sigma.mk.injEq, FunctorToTypes.map_id_apply, - heq_eq_eq, true_and] - rw! [F.map_id Γ] - simp [FunctorToTypes.naturality]) - -end DepFunctor - -open Limits in -/-- The functor `(b : Γ ⟶ B) ↦ Hom(dom(b*p), -)`. -/ -noncomputable def pullbackDep.{v} {𝒞 : Type*} [Category.{v} 𝒞] [HasPullbacks 𝒞] - {E B : 𝒞} (p : E ⟶ B) : - DepFunctor (yoneda.obj B) (𝒞 ⥤ Type v) where - obj _ b := coyoneda.obj <| Opposite.op <| pullback b p - map _ _ σ _ _ eq := - coyoneda.map <| Quiver.Hom.op <| - pullback.lift (pullback.fst .. ≫ σ.unop) (pullback.snd ..) - (by rw [eq]; simp [pullback.condition]) - map_id := by simp - map_comp := by - intros - ext : 3 - dsimp - simp only [← Category.assoc] - congr 1 - ext <;> simp - --- TODO: move elsewhere -@[simps] -def bifunctor_comp_snd {𝒟' : Type*} [Category 𝒟'] (F : 𝒟' ⥤ 𝒟) (P : 𝒞 ⥤ 𝒟 ⥤ ℰ) : 𝒞 ⥤ 𝒟' ⥤ ℰ where - obj Γ := F ⋙ P.obj Γ - map σ := whiskerLeft F (P.map σ) - -/-- The hom-functor `𝒞/Aᵒᵖ ⥤ 𝒞/A ⥤ Type` given by -`(X, g : X ⟶ A) (Y, f : Y ⟶ A) ↦ 𝒞/A(g, f)` -written as a dependent functor `∫y(A) ⥤ 𝒞/A ⥤ Type`. -This is to express the dependent sum `Σ(g : X ⟶ A), 𝒞/A(g, f)`. -/ -@[simps] -def overDep (A : 𝒞) : DepFunctor (yoneda.obj A) (Over A ⥤ Type) where - obj _ g := coyoneda.obj <| Opposite.op <| Over.mk g - map _ _ σ f g eq := coyoneda.map <| Quiver.Hom.op <| Over.homMk σ.unop (by simp [eq]) - map_id := by simp - map_comp := by - intros - ext : 3 - dsimp - ext : 1 - simp - --- TODO: this in mathlib? -@[simps] -def Over_equiv {A : 𝒞} (X : 𝒞) (f : Over A) : (X ⟶ f.left) ≃ (b : X ⟶ A) × (Over.mk b ⟶ f) where - toFun g := ⟨g ≫ f.hom, Over.homMk g rfl⟩ - invFun g := g.2.left - left_inv _ := by simp - right_inv := fun x => by - dsimp; congr! 1 with h - . simp - . rw! [h] - simp - -/-- `𝒞(X, Over.forget f) ≅ Σ(g: X ⟶ A), 𝒞/A(g, f)` -/ -def Over_iso (A : 𝒞) : - bifunctor_comp_snd (Over.forget A) (coyoneda (C := 𝒞)) ≅ (overDep A).Sigma := by - refine NatIso.ofComponents₂ (fun Γ U => Equiv.toIso <| Over_equiv Γ.unop U) ?_ ?_ <;> ( - intros - dsimp - ext : 1 - apply let h := ?_; Sigma.ext h ?_ - . simp - . dsimp at h ⊢ - rw! [h] - apply heq_of_eq - ext - simp - ) - -end CategoryTheory + apply let h := ?_; Sigma.ext h ?_ + . simp + . dsimp [Sigma] at h ⊢ + simp [FunctorToTypes.binaturality_left, FunctorToTypes.binaturality_right] + } diff --git a/Poly/ForMathlib/CategoryTheory/Elements.lean b/Poly/ForMathlib/CategoryTheory/Elements.lean new file mode 100644 index 0000000..e499531 --- /dev/null +++ b/Poly/ForMathlib/CategoryTheory/Elements.lean @@ -0,0 +1,39 @@ +import Mathlib.CategoryTheory.Elements + +namespace CategoryTheory + +variable {𝒞 𝒟 : Type*} [Category 𝒞] [Category 𝒟] + +namespace CategoryOfElements + +variable (F : 𝒞 ⥤ Type*) (G : F.Elements ⥤ 𝒟) + +-- TODO: These are the same definition; but neither works with dot notation on `Hom` :( +#check NatTrans.mapElements +#check CategoryOfElements.map + +-- Cannot add `simps` for defs in imported modules +-- attribute [simps map] NatTrans.mapElements + +@[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⟩) := + 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 (α := Y ⟶ Z) g (by 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)⟩ + set f : X ⟶ Y := ⟨f, rfl⟩ + set g : Y ⟶ Z := ⟨g, rfl⟩ + show G.map (f ≫ g) = G.map f ≫ G.map g + simp + +end CategoryOfElements + +end CategoryTheory diff --git a/Poly/ForMathlib/CategoryTheory/NatIso.lean b/Poly/ForMathlib/CategoryTheory/NatIso.lean index 104c37b..373c37a 100644 --- a/Poly/ForMathlib/CategoryTheory/NatIso.lean +++ b/Poly/ForMathlib/CategoryTheory/NatIso.lean @@ -13,6 +13,7 @@ variable {𝒞 𝒟 ℰ : Type*} [Category 𝒞] [Category 𝒟] [Category ℰ] /-- Natural isomorphism of bifunctors from naturality in both arguments. -/ def ofComponents₂ {F G : 𝒞 ⥤ 𝒟 ⥤ ℰ} (app : ∀ Γ X, (F.obj Γ).obj X ≅ (G.obj Γ).obj X) + -- binaturality_left? (naturality_left : ∀ {Γ Δ : 𝒞} (X : 𝒟) (σ : Γ ⟶ Δ), (F.map σ).app X ≫ (app Δ X).hom = (app Γ X).hom ≫ (G.map σ).app X := by aesop_cat) (naturality_right : ∀ {X Y : 𝒟} (Γ : 𝒞) (f : X ⟶ Y), diff --git a/Poly/ForMathlib/CategoryTheory/Types.lean b/Poly/ForMathlib/CategoryTheory/Types.lean new file mode 100644 index 0000000..5319d53 --- /dev/null +++ b/Poly/ForMathlib/CategoryTheory/Types.lean @@ -0,0 +1,37 @@ +/- +Copyright (c) 2025 Wojciech Nawrocki. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Wojciech Nawrocki +-/ + +import Mathlib.CategoryTheory.Types + +namespace CategoryTheory.FunctorToTypes + +/-! Gross lemmas about bifunctors into `Type`. +Is there a better way? +Mathlib doesn't seem to think so: +see `hom_inv_id_app`, `hom_inv_id_app_app`, `hom_inv_id_app_app_app`. +Can a `simproc` that tries `congr_fun/congr_arg simpLemma` work? -/ + +universe w +variable {𝒞 𝒟 : Type*} [Category 𝒞] [Category 𝒟] (F G : 𝒞 ⥤ 𝒟 ⥤ Type w) + {C₁ C₂ : 𝒞} {D₁ D₂ : 𝒟} + +theorem binaturality_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 + +theorem binaturality_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 .. + +@[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 + +@[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 From 3c8bab73a867cba05c15a1280e4a1bcaa0a2ef4f Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Tue, 18 Mar 2025 14:20:16 -0400 Subject: [PATCH 10/18] feat: experiments --- Poly/DepFunctor/PullbackUPs.lean | 124 +++++++++++++++++++++++++++++++ 1 file changed, 124 insertions(+) create mode 100644 Poly/DepFunctor/PullbackUPs.lean diff --git a/Poly/DepFunctor/PullbackUPs.lean b/Poly/DepFunctor/PullbackUPs.lean new file mode 100644 index 0000000..fe1fd4b --- /dev/null +++ b/Poly/DepFunctor/PullbackUPs.lean @@ -0,0 +1,124 @@ +import Poly.DepFunctor.Sigma + +/-! ### Three ways to state the UP of pullbacks -/ + +open CategoryTheory Functor Limits + +universe v u +variable {𝒞 : Type u} [Category.{v} 𝒞] +variable {X Y Z : 𝒞} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] + +/-! #### 1. Current approach -/ + +noncomputable def pullbackHomEquiv (W : 𝒞) : + (W ⟶ pullback f g) ≃ (i : W ⟶ X) × (j : W ⟶ Y) ×' i ≫ f = j ≫ g where + toFun h := ⟨h ≫ pullback.fst f g, h ≫ pullback.snd f g, by simp[pullback.condition]⟩ + invFun x := pullback.lift x.1 x.2.1 x.2.2 + left_inv _ := pullback.hom_ext (by simp) (by simp) + right_inv := by rintro ⟨_,_,_⟩; congr!; simp; simp + +-- Issue: this kind of naturality statement does not easily compose +-- when equivalences are chained, e.g. using `Equiv.sigmaCongrLeft`. +theorem naturality_left {W W' : 𝒞} (h : W ⟶ W') (k : W' ⟶ pullback f g) : + let p := pullbackHomEquiv f g W' k + pullbackHomEquiv f g W (h ≫ k) = ⟨h ≫ p.1, h ≫ p.2.1, by simp [p.2.2]⟩ := by + dsimp [pullbackHomEquiv] + congr! 1 with h + . simp + . rw! [h]; simp + +/-! #### 2. Natural iso. of cone functors -/ + +/-- Sends `W` to the type of cones on the cospan `👉f👉👈g👈` with apex `W`, +i.e., tuples `(i : W ⟶ X) × (j : W ⟶ Y) ×' (i ≫ f = j ≫ g)`. -/ +def pullbackCones : 𝒞ᵒᵖ ⥤ Type v := + (cospan f g).cones + +omit [HasPullback f g] in +@[simp] +theorem PullbackCone.eta' (c : PullbackCone f g) : PullbackCone.mk c.fst c.snd c.condition = c := by + dsimp [PullbackCone.mk] + congr 2 + ext i : 1 + rcases i with _ | ⟨_ | _⟩ <;> simp + +omit [HasPullback f g] in +theorem PullbackCone.mk_comp_π {W' : 𝒞} (h : W' ⟶ W) (i : W ⟶ X) (j : W ⟶ Y) + (eq : (h ≫ i) ≫ f = (h ≫ j) ≫ g) eq' : + (PullbackCone.mk (h ≫ i) (h ≫ j) eq).π = (const _).map h ≫ (PullbackCone.mk i j eq').π := by + ext i : 2 + dsimp + rcases i with _ | ⟨_ | _⟩ <;> simp + +/-- We can also define `pullbackCones` using `PullbackCone`, but storing the apex +- bumps up the universe level; and +- forces the use of `eqToHom`. -/ +def pullbackCones' : 𝒞ᵒᵖ ⥤ Type (max v u) where + obj W := { c : PullbackCone f g // W.unop = c.pt } + map f := fun ⟨c, eq⟩ => ⟨ + PullbackCone.mk + (f.unop ≫ eqToHom eq ≫ c.fst) + (f.unop ≫ eqToHom eq ≫ c.snd) + (by rw! (castMode := .all) [eq]; simp [c.condition]), + rfl⟩ + map_id _ := by dsimp; ext ⟨_, eq⟩ : 2; rw! [eq]; simp + map_comp _ _ := by ext : 1; simp + +-- This composes more directly than `naturality_left` above. +noncomputable def pullbackConesIso : yoneda.obj (pullback f g) ≅ pullbackCones f g := + NatIso.ofComponents + (fun W => Equiv.toIso { + toFun h := + (PullbackCone.mk + (h ≫ pullback.fst f g) (h ≫ pullback.snd f g) (by simp [pullback.condition])).π + invFun c := + let c' : PullbackCone f g := ⟨W.unop, c⟩ + pullback.lift c'.fst c'.snd c'.condition + left_inv _ := by + dsimp + ext : 1 <;> simp [PullbackCone.fst, PullbackCone.snd] + right_inv π := by + -- Nasty proof because there is good API for `PullbackCone`, + -- but not for `pullbackCones`. + dsimp [PullbackCone.mk] + congr 1 with i + have := π.naturality (WidePullbackShape.Hom.term .left) + dsimp at this + rcases i with _ | ⟨_ | _⟩ <;> simp [PullbackCone.fst, ← this] + }) + (fun _ => by + ext : 1 + dsimp + rw [PullbackCone.mk_comp_π (eq' := by simp [pullback.condition]), + PullbackCone.mk_comp_π (eq' := by simp [pullback.condition])] + simp [pullbackCones, Functor.cones]) + +/-! #### 3. Equivalence with category of cones + +I didn't finish constructing this approach as it seems very awkward. -/ + +@[simps] +def PullbackCone.mkHom {W : 𝒞} (i₁ : W' ⟶ X) (j₁ : W' ⟶ Y) (i₂ : W ⟶ X) (j₂ : W ⟶ Y) + (eq₁ : i₁ ≫ f = j₁ ≫ g) (eq₂ : i₂ ≫ f = j₂ ≫ g) + (h : W' ⟶ W) (w_i : h ≫ i₂ = i₁) (w_j : h ≫ j₂ = j₁) : + PullbackCone.mk i₁ j₁ eq₁ ⟶ PullbackCone.mk i₂ j₂ eq₂ where + hom := h + w := by rintro (_ | ⟨_ | _⟩) <;> simp [reassoc_of% w_i, w_i, w_j] + +noncomputable def pullbackIso : Over (pullback f g) ≌ PullbackCone f g where + functor := { + obj U := PullbackCone.mk (U.hom ≫ pullback.fst f g) (U.hom ≫ pullback.snd f g) + (by simp [pullback.condition]) + map t := PullbackCone.mkHom f g (h := t.left) (w_i := by simp [t.w]) (w_j := by simp [t.w]) .. + map_id := by intros; ext : 1; simp + map_comp := by intros; ext : 1; simp + } + inverse := { + obj c := Over.mk (pullback.lift c.fst c.snd c.condition) + map t := Over.homMk t.hom (by dsimp; ext <;> simp) + map_id := by intros; ext : 1; simp + map_comp := by intros; ext : 1; simp + } + unitIso := NatIso.ofComponents (fun X => eqToIso sorry) sorry + counitIso := NatIso.ofComponents (fun X => eqToIso sorry) sorry + functor_unitIso_comp := sorry From 47db45e478dd08f7b0ea1c335722ad526a3a4d37 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Wed, 19 Mar 2025 01:42:51 -0400 Subject: [PATCH 11/18] feat: UvPoly.iso_Sigma --- Poly/DepFunctor/Basic.lean | 156 ------------------------------- Poly/DepFunctor/Sigma.lean | 185 +++++++++++++++++++++++++++++++++++-- Poly/UvPoly.lean | 124 +++++++++++++++---------- 3 files changed, 251 insertions(+), 214 deletions(-) delete mode 100644 Poly/DepFunctor/Basic.lean diff --git a/Poly/DepFunctor/Basic.lean b/Poly/DepFunctor/Basic.lean deleted file mode 100644 index e68033e..0000000 --- a/Poly/DepFunctor/Basic.lean +++ /dev/null @@ -1,156 +0,0 @@ -/- -Copyright (c) 2025 Wojciech Nawrocki. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Wojciech Nawrocki --/ - -import Poly.Util - -namespace CategoryTheory - -variable {𝒞 𝒟 ℰ : Type*} [Category 𝒞] [Category 𝒟] [Category ℰ] - -/-! ## Dependent functors -/ - -/-- A functor into `𝒟` that depends on `F` -in other words `∫F ⥤ 𝒟` where all the `F(Γ)` are discrete, -spelled out in elementary terms. - -(In the general case, we would have -`map : ∀ ⦃Γ Δ⦄ ⦃b : F.obj Γ⦄ ⦃c : F.obj Δ⦄ - (σ : Γ ⟶ Δ) (f : F.map σ b ⟶ c), obj b ⟶ obj c`.) - -Equivalently, this is a (lax or strict or something) transformation `F ⟶ const 𝒟`. -/ --- NOTE: A more mathlib-ready, general approach might use `∫F ⥤ 𝒟`, --- and introduce a special-case constructor for discrete `F(Γ)` --- with an argument for each field of this structure. -/ -structure DepFunctor (F : 𝒞 ⥤ Type*) (𝒟 : Type*) [Category 𝒟] where - obj : ∀ ⦃Γ⦄, F.obj Γ → 𝒟 - -- Forded to avoid `eqToHom` in the axioms. - map : ∀ ⦃Γ Δ⦄ (σ : Γ ⟶ Δ) (b : F.obj Γ) (c : F.obj Δ), c = F.map σ b → (obj b ⟶ obj c) - map_id : ∀ ⦃Γ⦄ b h, map (𝟙 Γ) b b h = 𝟙 (obj b) := by aesop_cat - /-- **Note about `simp`.** - The two `map` equalities in the LHS imply the one in the RHS, but not vice-versa. - This axiom is thus stated in a "packing" rather than an "unpacking" direction, - so that `simp` can apply it automatically by matching `h₁` and `h₂`. - However, we do not mark it `simp` globally, - preferring `map_comp'` whenever it applies. -/ - map_comp : ∀ ⦃Γ Δ Θ⦄ (σ : Γ ⟶ Δ) (τ : Δ ⟶ Θ) b c d h₁ h₂, - map σ b c h₁ ≫ map τ c d h₂ = map (σ ≫ τ) b d (by simp [h₁, h₂]) := by aesop_cat - -namespace DepFunctor - -attribute [simp] map_id - -/-- Specialized variant of `(map_comp ..).symm` that `simp` can match against. -/ -@[simp] -theorem map_comp' {F : 𝒞 ⥤ Type*} {G : DepFunctor F 𝒟} ⦃Γ Δ Θ⦄ (σ : Γ ⟶ Δ) (τ : Δ ⟶ Θ) b h : - G.map (σ ≫ τ) b (F.map τ (F.map σ b)) h = G.map σ b (F.map σ b) rfl ≫ G.map τ _ _ rfl := - (G.map_comp σ τ ..).symm - -@[simps] -def isoLeft.{v} {F₁ F₂ : 𝒞 ⥤ Type v} (G : DepFunctor F₁ 𝒟) (i : F₂ ≅ F₁) : DepFunctor F₂ 𝒟 where - obj Γ b := G.obj (i.hom.app Γ b) - map Γ _ σ _ _ eq := G.map σ _ _ (by simp [eq, FunctorToTypes.naturality]) - map_id := by simp - map_comp := by simp [G.map_comp] - -end DepFunctor - -@[ext] -structure DepNatTrans {F : 𝒞 ⥤ Type*} (G₁ G₂ : DepFunctor F 𝒟) where - app : ∀ ⦃Γ⦄ (b : F.obj Γ), G₁.obj b ⟶ G₂.obj b - naturality : ∀ ⦃Γ Δ⦄ (σ : Γ ⟶ Δ) (b : F.obj Γ) (c : F.obj Δ) h, - app b ≫ G₂.map σ b c h = G₁.map σ b c h ≫ app c := by aesop_cat - -@[simps] -instance (F : 𝒞 ⥤ Type*) : Category (DepFunctor F 𝒟) where - Hom := DepNatTrans - id G := { app := fun _ _ => 𝟙 _ } - comp η ν := { - app := fun _ b => η.app b ≫ ν.app b - naturality := by simp [reassoc_of% η.naturality, ν.naturality] - } - -namespace DepNatTrans - -variable {F : 𝒞 ⥤ Type*} {Γ : 𝒞} (b : F.obj Γ) - -@[ext] -theorem ext' {G₁ G₂ : DepFunctor F 𝒟} {α β : G₁ ⟶ G₂} (w : α.app = β.app) : α = β := - DepNatTrans.ext w - -@[simp] -theorem id_app (G₁ : DepFunctor F 𝒟) : (𝟙 G₁ : G₁ ⟶ G₁).app b = 𝟙 (G₁.obj b) := rfl - -@[reassoc (attr := simp)] -theorem comp_app {G₁ G₂ G₃ : DepFunctor F 𝒟} (α : G₁ ⟶ G₂) (β : G₂ ⟶ G₃) : - (α ≫ β).app b = α.app b ≫ β.app b := rfl - -theorem naturality_app {G₁ G₂ : DepFunctor F (𝒟 ⥤ ℰ)} (α : G₁ ⟶ G₂) - {Γ Δ : 𝒞} (σ : Γ ⟶ Δ) (b : F.obj Γ) (c : F.obj Δ) h (X : 𝒟) : - (G₁.map σ b c h).app X ≫ (α.app c).app X = (α.app b).app X ≫ (G₂.map σ b c h).app X := - (congr_fun (congr_arg NatTrans.app (α.naturality σ b c h)) X).symm - -end DepNatTrans - -namespace DepNatIso - -variable {F : 𝒞 ⥤ Type*} {G₁ G₂ : DepFunctor F 𝒟} - -@[reassoc (attr := simp)] -theorem hom_inv_id_app {Γ : 𝒞} (α : G₁ ≅ G₂) (b : F.obj Γ) : - α.hom.app b ≫ α.inv.app b = 𝟙 (G₁.obj b) := by - simp [← DepNatTrans.comp_app] - -@[reassoc (attr := simp)] -theorem inv_hom_id_app {Γ : 𝒞} (α : G₁ ≅ G₂) (b : F.obj Γ) : - α.inv.app b ≫ α.hom.app b = 𝟙 (G₂.obj b) := by - simp [← DepNatTrans.comp_app] - -instance hom_app_isIso {Γ : 𝒞} (α : G₁ ≅ G₂) (b : F.obj Γ) : IsIso (α.hom.app b) := - ⟨α.inv.app b, by simp⟩ - -instance inv_app_isIso {Γ : 𝒞} (α : G₁ ≅ G₂) (b : F.obj Γ) : IsIso (α.inv.app b) := - ⟨α.hom.app b, by simp⟩ - -def ofComponents - (app : ∀ {Γ} (b : F.obj Γ), G₁.obj b ≅ G₂.obj b) - (naturality : ∀ {Γ Δ} (σ : Γ ⟶ Δ) (b : F.obj Γ) (c : F.obj Δ) h, - (app b).hom ≫ G₂.map σ b c h = G₁.map σ b c h ≫ (app c).hom) : - G₁ ≅ G₂ where - hom := { app := fun _ b => (app b).hom } - inv := { - app := fun _ b => (app b).inv - naturality := fun _ _ σ b c h => by - have : (app b).inv ≫ (app b).hom ≫ G₂.map σ b c h ≫ (app c).inv = - (app b).inv ≫ G₁.map σ b c h ≫ (app c).hom ≫ (app c).inv := by - simp [reassoc_of% naturality] - simpa using this.symm - } - -variable {G₁ G₂ : DepFunctor F (Type v)} - -@[simp] -theorem hom_inv_id_app_apply {Γ : 𝒞} (α : G₁ ≅ G₂) (X : F.obj Γ) (x) : - α.inv.app X (α.hom.app X x) = x := - congr_fun (hom_inv_id_app α X) x - -@[simp] -theorem inv_hom_id_app_apply {Γ : 𝒞} (α : G₁ ≅ G₂) (X : F.obj Γ) (x) : - α.hom.app X (α.inv.app X x) = x := - congr_fun (inv_hom_id_app α X) x - -variable {G₁ G₂ : DepFunctor F (𝒟 ⥤ Type v)} - -@[simp] -theorem hom_inv_id_app_app_apply {Γ : 𝒞} (α : G₁ ≅ G₂) (b : F.obj Γ) (X : 𝒟) (x) : - (α.inv.app b).app X ((α.hom.app b).app X x) = x := - congr_fun (congr_fun (congr_arg NatTrans.app (hom_inv_id_app α b)) X) x - -@[simp] -theorem inv_hom_id_app_app_apply {Γ : 𝒞} (α : G₁ ≅ G₂) (b : F.obj Γ) (X : 𝒟) (x) : - (α.hom.app b).app X ((α.inv.app b).app X x) = x := - congr_fun (congr_fun (congr_arg NatTrans.app (inv_hom_id_app α b)) X) x - -end DepNatIso diff --git a/Poly/DepFunctor/Sigma.lean b/Poly/DepFunctor/Sigma.lean index cb3bad7..39c554b 100644 --- a/Poly/DepFunctor/Sigma.lean +++ b/Poly/DepFunctor/Sigma.lean @@ -5,14 +5,17 @@ Authors: Wojciech Nawrocki -/ import Lean.Elab.Tactic.DiscrTreeKey + import Mathlib.CategoryTheory.Elements import Mathlib.CategoryTheory.Functor.Currying import Mathlib.CategoryTheory.Functor.Category - +import Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback import SEq.Tactic.DepRewrite + import Poly.ForMathlib.CategoryTheory.Elements import Poly.ForMathlib.CategoryTheory.NatIso import Poly.ForMathlib.CategoryTheory.Types +import Poly.Util open private mkKey from Lean.Elab.Tactic.DiscrTreeKey in open Lean Meta Elab Tactic in @@ -37,7 +40,9 @@ elab "discr_tree_match" n:ident : conv => do namespace CategoryTheory.Functor -variable {𝒞 𝒟 : Type*} [Category 𝒞] [Category 𝒟] +universe w v u t s r + +variable {𝒞 : Type t} [Category.{u} 𝒞] {𝒟 : Type r} [Category.{s} 𝒟] /-- Given functors `F : 𝒞 ⥤ Type v` and `G : ∫F ⥤ 𝒟 ⥤ Type v`, produce the functor `(C, D) ↦ (a : F(C)) × G((C, a))(D)`. @@ -63,7 +68,7 @@ a functor `F'` s.t. `F'.Elements ≅ F.Elements × 𝒟`; very awkward. - what conditions are needed on `𝒟` for `∫F` to make sense? - what about for `ΣF. G : 𝒞 ⥤ 𝒟` to make sense? - known concrete instances are `𝒟 ∈ {Type, Cat, Grpd}` -/ -def Sigma.{v,u} {F : 𝒞 ⥤ Type v} (G : F.Elements ⥤ 𝒟 ⥤ Type u) : 𝒞 ⥤ 𝒟 ⥤ Type (max v u) := by +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⟩ => @@ -79,12 +84,12 @@ def Sigma.{v,u} {F : 𝒞 ⥤ Type v} (G : F.Elements ⥤ 𝒟 ⥤ Type u) : . rw! [h]; simp [FunctorToTypes.naturality] } -def Sigma.isoCongrLeft.{v,u} {F₁ F₂ : 𝒞 ⥤ Type v} +def Sigma.isoCongrLeft {F₁ F₂ : 𝒞 ⥤ Type w} /- Q: What kind of map `F₂.Elements ⥤ F₁.Elements` could `NatTrans.mapElements i.hom` generalize to? We need to send `x ∈ F₂(C)` to something in `F₁(C)`; so maybe the map has to at least be over `𝒞`. -/ - (G : F₁.Elements ⥤ 𝒟 ⥤ Type u) (i : F₂ ≅ F₁) : + (G : F₁.Elements ⥤ 𝒟 ⥤ Type v) (i : F₂ ≅ F₁) : Sigma (NatTrans.mapElements i.hom ⋙ G) ≅ Sigma G := by refine NatIso.ofComponents₂ (fun C D => Equiv.toIso { @@ -96,14 +101,14 @@ def Sigma.isoCongrLeft.{v,u} {F₁ F₂ : 𝒞 ⥤ Type v} intros ext : 1 dsimp - apply let h := ?_; Sigma.ext h ?_ + apply have h := ?_; Sigma.ext h ?_ . simp [FunctorToTypes.naturality] . dsimp [Sigma] at h ⊢ rw! [← h] simp [NatTrans.mapElements] } -def Sigma.isoCongrRight.{v,u} {F : 𝒞 ⥤ Type v} {G₁ G₂ : F.Elements ⥤ 𝒟 ⥤ Type u} (i : G₁ ≅ G₂) : +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 { @@ -115,8 +120,172 @@ def Sigma.isoCongrRight.{v,u} {F : 𝒞 ⥤ Type v} {G₁ G₂ : F.Elements ⥤ intros ext : 1 dsimp - apply let h := ?_; Sigma.ext h ?_ + apply have h := ?_; Sigma.ext h ?_ . simp . dsimp [Sigma] at h ⊢ simp [FunctorToTypes.binaturality_left, FunctorToTypes.binaturality_right] } + +end CategoryTheory.Functor + +/-! ### Profunctor operations -/ + +namespace CategoryTheory.Functor + +variable {𝒞 𝒟' 𝒟 ℰ : Type*} [Category 𝒞] [Category 𝒟'] [Category 𝒟] [Category ℰ] + +/-- Precompose a profunctor in the second argument. +Note that `G ⋙₂ F ⋙ P = F ⋙ G ⋙₂ P` definitionally. -/ +@[simps] +def comp₂ (F : 𝒟' ⥤ 𝒟) (P : 𝒞 ⥤ 𝒟 ⥤ ℰ) : 𝒞 ⥤ 𝒟' ⥤ ℰ where + obj Γ := F ⋙ P.obj Γ + map f := whiskerLeft F (P.map f) + +@[inherit_doc] +scoped [CategoryTheory] infixr:80 " ⋙₂ " => Functor.comp₂ + +@[simp] +theorem comp_comp₂ {𝒟'' : Type*} [Category 𝒟''] + (F : 𝒟'' ⥤ 𝒟') (G : 𝒟' ⥤ 𝒟) (P : 𝒞 ⥤ 𝒟 ⥤ ℰ) : + (F ⋙ G) ⋙₂ P = F ⋙₂ (G ⋙₂ P) := by + rfl + +@[simp] +-- Composition with `F,G` ordered like the arguments of `P` is considered 'simplified'. +theorem comp₂_comp {𝒞' : Type*} [Category 𝒞'] + (F : 𝒞' ⥤ 𝒞) (G : 𝒟' ⥤ 𝒟) (P : 𝒞 ⥤ 𝒟 ⥤ ℰ) : + G ⋙₂ (F ⋙ P) = F ⋙ (G ⋙₂ P) := by + rfl + +theorem comp₂_Sigma {F : 𝒞 ⥤ Type w} (G : 𝒟' ⥤ 𝒟) (P : F.Elements ⥤ 𝒟 ⥤ Type v) : + G ⋙₂ Sigma P = Sigma (G ⋙₂ P) := by + apply Functor.hext + . intro C + apply Functor.hext + . intro; simp + . intros + apply heq_of_eq + ext : 1 + apply Sigma.ext <;> simp + . intros + apply heq_of_eq + ext : 3 + apply Sigma.ext <;> simp + +@[simps!] +def 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 C f => by + have := congr_arg (P₂.obj C).map (i.hom.naturality f) + simp only [map_comp] at this + simp [this]) + +@[simps!] +def iso₂WhiskerLeft {P₁ P₂ : 𝒞 ⥤ 𝒟 ⥤ ℰ} (F : 𝒟' ⥤ 𝒟) (i : P₁ ≅ P₂) : F ⋙₂ P₁ ≅ F ⋙₂ P₂ := + iso₂ (Iso.refl F) i + +@[simps!] +def iso₂WhiskerRight {F₁ F₂ : 𝒟' ⥤ 𝒟} (i : F₁ ≅ F₂) (P : 𝒞 ⥤ 𝒟 ⥤ ℰ) : F₁ ⋙₂ P ≅ F₂ ⋙₂ P := + iso₂ i (Iso.refl P) + +end CategoryTheory.Functor + +/-! ### Natural isomorphisms-/ + +/-! #### Hom-types -/ + +namespace CategoryTheory.Functor + +universe v u +variable {𝒞 : Type u} [Category.{v} 𝒞] + +theorem comp₂_coyoneda_naturality_left {𝒞' : Type*} [Category 𝒞'] + (F : 𝒞' ⥤ 𝒞) (P : 𝒞ᵒᵖ ⥤ 𝒞' ⥤ Type v) (i : F ⋙₂ coyoneda (C := 𝒞) ⟶ P) (X Y : 𝒞) (Z : 𝒞') + (f : X ⟶ Y) (g : Y ⟶ F.obj Z) : + -- TODO: 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.binaturality_left] + +theorem comp₂_coyoneda_naturality_right {𝒞' : Type*} [Category 𝒞'] + (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.binaturality_right] + +end CategoryTheory.Functor + +/-! #### Over -/ + +namespace CategoryTheory.Over + +universe v u +variable {𝒞 : Type u} [Category.{v} 𝒞] + +-- Q: is this in mathlib? +@[simps] +def equiv_Sigma {A : 𝒞} (X : 𝒞) (U : Over A) : (X ⟶ U.left) ≃ (b : X ⟶ A) × (Over.mk b ⟶ U) where + toFun g := ⟨g ≫ U.hom, Over.homMk g rfl⟩ + invFun p := p.snd.left + left_inv _ := by simp + right_inv := fun _ => by + dsimp; 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) + } + inverse := { + obj := fun U => ⟨.op U.unop.left, U.unop.hom⟩ + map := fun f => ⟨.op f.unop.left, by simp⟩ + } + unitIso := NatIso.ofComponents Iso.refl (by simp) + 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]) + +/-- `𝒞(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 have h := ?_; Sigma.ext h ?_ + . simp + . dsimp at h ⊢ + rw! [h] + simp + . intros X Y U f + ext : 1 + dsimp + apply have h := ?_; Sigma.ext h ?_ + . simp + . dsimp at h ⊢ + rw! [h] + -- simp -- TODO: `homMk f.left ⋯` and `homMk (𝟙 _) ⋯` don't get simplified here + apply heq_of_eq + ext : 1 + simp + +end CategoryTheory.Over + +/-! #### Adjunction -/ + +namespace CategoryTheory.Adjunction + +variable {𝒞 𝒟 : Type*} [Category 𝒞] [Category 𝒟] + +def homIso {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]) + +end CategoryTheory.Adjunction diff --git a/Poly/UvPoly.lean b/Poly/UvPoly.lean index 1f75268..d8373bc 100644 --- a/Poly/UvPoly.lean +++ b/Poly/UvPoly.lean @@ -7,6 +7,8 @@ Authors: Sina Hazratpour import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.BeckChevalley -- LCCC.BeckChevalley import Mathlib.CategoryTheory.Functor.TwoSquare import Poly.ForMathlib.CategoryTheory.PartialProduct +import Poly.DepFunctor.Sigma + /-! # Polynomial Functor @@ -72,7 +74,7 @@ def prod {E' B'} (P : UvPoly E B) (Q : UvPoly E' B') [HasBinaryCoproducts C]: /-- For a category `C` with binary products, `P.functor : C ⥤ C` is the functor associated to a single variable polynomial `P : UvPoly E B`. -/ def functor [HasBinaryProducts C] (P : UvPoly E B) : C ⥤ C := - Over.star E ⋙ pushforward P.p ⋙ forget B + star E ⋙ pushforward P.p ⋙ forget B /-- The evaluation function of a polynomial `P` at an object `X`. -/ def apply (P : UvPoly E B) : C → C := (P.functor).obj @@ -236,7 +238,7 @@ def Total.ofHom {E' B' : C} (P : UvPoly E B) (Q : UvPoly E' B') (α : P.Hom Q) : namespace UvPoly -variable {C : Type*} [Category C] [HasTerminal C] [HasPullbacks C] +variable {C : Type u} [Category.{v} C] [HasTerminal C] [HasPullbacks C] instance : SMul C (Total C) where smul S P := Total.of (smul S P.poly) @@ -352,55 +354,77 @@ def equiv (P : UvPoly E B) (Γ : C) (X : C) : · simp only [proj_fst, lift_fst] · sorry -#exit - -/-- `UvPoly.equiv` is natural in `Γ`. -/ -lemma equiv_naturality_left {Δ Γ : C} (σ : Δ ⟶ Γ) (P : UvPoly E B) (X : C) - (f : Γ ⟶ P @ X) : - equiv P Δ X (σ ≫ f) = let ⟨b, e⟩ := equiv P Γ X f - ⟨σ ≫ b, pullback.lift (pullback.fst .. ≫ σ) (pullback.snd ..) - (assoc (obj := C) .. ▸ pullback.condition) ≫ e⟩ := by - dsimp - congr! with h - . simp [polyPair, partialProduct.liftAux] - . set g := _ ≫ (P.polyPair be).snd - rw [(_ : (P.polyPair (σ ≫ be)).snd = (pullback.congrHom h rfl).hom ≫ g)] - · generalize (P.polyPair (σ ≫ be)).fst = x at h - cases h - simp - · simp only [polyPair, comp_obj, homEquiv_counit, id_obj, comp_left, pullback_obj_left, - mk_left, mk_hom, star_obj_left, pullback_map_left, homMk_left, pullback.congrHom_hom, ← - assoc, g] - congr 2 - ext <;> simp - -/-- `UvPoly.equiv` is natural in `X`. -/ -lemma equiv_naturality_right {Γ X Y : C} +variable {Γ X : C} (P : UvPoly E B) + +/-- `𝒞(Γ, PₚX) ≅ Σ(b : Γ ⟶ B), 𝒞(b*p, X)` -/ +def iso_Sigma (P : UvPoly E B) : + P.functor ⋙₂ coyoneda (C := C) ≅ + Functor.Sigma + ((equivalence_Elements B).functor ⋙ (Over.pullback P.p).op ⋙ + (forget E).op ⋙ coyoneda (C := C)) := + calc + P.functor ⋙₂ coyoneda (C := C) ≅ + (star E ⋙ pushforward P.p) ⋙₂ (forget B ⋙₂ coyoneda (C := C)) := + Iso.refl _ + + _ ≅ (star E ⋙ pushforward P.p) ⋙₂ Functor.Sigma + ((equivalence_Elements B).functor ⋙ coyoneda (C := Over B)) := + iso₂WhiskerLeft _ (forget_iso_Sigma B) + + _ ≅ Functor.Sigma + ((equivalence_Elements B).functor ⋙ + star E ⋙₂ pushforward P.p ⋙₂ coyoneda (C := Over B)) := + -- Q: better make `comp₂_Sigma` an iso and avoid `eqToIso`? + eqToIso (by simp [comp₂_Sigma]) + + _ ≅ _ := + let i := + calc + star E ⋙₂ pushforward P.p ⋙₂ coyoneda (C := Over B) ≅ + star E ⋙₂ (Over.pullback P.p).op ⋙ coyoneda (C := Over E) := + iso₂WhiskerLeft (star E) (Adjunction.homIso <| adj P.p).symm + + _ ≅ (Over.pullback P.p).op ⋙ star E ⋙₂ coyoneda (C := Over E) := + Iso.refl _ + + _ ≅ (Over.pullback P.p).op ⋙ (forget E).op ⋙ coyoneda (C := C) := + isoWhiskerLeft (Over.pullback P.p).op (Adjunction.homIso <| forgetAdjStar E).symm; + + Functor.Sigma.isoCongrRight (isoWhiskerLeft _ i) + +-- Alternative definition of `equiv`. +def equiv' (P : UvPoly E B) (Γ X : C) : + (Γ ⟶ P.functor.obj X) ≃ (b : Γ ⟶ B) × (pullback b P.p ⟶ X) := + Iso.toEquiv <| (P.iso_Sigma.app (.op Γ)).app X + +theorem equiv'_app (P : UvPoly E B) (Γ X : C) (be : Γ ⟶ P.functor.obj X) : + P.equiv' Γ X be = (P.iso_Sigma.hom.app <| .op Γ).app X be := by + simp [equiv'] + +-- TODO(WN): Tactic script takes 10s, and kernel typechecking another 10s! +set_option maxHeartbeats 0 in +lemma equiv'_naturality_left {Δ Γ : C} (σ : Δ ⟶ Γ) (P : UvPoly E B) (X : C) (be : Γ ⟶ P.functor.obj X) : + P.equiv' Δ X (σ ≫ be) = let p := P.equiv' Γ X be + ⟨σ ≫ p.1, pullback.lift (pullback.fst .. ≫ σ) (pullback.snd ..) + (assoc (obj := C) .. ▸ pullback.condition) ≫ p.2⟩ := by + conv_lhs => rw [equiv'_app, comp₂_coyoneda_naturality_left, ← equiv'_app] + apply Sigma.ext <;> simp + +set_option maxHeartbeats 0 in +lemma equiv'_naturality_right {Γ X Y : C} (P : UvPoly E B) (be : Γ ⟶ P.functor.obj X) (f : X ⟶ Y) : - equiv P Γ Y (be ≫ P.functor.map f) = - let ⟨b, e⟩ := equiv P Γ X be - ⟨b, e ≫ f⟩ := by - dsimp - congr! 1 with h - . simp [polyPair] - . set g := (P.polyPair be).snd ≫ f - rw [(_ : (P.polyPair (be ≫ P.functor.map f)).snd = (pullback.congrHom h rfl).hom ≫ g)] - · generalize (P.polyPair (be ≫ P.functor.map f)).fst = x at h - cases h - simp - · dsimp only [polyPair, g] - rw [homMk_comp (w_f := by simp [fstProj, functor]) (w_g := by simp [functor])] - simp only [UvPoly.functor, Functor.comp_map, forget_map, homMk_eta, - homEquiv_naturality_right_symm, comp_left, assoc] - admit - --rw [show ((Over.pullback E).map f).left ≫ prod.snd = prod.snd ≫ f by simp] - -- simp only [← assoc] - -- congr 2 - -- simp only [comp_obj, forget_obj, star_obj_left, homEquiv_counit, id_obj, comp_left, - -- pullback_obj_left, mk_left, mk_hom, pullback_map_left, Over.homMk_left, - -- pullback.congrHom_hom, ← assoc] - -- congr 1 - -- ext <;> simp + equiv' P Γ Y (be ≫ P.functor.map f) = + let p := equiv' P Γ X be + ⟨p.1, p.2 ≫ f⟩ := by + conv_lhs => rw [equiv'_app, comp₂_coyoneda_naturality_right, ← equiv'_app] + have : (𝟙 Γ ≫ ((P.equiv' Γ X) be).fst) = (P.equiv' Γ X be).fst := by simp + apply Sigma.ext + . simp + . dsimp + rw! (castMode := .all) [this] + simp + +#exit /-- 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) := From 9511690c7476814698d98b47870ed50dd0673fb9 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Wed, 19 Mar 2025 16:12:52 -0400 Subject: [PATCH 12/18] chore: style --- Poly/DepFunctor/Sigma.lean | 3 ++- Poly/UvPoly.lean | 16 ++++++++-------- 2 files changed, 10 insertions(+), 9 deletions(-) diff --git a/Poly/DepFunctor/Sigma.lean b/Poly/DepFunctor/Sigma.lean index 39c554b..fefe1b3 100644 --- a/Poly/DepFunctor/Sigma.lean +++ b/Poly/DepFunctor/Sigma.lean @@ -249,7 +249,7 @@ def equivalence_Elements (A : 𝒞) : (yoneda.obj A).Elements ≌ (Over A)ᵒᵖ -- TODO: `simp` fails to unify `id_comp`/`comp_id` (fun f => by simp [Category.comp_id f, Category.id_comp f]) -/-- `𝒞(X, Over.forget f) ≅ Σ(g: X ⟶ A), 𝒞/A(g, f)` -/ +/-- 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 @@ -282,6 +282,7 @@ namespace CategoryTheory.Adjunction variable {𝒞 𝒟 : Type*} [Category 𝒞] [Category 𝒟] +/-- For `F ⊣ G`, `𝒟(FX, Y) ≅ 𝒞(X, GY)`. -/ def homIso {F : 𝒞 ⥤ 𝒟} {G : 𝒟 ⥤ 𝒞} (A : F ⊣ G) : F.op ⋙ coyoneda (C := 𝒟) ≅ G ⋙₂ coyoneda (C := 𝒞) := NatIso.ofComponents₂ (fun C D => Equiv.toIso <| A.homEquiv C.unop D) diff --git a/Poly/UvPoly.lean b/Poly/UvPoly.lean index d8373bc..5356fe3 100644 --- a/Poly/UvPoly.lean +++ b/Poly/UvPoly.lean @@ -379,16 +379,16 @@ def iso_Sigma (P : UvPoly E B) : _ ≅ _ := let i := - calc - star E ⋙₂ pushforward P.p ⋙₂ coyoneda (C := Over B) ≅ - star E ⋙₂ (Over.pullback P.p).op ⋙ coyoneda (C := Over E) := - iso₂WhiskerLeft (star E) (Adjunction.homIso <| adj P.p).symm + calc + star E ⋙₂ pushforward P.p ⋙₂ coyoneda (C := Over B) ≅ + star E ⋙₂ (Over.pullback P.p).op ⋙ coyoneda (C := Over E) := + iso₂WhiskerLeft (star E) (Adjunction.homIso <| adj P.p).symm - _ ≅ (Over.pullback P.p).op ⋙ star E ⋙₂ coyoneda (C := Over E) := - Iso.refl _ + _ ≅ (Over.pullback P.p).op ⋙ star E ⋙₂ coyoneda (C := Over E) := + Iso.refl _ - _ ≅ (Over.pullback P.p).op ⋙ (forget E).op ⋙ coyoneda (C := C) := - isoWhiskerLeft (Over.pullback P.p).op (Adjunction.homIso <| forgetAdjStar E).symm; + _ ≅ (Over.pullback P.p).op ⋙ (forget E).op ⋙ coyoneda (C := C) := + isoWhiskerLeft (Over.pullback P.p).op (Adjunction.homIso <| forgetAdjStar E).symm; Functor.Sigma.isoCongrRight (isoWhiskerLeft _ i) From 2b94ae01910f19cfe625c51fe956e1abe9941571 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Thu, 20 Mar 2025 19:48:53 -0400 Subject: [PATCH 13/18] chore: start cleaning up --- Poly/Bifunctor/Basic.lean | 96 +++++++++++++ Poly/{DepFunctor => Bifunctor}/Sigma.lean | 130 ++---------------- Poly/DepFunctor/PullbackUPs.lean | 124 ----------------- .../CategoryTheory/Comma/Over/Basic.lean | 32 ++++- Poly/ForMathlib/CategoryTheory/Elements.lean | 21 ++- Poly/ForMathlib/CategoryTheory/NatIso.lean | 9 +- Poly/ForMathlib/CategoryTheory/Types.lean | 9 +- Poly/Util.lean | 75 ---------- Poly/UvPoly.lean | 57 ++++---- 9 files changed, 184 insertions(+), 369 deletions(-) create mode 100644 Poly/Bifunctor/Basic.lean rename Poly/{DepFunctor => Bifunctor}/Sigma.lean (52%) delete mode 100644 Poly/DepFunctor/PullbackUPs.lean delete mode 100644 Poly/Util.lean diff --git a/Poly/Bifunctor/Basic.lean b/Poly/Bifunctor/Basic.lean new file mode 100644 index 0000000..fc573d8 --- /dev/null +++ b/Poly/Bifunctor/Basic.lean @@ -0,0 +1,96 @@ +/- +Copyright (c) 2025 Wojciech Nawrocki. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Wojciech Nawrocki +-/ +import Mathlib.CategoryTheory.Adjunction.Basic + +import Poly.ForMathlib.CategoryTheory.NatIso +import Poly.ForMathlib.CategoryTheory.Types + +/-! ## Composition of bifunctors -/ + +namespace CategoryTheory.Functor + +variable {𝒞 𝒟' 𝒟 ℰ : Type*} [Category 𝒞] [Category 𝒟'] [Category 𝒟] [Category ℰ] + +/-- Precompose a bifunctor in the second argument. +Note that `G ⋙₂ F ⋙ P = F ⋙ G ⋙₂ P` definitionally. -/ +@[simps] +def comp₂ (F : 𝒟' ⥤ 𝒟) (P : 𝒞 ⥤ 𝒟 ⥤ ℰ) : 𝒞 ⥤ 𝒟' ⥤ ℰ where + obj Γ := F ⋙ P.obj Γ + map f := whiskerLeft F (P.map f) + +@[inherit_doc] +scoped [CategoryTheory] infixr:80 " ⋙₂ " => Functor.comp₂ + +@[simp] +theorem comp_comp₂ {𝒟'' : Type*} [Category 𝒟''] + (F : 𝒟'' ⥤ 𝒟') (G : 𝒟' ⥤ 𝒟) (P : 𝒞 ⥤ 𝒟 ⥤ ℰ) : + (F ⋙ G) ⋙₂ P = F ⋙₂ (G ⋙₂ P) := by + rfl + +/-- Composition with `F,G` ordered like the arguments of `P` is considered `simp`ler. -/ +@[simp] +theorem comp₂_comp {𝒞' : Type*} [Category 𝒞'] + (F : 𝒞' ⥤ 𝒞) (G : 𝒟' ⥤ 𝒟) (P : 𝒞 ⥤ 𝒟 ⥤ ℰ) : + G ⋙₂ (F ⋙ P) = F ⋙ (G ⋙₂ P) := by + rfl + +@[simps!] +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 C f => by + have := congr_arg (P₂.obj C).map (i.hom.naturality f) + simp only [map_comp] at this + simp [this]) + +@[simps!] +def comp₂_isoWhiskerLeft {P₁ P₂ : 𝒞 ⥤ 𝒟 ⥤ ℰ} (F : 𝒟' ⥤ 𝒟) (i : P₁ ≅ P₂) : + F ⋙₂ P₁ ≅ F ⋙₂ P₂ := + comp₂_iso (Iso.refl F) i + +@[simps!] +def comp₂_isoWhiskerRight {F₁ F₂ : 𝒟' ⥤ 𝒟} (i : F₁ ≅ F₂) (P : 𝒞 ⥤ 𝒟 ⥤ ℰ) : + F₁ ⋙₂ P ≅ F₂ ⋙₂ P := + comp₂_iso i (Iso.refl P) + +end CategoryTheory.Functor + +/-! ## Natural isomorphisms of bifunctors -/ + +namespace CategoryTheory +universe v u +variable {𝒞 : Type u} [Category.{v} 𝒞] +variable {𝒟 : Type*} [Category 𝒟] + +namespace coyoneda + +theorem comp₂_naturality₂_left (F : 𝒟 ⥤ 𝒞) (P : 𝒞ᵒᵖ ⥤ 𝒟 ⥤ Type v) + (i : F ⋙₂ coyoneda (C := 𝒞) ⟶ P) (X Y : 𝒞) (Z : 𝒟) (f : X ⟶ Y) (g : Y ⟶ F.obj Z) : + -- TODO: 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] + +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] + +end coyoneda + +namespace Adjunction + +variable {𝒟 : Type*} [Category 𝒟] + +/-- For `F ⊣ G`, `𝒟(FX, Y) ≅ 𝒞(X, GY)`. -/ +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]) + +end Adjunction +end CategoryTheory diff --git a/Poly/DepFunctor/Sigma.lean b/Poly/Bifunctor/Sigma.lean similarity index 52% rename from Poly/DepFunctor/Sigma.lean rename to Poly/Bifunctor/Sigma.lean index fefe1b3..6740cb5 100644 --- a/Poly/DepFunctor/Sigma.lean +++ b/Poly/Bifunctor/Sigma.lean @@ -3,40 +3,16 @@ Copyright (c) 2025 Wojciech Nawrocki. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Wojciech Nawrocki -/ - -import Lean.Elab.Tactic.DiscrTreeKey - -import Mathlib.CategoryTheory.Elements +import Mathlib.CategoryTheory.Comma.Over.Basic import Mathlib.CategoryTheory.Functor.Currying -import Mathlib.CategoryTheory.Functor.Category -import Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback + import SEq.Tactic.DepRewrite import Poly.ForMathlib.CategoryTheory.Elements -import Poly.ForMathlib.CategoryTheory.NatIso -import Poly.ForMathlib.CategoryTheory.Types -import Poly.Util +import Poly.ForMathlib.CategoryTheory.Comma.Over.Basic +import Poly.Bifunctor.Basic -open private mkKey from Lean.Elab.Tactic.DiscrTreeKey in -open Lean Meta Elab Tactic in -/-- Print the `DiscrTree` key of the current `conv` mode target. -/ -macro "discr_tree_key" : conv => - `(conv| tactic => run_tac do - let g ← Conv.getLhs - logInfo <| ← DiscrTree.keysAsPattern <| ← mkKey g false) - -open private mkKey from Lean.Elab.Tactic.DiscrTreeKey in -open Lean Meta Elab Tactic Conv in -/-- Attempt to match the current `conv` mode target -against the LHS of the specified theorem. -/ -elab "discr_tree_match" n:ident : conv => do - let c ← realizeGlobalConstNoOverloadWithInfo n - let ci ← getConstInfo c - let e ← Conv.getLhs - let ciKey ← mkKey ci.type true - let gKey ← mkKey e false - logInfo m!"{ciKey.zip gKey |>.map fun (a, b) => m!"{a} := {b}"}" - logInfo m!"{← DiscrTree.keysAsPattern ciKey} := {← DiscrTree.keysAsPattern gKey}" +/-! ## Dependent sums of functors -/ namespace CategoryTheory.Functor @@ -123,41 +99,11 @@ def Sigma.isoCongrRight {F : 𝒞 ⥤ Type w} {G₁ G₂ : F.Elements ⥤ 𝒟 apply have h := ?_; Sigma.ext h ?_ . simp . dsimp [Sigma] at h ⊢ - simp [FunctorToTypes.binaturality_left, FunctorToTypes.binaturality_right] + simp [FunctorToTypes.naturality₂_left, FunctorToTypes.naturality₂_right] } -end CategoryTheory.Functor - -/-! ### Profunctor operations -/ - -namespace CategoryTheory.Functor - -variable {𝒞 𝒟' 𝒟 ℰ : Type*} [Category 𝒞] [Category 𝒟'] [Category 𝒟] [Category ℰ] - -/-- Precompose a profunctor in the second argument. -Note that `G ⋙₂ F ⋙ P = F ⋙ G ⋙₂ P` definitionally. -/ -@[simps] -def comp₂ (F : 𝒟' ⥤ 𝒟) (P : 𝒞 ⥤ 𝒟 ⥤ ℰ) : 𝒞 ⥤ 𝒟' ⥤ ℰ where - obj Γ := F ⋙ P.obj Γ - map f := whiskerLeft F (P.map f) - -@[inherit_doc] -scoped [CategoryTheory] infixr:80 " ⋙₂ " => Functor.comp₂ - -@[simp] -theorem comp_comp₂ {𝒟'' : Type*} [Category 𝒟''] - (F : 𝒟'' ⥤ 𝒟') (G : 𝒟' ⥤ 𝒟) (P : 𝒞 ⥤ 𝒟 ⥤ ℰ) : - (F ⋙ G) ⋙₂ P = F ⋙₂ (G ⋙₂ P) := by - rfl - -@[simp] --- Composition with `F,G` ordered like the arguments of `P` is considered 'simplified'. -theorem comp₂_comp {𝒞' : Type*} [Category 𝒞'] - (F : 𝒞' ⥤ 𝒞) (G : 𝒟' ⥤ 𝒟) (P : 𝒞 ⥤ 𝒟 ⥤ ℰ) : - G ⋙₂ (F ⋙ P) = F ⋙ (G ⋙₂ P) := by - rfl - -theorem comp₂_Sigma {F : 𝒞 ⥤ Type w} (G : 𝒟' ⥤ 𝒟) (P : F.Elements ⥤ 𝒟 ⥤ Type v) : +theorem comp₂_Sigma {𝒟' : Type*} [Category 𝒟'] + {F : 𝒞 ⥤ Type w} (G : 𝒟' ⥤ 𝒟) (P : F.Elements ⥤ 𝒟 ⥤ Type v) : G ⋙₂ Sigma P = Sigma (G ⋙₂ P) := by apply Functor.hext . intro C @@ -172,51 +118,9 @@ theorem comp₂_Sigma {F : 𝒞 ⥤ Type w} (G : 𝒟' ⥤ 𝒟) (P : F.Elements ext : 3 apply Sigma.ext <;> simp -@[simps!] -def 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 C f => by - have := congr_arg (P₂.obj C).map (i.hom.naturality f) - simp only [map_comp] at this - simp [this]) - -@[simps!] -def iso₂WhiskerLeft {P₁ P₂ : 𝒞 ⥤ 𝒟 ⥤ ℰ} (F : 𝒟' ⥤ 𝒟) (i : P₁ ≅ P₂) : F ⋙₂ P₁ ≅ F ⋙₂ P₂ := - iso₂ (Iso.refl F) i - -@[simps!] -def iso₂WhiskerRight {F₁ F₂ : 𝒟' ⥤ 𝒟} (i : F₁ ≅ F₂) (P : 𝒞 ⥤ 𝒟 ⥤ ℰ) : F₁ ⋙₂ P ≅ F₂ ⋙₂ P := - iso₂ i (Iso.refl P) - -end CategoryTheory.Functor - -/-! ### Natural isomorphisms-/ - -/-! #### Hom-types -/ - -namespace CategoryTheory.Functor - -universe v u -variable {𝒞 : Type u} [Category.{v} 𝒞] - -theorem comp₂_coyoneda_naturality_left {𝒞' : Type*} [Category 𝒞'] - (F : 𝒞' ⥤ 𝒞) (P : 𝒞ᵒᵖ ⥤ 𝒞' ⥤ Type v) (i : F ⋙₂ coyoneda (C := 𝒞) ⟶ P) (X Y : 𝒞) (Z : 𝒞') - (f : X ⟶ Y) (g : Y ⟶ F.obj Z) : - -- TODO: 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.binaturality_left] - -theorem comp₂_coyoneda_naturality_right {𝒞' : Type*} [Category 𝒞'] - (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.binaturality_right] - end CategoryTheory.Functor -/-! #### Over -/ +/-! ## Over categories -/ namespace CategoryTheory.Over @@ -269,24 +173,10 @@ def forget_iso_Sigma (A : 𝒞) : . simp . dsimp at h ⊢ rw! [h] - -- simp -- TODO: `homMk f.left ⋯` and `homMk (𝟙 _) ⋯` don't get simplified here apply heq_of_eq ext : 1 simp end CategoryTheory.Over -/-! #### Adjunction -/ - -namespace CategoryTheory.Adjunction - -variable {𝒞 𝒟 : Type*} [Category 𝒞] [Category 𝒟] - -/-- For `F ⊣ G`, `𝒟(FX, Y) ≅ 𝒞(X, GY)`. -/ -def homIso {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]) - -end CategoryTheory.Adjunction +#min_imports diff --git a/Poly/DepFunctor/PullbackUPs.lean b/Poly/DepFunctor/PullbackUPs.lean deleted file mode 100644 index fe1fd4b..0000000 --- a/Poly/DepFunctor/PullbackUPs.lean +++ /dev/null @@ -1,124 +0,0 @@ -import Poly.DepFunctor.Sigma - -/-! ### Three ways to state the UP of pullbacks -/ - -open CategoryTheory Functor Limits - -universe v u -variable {𝒞 : Type u} [Category.{v} 𝒞] -variable {X Y Z : 𝒞} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g] - -/-! #### 1. Current approach -/ - -noncomputable def pullbackHomEquiv (W : 𝒞) : - (W ⟶ pullback f g) ≃ (i : W ⟶ X) × (j : W ⟶ Y) ×' i ≫ f = j ≫ g where - toFun h := ⟨h ≫ pullback.fst f g, h ≫ pullback.snd f g, by simp[pullback.condition]⟩ - invFun x := pullback.lift x.1 x.2.1 x.2.2 - left_inv _ := pullback.hom_ext (by simp) (by simp) - right_inv := by rintro ⟨_,_,_⟩; congr!; simp; simp - --- Issue: this kind of naturality statement does not easily compose --- when equivalences are chained, e.g. using `Equiv.sigmaCongrLeft`. -theorem naturality_left {W W' : 𝒞} (h : W ⟶ W') (k : W' ⟶ pullback f g) : - let p := pullbackHomEquiv f g W' k - pullbackHomEquiv f g W (h ≫ k) = ⟨h ≫ p.1, h ≫ p.2.1, by simp [p.2.2]⟩ := by - dsimp [pullbackHomEquiv] - congr! 1 with h - . simp - . rw! [h]; simp - -/-! #### 2. Natural iso. of cone functors -/ - -/-- Sends `W` to the type of cones on the cospan `👉f👉👈g👈` with apex `W`, -i.e., tuples `(i : W ⟶ X) × (j : W ⟶ Y) ×' (i ≫ f = j ≫ g)`. -/ -def pullbackCones : 𝒞ᵒᵖ ⥤ Type v := - (cospan f g).cones - -omit [HasPullback f g] in -@[simp] -theorem PullbackCone.eta' (c : PullbackCone f g) : PullbackCone.mk c.fst c.snd c.condition = c := by - dsimp [PullbackCone.mk] - congr 2 - ext i : 1 - rcases i with _ | ⟨_ | _⟩ <;> simp - -omit [HasPullback f g] in -theorem PullbackCone.mk_comp_π {W' : 𝒞} (h : W' ⟶ W) (i : W ⟶ X) (j : W ⟶ Y) - (eq : (h ≫ i) ≫ f = (h ≫ j) ≫ g) eq' : - (PullbackCone.mk (h ≫ i) (h ≫ j) eq).π = (const _).map h ≫ (PullbackCone.mk i j eq').π := by - ext i : 2 - dsimp - rcases i with _ | ⟨_ | _⟩ <;> simp - -/-- We can also define `pullbackCones` using `PullbackCone`, but storing the apex -- bumps up the universe level; and -- forces the use of `eqToHom`. -/ -def pullbackCones' : 𝒞ᵒᵖ ⥤ Type (max v u) where - obj W := { c : PullbackCone f g // W.unop = c.pt } - map f := fun ⟨c, eq⟩ => ⟨ - PullbackCone.mk - (f.unop ≫ eqToHom eq ≫ c.fst) - (f.unop ≫ eqToHom eq ≫ c.snd) - (by rw! (castMode := .all) [eq]; simp [c.condition]), - rfl⟩ - map_id _ := by dsimp; ext ⟨_, eq⟩ : 2; rw! [eq]; simp - map_comp _ _ := by ext : 1; simp - --- This composes more directly than `naturality_left` above. -noncomputable def pullbackConesIso : yoneda.obj (pullback f g) ≅ pullbackCones f g := - NatIso.ofComponents - (fun W => Equiv.toIso { - toFun h := - (PullbackCone.mk - (h ≫ pullback.fst f g) (h ≫ pullback.snd f g) (by simp [pullback.condition])).π - invFun c := - let c' : PullbackCone f g := ⟨W.unop, c⟩ - pullback.lift c'.fst c'.snd c'.condition - left_inv _ := by - dsimp - ext : 1 <;> simp [PullbackCone.fst, PullbackCone.snd] - right_inv π := by - -- Nasty proof because there is good API for `PullbackCone`, - -- but not for `pullbackCones`. - dsimp [PullbackCone.mk] - congr 1 with i - have := π.naturality (WidePullbackShape.Hom.term .left) - dsimp at this - rcases i with _ | ⟨_ | _⟩ <;> simp [PullbackCone.fst, ← this] - }) - (fun _ => by - ext : 1 - dsimp - rw [PullbackCone.mk_comp_π (eq' := by simp [pullback.condition]), - PullbackCone.mk_comp_π (eq' := by simp [pullback.condition])] - simp [pullbackCones, Functor.cones]) - -/-! #### 3. Equivalence with category of cones - -I didn't finish constructing this approach as it seems very awkward. -/ - -@[simps] -def PullbackCone.mkHom {W : 𝒞} (i₁ : W' ⟶ X) (j₁ : W' ⟶ Y) (i₂ : W ⟶ X) (j₂ : W ⟶ Y) - (eq₁ : i₁ ≫ f = j₁ ≫ g) (eq₂ : i₂ ≫ f = j₂ ≫ g) - (h : W' ⟶ W) (w_i : h ≫ i₂ = i₁) (w_j : h ≫ j₂ = j₁) : - PullbackCone.mk i₁ j₁ eq₁ ⟶ PullbackCone.mk i₂ j₂ eq₂ where - hom := h - w := by rintro (_ | ⟨_ | _⟩) <;> simp [reassoc_of% w_i, w_i, w_j] - -noncomputable def pullbackIso : Over (pullback f g) ≌ PullbackCone f g where - functor := { - obj U := PullbackCone.mk (U.hom ≫ pullback.fst f g) (U.hom ≫ pullback.snd f g) - (by simp [pullback.condition]) - map t := PullbackCone.mkHom f g (h := t.left) (w_i := by simp [t.w]) (w_j := by simp [t.w]) .. - map_id := by intros; ext : 1; simp - map_comp := by intros; ext : 1; simp - } - inverse := { - obj c := Over.mk (pullback.lift c.fst c.snd c.condition) - map t := Over.homMk t.hom (by dsimp; ext <;> simp) - map_id := by intros; ext : 1; simp - map_comp := by intros; ext : 1; simp - } - unitIso := NatIso.ofComponents (fun X => eqToIso sorry) sorry - counitIso := NatIso.ofComponents (fun X => eqToIso sorry) sorry - functor_unitIso_comp := sorry diff --git a/Poly/ForMathlib/CategoryTheory/Comma/Over/Basic.lean b/Poly/ForMathlib/CategoryTheory/Comma/Over/Basic.lean index f2b046c..4a8ab7b 100644 --- a/Poly/ForMathlib/CategoryTheory/Comma/Over/Basic.lean +++ b/Poly/ForMathlib/CategoryTheory/Comma/Over/Basic.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2025 Sina Hazratpour. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Sina Hazratpour +Authors: Sina Hazratpour, Wojciech Nawrocki -/ import Mathlib.CategoryTheory.Comma.Over.Basic import Mathlib.CategoryTheory.Comma.StructuredArrow.Basic @@ -9,16 +9,36 @@ import Mathlib.CategoryTheory.Category.Cat namespace CategoryTheory +-- morphism levels before object levels. See note [CategoryTheory universes]. universe v₁ v₂ v₃ u₁ u₂ u₃ --- morphism levels before object levels. See note [CategoryTheory universes]. variable {T : Type u₁} [Category.{v₁} T] namespace Over -/-- `Over.Sigma Y U` a shorthand for `(Over.map Y.hom).obj U`. This is the categoy-theoretic -analogue of `Sigma` for types. --/ +@[simp] +theorem mk_eta {X : T} (U : Over X) : mk U.hom = U := by + rfl + +/-- A variant of `homMk_comp` that can trigger in `simp`. -/ +@[simp] +lemma homMk_comp' {X Y Z W : T} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) (fgh_comp) : + homMk (U := mk (f ≫ g ≫ h)) (f ≫ g) fgh_comp = + homMk f ≫ homMk (U := mk (g ≫ h)) (V := mk h) g := + rfl + +@[simp] +lemma homMk_comp'_assoc {X Y Z W : T} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) (fgh_comp) : + homMk (U := mk ((f ≫ g) ≫ h)) (f ≫ g) fgh_comp = + homMk f ≫ homMk (U := mk (g ≫ h)) (V := mk h) g := by + rfl + +@[simp] +lemma homMk_id {X B : T} (f : X ⟶ B) (h : 𝟙 X ≫ f = f) : homMk (𝟙 X) h = 𝟙 (mk f) := + rfl + +/-- `Over.Sigma Y U` is a shorthand for `(Over.map Y.hom).obj U`. +This is a category-theoretic analogue of `Sigma` for types. -/ abbrev Sigma {X : T} (Y : Over X) (U : Over (Y.left)) : Over X := (map Y.hom).obj U @@ -32,6 +52,7 @@ lemma hom {Y : Over X} (Z : Over (Y.left)) : (Sigma Y Z).hom = Z.hom ≫ Y.hom : def map {Y : Over X} {Z Z' : Over (Y.left)} (g : Z ⟶ Z') : (Sigma Y Z) ⟶ (Sigma Y Z') := (Over.map Y.hom).map g +@[simp] lemma map_left {Y : Over X} {Z Z' : Over (Y.left)} {g : Z ⟶ Z'} : ((Over.map Y.hom).map g).left = g.left := Over.map_map_left @@ -43,6 +64,7 @@ lemma map_homMk_left {Y : Over X} {Z Z' : Over (Y.left)} {g : Z ⟶ Z'} : @[simps!] def fst {Y : Over X} (Z : Over (Y.left)) : (Sigma Y Z) ⟶ Y := Over.homMk Z.hom +@[simp] lemma map_comp_fst {Y : Over X} {Z Z' : Over (Y.left)} (g : Z ⟶ Z') : (Over.map Y.hom).map g ≫ fst Z' = fst Z := by ext diff --git a/Poly/ForMathlib/CategoryTheory/Elements.lean b/Poly/ForMathlib/CategoryTheory/Elements.lean index e499531..ab84dd6 100644 --- a/Poly/ForMathlib/CategoryTheory/Elements.lean +++ b/Poly/ForMathlib/CategoryTheory/Elements.lean @@ -1,19 +1,16 @@ +/- +Copyright (c) 2025 Wojciech Nawrocki. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Wojciech Nawrocki +-/ import Mathlib.CategoryTheory.Elements -namespace CategoryTheory +namespace CategoryTheory.CategoryOfElements variable {𝒞 𝒟 : Type*} [Category 𝒞] [Category 𝒟] - -namespace CategoryOfElements - variable (F : 𝒞 ⥤ Type*) (G : F.Elements ⥤ 𝒟) --- TODO: These are the same definition; but neither works with dot notation on `Hom` :( -#check NatTrans.mapElements -#check CategoryOfElements.map - --- Cannot add `simps` for defs in imported modules --- attribute [simps map] NatTrans.mapElements +-- 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) : @@ -34,6 +31,4 @@ theorem map_homMk_comp {X Y Z : 𝒞} (f : X ⟶ Y) (g : Y ⟶ Z) (a : F.obj X) show G.map (f ≫ g) = G.map f ≫ G.map g simp -end CategoryOfElements - -end CategoryTheory +end CategoryTheory.CategoryOfElements diff --git a/Poly/ForMathlib/CategoryTheory/NatIso.lean b/Poly/ForMathlib/CategoryTheory/NatIso.lean index 373c37a..27b100f 100644 --- a/Poly/ForMathlib/CategoryTheory/NatIso.lean +++ b/Poly/ForMathlib/CategoryTheory/NatIso.lean @@ -13,14 +13,13 @@ variable {𝒞 𝒟 ℰ : Type*} [Category 𝒞] [Category 𝒟] [Category ℰ] /-- Natural isomorphism of bifunctors from naturality in both arguments. -/ def ofComponents₂ {F G : 𝒞 ⥤ 𝒟 ⥤ ℰ} (app : ∀ Γ X, (F.obj Γ).obj X ≅ (G.obj Γ).obj X) - -- binaturality_left? - (naturality_left : ∀ {Γ Δ : 𝒞} (X : 𝒟) (σ : Γ ⟶ Δ), + (naturality₂_left : ∀ {Γ Δ : 𝒞} (X : 𝒟) (σ : Γ ⟶ Δ), (F.map σ).app X ≫ (app Δ X).hom = (app Γ X).hom ≫ (G.map σ).app X := by aesop_cat) - (naturality_right : ∀ {X Y : 𝒟} (Γ : 𝒞) (f : X ⟶ Y), + (naturality₂_right : ∀ {X Y : 𝒟} (Γ : 𝒞) (f : X ⟶ Y), (F.obj Γ).map f ≫ (app Γ Y).hom = (app Γ X).hom ≫ (G.obj Γ).map f := by aesop_cat) : F ≅ G := NatIso.ofComponents - (fun Γ => NatIso.ofComponents (app Γ) (fun f => by simpa using naturality_right Γ f)) - (fun σ => by ext X : 2; simpa using naturality_left X σ) + (fun Γ => NatIso.ofComponents (app Γ) (fun f => by simpa using naturality₂_right Γ f)) + (fun σ => by ext X : 2; simpa using naturality₂_left X σ) end CategoryTheory.NatIso diff --git a/Poly/ForMathlib/CategoryTheory/Types.lean b/Poly/ForMathlib/CategoryTheory/Types.lean index 5319d53..b221290 100644 --- a/Poly/ForMathlib/CategoryTheory/Types.lean +++ b/Poly/ForMathlib/CategoryTheory/Types.lean @@ -8,8 +8,9 @@ import Mathlib.CategoryTheory.Types namespace CategoryTheory.FunctorToTypes -/-! Gross lemmas about bifunctors into `Type`. -Is there a better way? +/-! Repetitive lemmas about bifunctors into `Type`. + +Q: Is there a better way? Mathlib doesn't seem to think so: see `hom_inv_id_app`, `hom_inv_id_app_app`, `hom_inv_id_app_app_app`. Can a `simproc` that tries `congr_fun/congr_arg simpLemma` work? -/ @@ -18,11 +19,11 @@ universe w variable {𝒞 𝒟 : Type*} [Category 𝒞] [Category 𝒟] (F G : 𝒞 ⥤ 𝒟 ⥤ Type w) {C₁ C₂ : 𝒞} {D₁ D₂ : 𝒟} -theorem binaturality_left (σ : F ⟶ G) (f : C₁ ⟶ C₂) (x : (F.obj C₁).obj D₁) : +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 -theorem binaturality_right (σ : F ⟶ G) (f : D₁ ⟶ D₂) (x : (F.obj C₁).obj D₁) : +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 .. diff --git a/Poly/Util.lean b/Poly/Util.lean deleted file mode 100644 index 6a8b0c0..0000000 --- a/Poly/Util.lean +++ /dev/null @@ -1,75 +0,0 @@ -import Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback -import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq -import Mathlib.CategoryTheory.Comma.Over.Basic - -/-! Miscellaneous results that don't fit anywhere else. -/ - -namespace CategoryTheory - -variable {𝒞 𝒟 : Type*} [Category 𝒞] [Category 𝒟] - -/-! ## `eqToHom` -/ - -/-- Note: if possible, -it's best to immediately rewrite `eqToHom` to an isomorphism -whose data is not defined by destructing an equality -in the second premise of this lemma. -/ --- If only there was a LiftIsos typeclass to do this for us! -lemma Sigma_hom_ext {X Y : 𝒞} {Z : 𝒟} (P : (X ⟶ Y) → 𝒟) - (p q : (f : X ⟶ Y) × (P f ⟶ Z)) - (fst_eq : p.fst = q.fst) - (snd_eq : (h : p.fst = q.fst) → p.snd = eqToHom (h ▸ rfl) ≫ q.snd) : - p = q := by - let ⟨b, e⟩ := p - let ⟨c, f⟩ := q - cases fst_eq - simp at snd_eq - simp [snd_eq] - -lemma Limits.pullback.eqToHom_eq_map {X Y Z : 𝒞} - (f₁ f₂ : X ⟶ Z) (g₁ g₂ : Y ⟶ Z) [HasPullback f₁ g₁] [HasPullback f₂ g₂] - (f_eq : f₁ = f₂) (g_eq : g₁ = g₂) : - eqToHom (by cases f_eq; cases g_eq; rfl) = - pullback.map f₁ g₁ f₂ g₂ (𝟙 X) (𝟙 Y) (𝟙 Z) (by simp [f_eq]) (by simp [g_eq]) := by - cases f_eq; cases g_eq; simp - -lemma IsPullback.eqToHom_eq_lift {P' P X Y Z : 𝒞} - {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z} - (pb : IsPullback fst snd f g) (eq : P' = P) : - eqToHom eq = - pb.lift (eqToHom eq ≫ fst) (eqToHom eq ≫ snd) (by simp [pb.w]) := by - cases eq; apply pb.hom_ext <;> simp - -lemma Over.eqToHom_eq_homMk {E B : 𝒞} (f g : E ⟶ B) (eq : f = g) : - eqToHom (show (Over.mk f) = (Over.mk g) from eq ▸ rfl) = - Over.homMk (𝟙 E) (by simp [eq]) := by - cases eq; rfl - -/-! ## Over categories -/ - -namespace Over - -/-- A variant of `homMk_comp` that can trigger in `simp`. -/ -@[simp] -lemma homMk_comp' {X Y Z W : 𝒞} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) (fgh_comp) : - homMk (U := mk (f ≫ g ≫ h)) (f ≫ g) fgh_comp = - homMk f ≫ homMk (U := mk (g ≫ h)) (V := mk h) g := - rfl - -@[simp] -lemma homMk_comp'_assoc {X Y Z W : 𝒞} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W) (fgh_comp) : - homMk (U := mk ((f ≫ g) ≫ h)) (f ≫ g) fgh_comp = - homMk f ≫ homMk (U := mk (g ≫ h)) (V := mk h) g := - rfl - -@[simp] -lemma homMk_id {B : 𝒞} (U : Over B) (h) : homMk (𝟙 U.left) h = 𝟙 U := - rfl - -/-- A variant of `homMk_id` that `simp` can use when `X ≢ U.left` syntactically. -/ -@[simp] -lemma homMk_id' {B : 𝒞} (f : X ⟶ B) (h) : homMk (𝟙 X) h = 𝟙 (mk f) := - rfl - -end Over -end CategoryTheory diff --git a/Poly/UvPoly.lean b/Poly/UvPoly.lean index 5356fe3..6a6a511 100644 --- a/Poly/UvPoly.lean +++ b/Poly/UvPoly.lean @@ -1,13 +1,13 @@ /- Copyright (c) 2024 Sina Hazratpour. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Sina Hazratpour +Authors: Sina Hazratpour, Wojciech Nawrocki -/ import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.BeckChevalley -- LCCC.BeckChevalley import Mathlib.CategoryTheory.Functor.TwoSquare import Poly.ForMathlib.CategoryTheory.PartialProduct -import Poly.DepFunctor.Sigma +import Poly.Bifunctor.Sigma /-! @@ -356,12 +356,28 @@ def equiv (P : UvPoly E B) (Γ : C) (X : C) : variable {Γ X : C} (P : UvPoly E B) +/-- Sends `(Γ, X)` to `Σ(b : Γ ⟶ B), 𝒞(pullback b P.p, X)`. -/ +@[simps! obj_obj map_app] +def fansOver : Cᵒᵖ ⥤ C ⥤ Type v := + Functor.Sigma + ((equivalence_Elements B).functor ⋙ (Over.pullback P.p).op ⋙ + (forget E).op ⋙ coyoneda (C := C)) + +omit [HasTerminal C] in +@[simp] +theorem fansOver_obj_map {X Y : C} (Γ : Cᵒᵖ) (f : X ⟶ Y) (x : P.fansOver.obj Γ |>.obj X) : + (P.fansOver.obj Γ).map f x = ⟨x.1, x.2 ≫ f⟩ := by + dsimp [fansOver] + have : 𝟙 Γ.unop ≫ x.1 = x.1 := by simp + ext : 1 + . simp + . dsimp + rw! (castMode := .all) [this] + simp + /-- `𝒞(Γ, PₚX) ≅ Σ(b : Γ ⟶ B), 𝒞(b*p, X)` -/ def iso_Sigma (P : UvPoly E B) : - P.functor ⋙₂ coyoneda (C := C) ≅ - Functor.Sigma - ((equivalence_Elements B).functor ⋙ (Over.pullback P.p).op ⋙ - (forget E).op ⋙ coyoneda (C := C)) := + P.functor ⋙₂ coyoneda (C := C) ≅ P.fansOver := calc P.functor ⋙₂ coyoneda (C := C) ≅ (star E ⋙ pushforward P.p) ⋙₂ (forget B ⋙₂ coyoneda (C := C)) := @@ -369,7 +385,7 @@ def iso_Sigma (P : UvPoly E B) : _ ≅ (star E ⋙ pushforward P.p) ⋙₂ Functor.Sigma ((equivalence_Elements B).functor ⋙ coyoneda (C := Over B)) := - iso₂WhiskerLeft _ (forget_iso_Sigma B) + comp₂_isoWhiskerLeft _ (forget_iso_Sigma B) _ ≅ Functor.Sigma ((equivalence_Elements B).functor ⋙ @@ -382,16 +398,17 @@ def iso_Sigma (P : UvPoly E B) : calc star E ⋙₂ pushforward P.p ⋙₂ coyoneda (C := Over B) ≅ star E ⋙₂ (Over.pullback P.p).op ⋙ coyoneda (C := Over E) := - iso₂WhiskerLeft (star E) (Adjunction.homIso <| adj P.p).symm + comp₂_isoWhiskerLeft (star E) (Adjunction.coyoneda_iso <| adj P.p).symm _ ≅ (Over.pullback P.p).op ⋙ star E ⋙₂ coyoneda (C := Over E) := Iso.refl _ _ ≅ (Over.pullback P.p).op ⋙ (forget E).op ⋙ coyoneda (C := C) := - isoWhiskerLeft (Over.pullback P.p).op (Adjunction.homIso <| forgetAdjStar E).symm; + isoWhiskerLeft (Over.pullback P.p).op (Adjunction.coyoneda_iso <| forgetAdjStar E).symm; Functor.Sigma.isoCongrRight (isoWhiskerLeft _ i) +-- TODO: make modules `UvPoly.UPIso` and `UvPoly.UPFan` -- Alternative definition of `equiv`. def equiv' (P : UvPoly E B) (Γ X : C) : (Γ ⟶ P.functor.obj X) ≃ (b : Γ ⟶ B) × (pullback b P.p ⟶ X) := @@ -401,28 +418,22 @@ theorem equiv'_app (P : UvPoly E B) (Γ X : C) (be : Γ ⟶ P.functor.obj X) : P.equiv' Γ X be = (P.iso_Sigma.hom.app <| .op Γ).app X be := by simp [equiv'] --- TODO(WN): Tactic script takes 10s, and kernel typechecking another 10s! -set_option maxHeartbeats 0 in +-- TODO(WN): Checking the theorem statement takes 5s, and kernel typechecking 10s! lemma equiv'_naturality_left {Δ Γ : C} (σ : Δ ⟶ Γ) (P : UvPoly E B) (X : C) (be : Γ ⟶ P.functor.obj X) : P.equiv' Δ X (σ ≫ be) = let p := P.equiv' Γ X be - ⟨σ ≫ p.1, pullback.lift (pullback.fst .. ≫ σ) (pullback.snd ..) - (assoc (obj := C) .. ▸ pullback.condition) ≫ p.2⟩ := by - conv_lhs => rw [equiv'_app, comp₂_coyoneda_naturality_left, ← equiv'_app] - apply Sigma.ext <;> simp + ⟨σ ≫ p.1, pullback.lift (pullback.fst .. ≫ σ) (pullback.snd ..) + (assoc (obj := C) .. ▸ pullback.condition) ≫ p.2⟩ := by + conv_lhs => rw [equiv'_app, coyoneda.comp₂_naturality₂_left, ← equiv'_app] + simp -set_option maxHeartbeats 0 in +-- TODO(WN): Kernel typechecking takes 10s! lemma equiv'_naturality_right {Γ X Y : C} (P : UvPoly E B) (be : Γ ⟶ P.functor.obj X) (f : X ⟶ Y) : equiv' P Γ Y (be ≫ P.functor.map f) = let p := equiv' P Γ X be ⟨p.1, p.2 ≫ f⟩ := by - conv_lhs => rw [equiv'_app, comp₂_coyoneda_naturality_right, ← equiv'_app] - have : (𝟙 Γ ≫ ((P.equiv' Γ X) be).fst) = (P.equiv' Γ X be).fst := by simp - apply Sigma.ext - . simp - . dsimp - rw! (castMode := .all) [this] - simp + conv_lhs => rw [equiv'_app, coyoneda.comp₂_naturality₂_right, ← equiv'_app] + simp #exit From 5236a45e1a04a24de151b2ee64f11111aa46e5fd Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Thu, 20 Mar 2025 20:55:17 -0400 Subject: [PATCH 14/18] chore: deprecate ForMathlib --- Poly/deprecated/Basic.lean | 2 +- Poly/{ => deprecated}/ForMathlib.lean | 0 2 files changed, 1 insertion(+), 1 deletion(-) rename Poly/{ => deprecated}/ForMathlib.lean (100%) diff --git a/Poly/deprecated/Basic.lean b/Poly/deprecated/Basic.lean index 2494521..bc69ad1 100644 --- a/Poly/deprecated/Basic.lean +++ b/Poly/deprecated/Basic.lean @@ -7,7 +7,7 @@ Authors: Emily Riehl, Sina Hazratpour, Wojciech Nawrocki import Mathlib.CategoryTheory.Adjunction.Over import Mathlib.CategoryTheory.Limits.Constructions.Over.Basic import Mathlib.CategoryTheory.ChosenFiniteProducts -import Poly.ForMathlib +import Poly.deprecated.ForMathlib /-! # Some basic equalities and isomorphisms of composition and base change functors diff --git a/Poly/ForMathlib.lean b/Poly/deprecated/ForMathlib.lean similarity index 100% rename from Poly/ForMathlib.lean rename to Poly/deprecated/ForMathlib.lean From d1b328844459afcc99e92023c25f9678e9c8af58 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Thu, 20 Mar 2025 21:29:39 -0400 Subject: [PATCH 15/18] chore: split out UP proofs --- Poly.lean | 5 +- Poly/{UvPoly.lean => UvPoly/Basic.lean} | 116 +----------------------- Poly/UvPoly/UPFan.lean | 35 +++++++ Poly/UvPoly/UPIso.lean | 95 +++++++++++++++++++ 4 files changed, 134 insertions(+), 117 deletions(-) rename Poly/{UvPoly.lean => UvPoly/Basic.lean} (74%) create mode 100644 Poly/UvPoly/UPFan.lean create mode 100644 Poly/UvPoly/UPIso.lean diff --git a/Poly.lean b/Poly.lean index b286754..f04a2ef 100644 --- a/Poly.lean +++ b/Poly.lean @@ -5,6 +5,7 @@ import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.Presheaf -- import Poly.LCCC.BeckChevalley -- import Poly.LCCC.Presheaf -- import Poly.Type.Univariate --- import Poly.Basic -- import Poly.Exponentiable -import Poly.UvPoly +import Poly.UvPoly.Basic +import Poly.UvPoly.UPFan +import Poly.UvPoly.UPIso diff --git a/Poly/UvPoly.lean b/Poly/UvPoly/Basic.lean similarity index 74% rename from Poly/UvPoly.lean rename to Poly/UvPoly/Basic.lean index 6a6a511..6ca2f50 100644 --- a/Poly/UvPoly.lean +++ b/Poly/UvPoly/Basic.lean @@ -7,7 +7,6 @@ Authors: Sina Hazratpour, Wojciech Nawrocki import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.BeckChevalley -- LCCC.BeckChevalley import Mathlib.CategoryTheory.Functor.TwoSquare import Poly.ForMathlib.CategoryTheory.PartialProduct -import Poly.Bifunctor.Sigma /-! @@ -335,119 +334,13 @@ theorem proj_snd {Γ X : C} {P : UvPoly E B} {f : Γ ⟶ P @ X} : (pullback.map _ _ _ _ f (𝟙 E) (𝟙 B) (by aesop) (by aesop)) ≫ ε P X ≫ prod.snd := by simp [proj] -/-- Universal property of the polynomial functor. -/ -@[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 [partialProd.lift] - rfl - · sorry - right_inv := by - intro ⟨b, e⟩ - ext - · simp only [proj_fst, lift_fst] - · sorry - -variable {Γ X : C} (P : UvPoly E B) - -/-- Sends `(Γ, X)` to `Σ(b : Γ ⟶ B), 𝒞(pullback b P.p, X)`. -/ -@[simps! obj_obj map_app] -def fansOver : Cᵒᵖ ⥤ C ⥤ Type v := - Functor.Sigma - ((equivalence_Elements B).functor ⋙ (Over.pullback P.p).op ⋙ - (forget E).op ⋙ coyoneda (C := C)) - -omit [HasTerminal C] in -@[simp] -theorem fansOver_obj_map {X Y : C} (Γ : Cᵒᵖ) (f : X ⟶ Y) (x : P.fansOver.obj Γ |>.obj X) : - (P.fansOver.obj Γ).map f x = ⟨x.1, x.2 ≫ f⟩ := by - dsimp [fansOver] - have : 𝟙 Γ.unop ≫ x.1 = x.1 := by simp - ext : 1 - . simp - . dsimp - rw! (castMode := .all) [this] - simp - -/-- `𝒞(Γ, PₚX) ≅ Σ(b : Γ ⟶ B), 𝒞(b*p, X)` -/ -def iso_Sigma (P : UvPoly E B) : - P.functor ⋙₂ coyoneda (C := C) ≅ P.fansOver := - calc - P.functor ⋙₂ coyoneda (C := C) ≅ - (star E ⋙ pushforward P.p) ⋙₂ (forget B ⋙₂ coyoneda (C := C)) := - Iso.refl _ - - _ ≅ (star E ⋙ pushforward P.p) ⋙₂ Functor.Sigma - ((equivalence_Elements B).functor ⋙ coyoneda (C := Over B)) := - comp₂_isoWhiskerLeft _ (forget_iso_Sigma B) - - _ ≅ Functor.Sigma - ((equivalence_Elements B).functor ⋙ - star E ⋙₂ pushforward P.p ⋙₂ coyoneda (C := Over B)) := - -- Q: better make `comp₂_Sigma` an iso and avoid `eqToIso`? - eqToIso (by simp [comp₂_Sigma]) - - _ ≅ _ := - let i := - calc - star E ⋙₂ pushforward P.p ⋙₂ coyoneda (C := Over B) ≅ - star E ⋙₂ (Over.pullback P.p).op ⋙ coyoneda (C := Over E) := - comp₂_isoWhiskerLeft (star E) (Adjunction.coyoneda_iso <| adj P.p).symm - - _ ≅ (Over.pullback P.p).op ⋙ star E ⋙₂ coyoneda (C := Over E) := - Iso.refl _ - - _ ≅ (Over.pullback P.p).op ⋙ (forget E).op ⋙ coyoneda (C := C) := - isoWhiskerLeft (Over.pullback P.p).op (Adjunction.coyoneda_iso <| forgetAdjStar E).symm; - - Functor.Sigma.isoCongrRight (isoWhiskerLeft _ i) - --- TODO: make modules `UvPoly.UPIso` and `UvPoly.UPFan` --- Alternative definition of `equiv`. -def equiv' (P : UvPoly E B) (Γ X : C) : - (Γ ⟶ P.functor.obj X) ≃ (b : Γ ⟶ B) × (pullback b P.p ⟶ X) := - Iso.toEquiv <| (P.iso_Sigma.app (.op Γ)).app X - -theorem equiv'_app (P : UvPoly E B) (Γ X : C) (be : Γ ⟶ P.functor.obj X) : - P.equiv' Γ X be = (P.iso_Sigma.hom.app <| .op Γ).app X be := by - simp [equiv'] - --- TODO(WN): Checking the theorem statement takes 5s, and kernel typechecking 10s! -lemma equiv'_naturality_left {Δ Γ : C} (σ : Δ ⟶ Γ) (P : UvPoly E B) (X : C) (be : Γ ⟶ P.functor.obj X) : - P.equiv' Δ X (σ ≫ be) = let p := P.equiv' Γ X be - ⟨σ ≫ p.1, pullback.lift (pullback.fst .. ≫ σ) (pullback.snd ..) - (assoc (obj := C) .. ▸ pullback.condition) ≫ p.2⟩ := by - conv_lhs => rw [equiv'_app, coyoneda.comp₂_naturality₂_left, ← equiv'_app] - simp - --- TODO(WN): Kernel typechecking takes 10s! -lemma equiv'_naturality_right {Γ X Y : C} - (P : UvPoly E B) (be : Γ ⟶ P.functor.obj X) (f : X ⟶ Y) : - equiv' P Γ Y (be ≫ P.functor.map f) = - let p := equiv' P Γ X be - ⟨p.1, p.2 ≫ f⟩ := by - conv_lhs => rw [equiv'_app, coyoneda.comp₂_naturality₂_right, ← equiv'_app] - simp - -#exit - /-- 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 -/-- The codomain of the composition of two polynomials. See `UvPoly.comp`. -/ -def compCod {E B D A : C} (P : UvPoly E B) (_ : UvPoly D A) := - P @ A - @[simps!] def comp [HasPullbacks C] [HasTerminal C] - {E B D A : C} (P : UvPoly E B) (Q : UvPoly D A) : UvPoly (compDom P Q) (compCod P Q) := + {E B D A : C} (P : UvPoly E B) (Q : UvPoly D A) : UvPoly (compDom P Q) (P @ A) := { p := (pullback.snd Q.p (fan P A).snd) ≫ (pullback.fst (fan P A).fst P.p) exp := by sorry @@ -469,12 +362,5 @@ instance monoidal [HasPullbacks C] [HasTerminal C] : MonoidalCategory (UvPoly.To rightUnitor := sorry end UvPoly - - - - - - end CategoryTheory - end diff --git a/Poly/UvPoly/UPFan.lean b/Poly/UvPoly/UPFan.lean new file mode 100644 index 0000000..7e000fe --- /dev/null +++ b/Poly/UvPoly/UPFan.lean @@ -0,0 +1,35 @@ +/- +Copyright (c) 2025 Sina Hazratpour. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Sina Hazratpour +-/ +import Poly.UvPoly.Basic + +noncomputable section + +namespace CategoryTheory.UvPoly +open Limits PartialProduct + +universe v u +variable {C : Type u} [Category.{v} C] [HasPullbacks C] [HasTerminal C] {E B : C} + +/-- Universal property of the polynomial functor. -/ +@[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 [partialProd.lift] + rfl + · sorry + right_inv := by + intro ⟨b, e⟩ + ext + · simp only [proj_fst, lift_fst] + · sorry + +end CategoryTheory.UvPoly diff --git a/Poly/UvPoly/UPIso.lean b/Poly/UvPoly/UPIso.lean new file mode 100644 index 0000000..d6d9eb6 --- /dev/null +++ b/Poly/UvPoly/UPIso.lean @@ -0,0 +1,95 @@ +/- +Copyright (c) 2025 Wojciech Nawrocki. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Wojciech Nawrocki +-/ +import Poly.UvPoly.Basic +import Poly.Bifunctor.Sigma + +noncomputable section + +namespace CategoryTheory.UvPoly +open Limits Over ExponentiableMorphism Functor + +universe v u +variable {C : Type u} [Category.{v} C] [HasPullbacks C] {E B : C} (P : UvPoly E B) + +/-- Sends `(Γ, X)` to `Σ(b : Γ ⟶ B), 𝒞(pullback b P.p, X)`. +This is equivalent to the type of partial product cones with apex `Γ` over `X`. -/ +@[simps! obj_obj map_app] +def partProdsOver : Cᵒᵖ ⥤ C ⥤ Type v := + Functor.Sigma + ((Over.equivalence_Elements B).functor ⋙ (Over.pullback P.p).op ⋙ + (forget E).op ⋙ coyoneda (C := C)) + +@[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] + have : 𝟙 Γ.unop ≫ x.1 = x.1 := by simp + ext : 1 + . simp + . dsimp + rw! (castMode := .all) [this] + simp + +variable [HasTerminal C] + +/-- `𝒞(Γ, PₚX) ≅ Σ(b : Γ ⟶ B), 𝒞(b*p, X)` -/ +def iso_Sigma (P : UvPoly E B) : + P.functor ⋙₂ coyoneda (C := C) ≅ P.partProdsOver := + calc + P.functor ⋙₂ coyoneda (C := C) ≅ + (star E ⋙ pushforward P.p) ⋙₂ (forget B ⋙₂ coyoneda (C := C)) := + Iso.refl _ + + _ ≅ (star E ⋙ pushforward P.p) ⋙₂ Functor.Sigma + ((equivalence_Elements B).functor ⋙ coyoneda (C := Over B)) := + comp₂_isoWhiskerLeft _ (forget_iso_Sigma B) + + _ ≅ Functor.Sigma + ((equivalence_Elements B).functor ⋙ + star E ⋙₂ pushforward P.p ⋙₂ coyoneda (C := Over B)) := + -- Q: better make `comp₂_Sigma` an iso and avoid `eqToIso`? + eqToIso (by simp [comp₂_Sigma]) + + _ ≅ _ := + let i := + calc + star E ⋙₂ pushforward P.p ⋙₂ coyoneda (C := Over B) ≅ + star E ⋙₂ (Over.pullback P.p).op ⋙ coyoneda (C := Over E) := + comp₂_isoWhiskerLeft (star E) (Adjunction.coyoneda_iso <| adj P.p).symm + + _ ≅ (Over.pullback P.p).op ⋙ star E ⋙₂ coyoneda (C := Over E) := + Iso.refl _ + + _ ≅ (Over.pullback P.p).op ⋙ (forget E).op ⋙ coyoneda (C := C) := + isoWhiskerLeft (Over.pullback P.p).op (Adjunction.coyoneda_iso <| forgetAdjStar E).symm; + + Functor.Sigma.isoCongrRight (isoWhiskerLeft _ i) + +def equiv (Γ X : C) : (Γ ⟶ P.functor.obj X) ≃ (b : Γ ⟶ B) × (pullback b P.p ⟶ X) := + Iso.toEquiv <| (P.iso_Sigma.app (.op Γ)).app X + +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] + +-- TODO(WN): Checking the theorem statement takes 5s, and kernel typechecking 10s! +lemma equiv_naturality_left {Δ Γ : C} (σ : Δ ⟶ Γ) (X : C) (be : Γ ⟶ P.functor.obj X) : + P.equiv Δ X (σ ≫ be) = + let p := P.equiv Γ X be + ⟨σ ≫ p.1, pullback.lift (pullback.fst .. ≫ σ) (pullback.snd ..) + (Category.assoc (obj := C) .. ▸ pullback.condition) ≫ p.2⟩ := by + conv_lhs => rw [equiv_app, coyoneda.comp₂_naturality₂_left, ← equiv_app] + simp + +-- TODO(WN): Kernel typechecking takes 10s! +lemma equiv_naturality_right {Γ X Y : C} (be : Γ ⟶ P.functor.obj X) (f : X ⟶ Y) : + equiv P Γ Y (be ≫ P.functor.map f) = + let p := equiv P Γ X be + ⟨p.1, p.2 ≫ f⟩ := by + conv_lhs => rw [equiv_app, coyoneda.comp₂_naturality₂_right, ← equiv_app] + simp + +end CategoryTheory.UvPoly From 6e84ebca6b12cccbf8be51ee4be16df4bdf2f66e Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Thu, 20 Mar 2025 21:31:26 -0400 Subject: [PATCH 16/18] chore: not a TODO --- Poly/Bifunctor/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Poly/Bifunctor/Basic.lean b/Poly/Bifunctor/Basic.lean index fc573d8..3ca5ab0 100644 --- a/Poly/Bifunctor/Basic.lean +++ b/Poly/Bifunctor/Basic.lean @@ -70,7 +70,7 @@ namespace coyoneda theorem comp₂_naturality₂_left (F : 𝒟 ⥤ 𝒞) (P : 𝒞ᵒᵖ ⥤ 𝒟 ⥤ Type v) (i : F ⋙₂ coyoneda (C := 𝒞) ⟶ P) (X Y : 𝒞) (Z : 𝒟) (f : X ⟶ Y) (g : Y ⟶ F.obj Z) : - -- TODO: the `op`s really are a pain. Why can't they be definitional like in Lean 3 :( + -- 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] From 70c3fc7951206308e5280c5fd77293a909532a63 Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Thu, 20 Mar 2025 21:36:21 -0400 Subject: [PATCH 17/18] chore: rm clashing imports --- Poly.lean | 2 -- 1 file changed, 2 deletions(-) diff --git a/Poly.lean b/Poly.lean index f04a2ef..3ee25a8 100644 --- a/Poly.lean +++ b/Poly.lean @@ -7,5 +7,3 @@ import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.Presheaf -- import Poly.Type.Univariate -- import Poly.Exponentiable import Poly.UvPoly.Basic -import Poly.UvPoly.UPFan -import Poly.UvPoly.UPIso From b514a5adebd8046abbf93ad22109bace6c9faf2b Mon Sep 17 00:00:00 2001 From: Wojciech Nawrocki Date: Tue, 25 Mar 2025 20:48:43 -0400 Subject: [PATCH 18/18] feat: adjust simp attributes --- Poly/UvPoly/Basic.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Poly/UvPoly/Basic.lean b/Poly/UvPoly/Basic.lean index 6ca2f50..77abc99 100644 --- a/Poly/UvPoly/Basic.lean +++ b/Poly/UvPoly/Basic.lean @@ -97,11 +97,10 @@ def idApplyIso (X : C) : (id B) @ X ≅ B ⨯ X := sorry variable {B} /-- The fstProjection morphism from `∑ b : B, X ^ (E b)` to `B` again. -/ -@[simp] def fstProj (P : UvPoly E B) (X : C) : P @ X ⟶ B := ((Over.star E ⋙ pushforward P.p).obj X).hom -@[simp, reassoc (attr := simp)] +@[reassoc (attr := simp)] lemma map_fstProj {X Y : C} (P : UvPoly E B) (f : X ⟶ Y) : P.functor.map f ≫ P.fstProj Y = P.fstProj X := by simp [fstProj, functor] @@ -275,7 +274,7 @@ polynomial functor. -/ def isLimitFan (P : UvPoly E B) (X : C) : IsLimit (fan P X) where lift c := (pushforwardCurry <| overPullbackToStar c.fst c.snd).left - fac_left := by aesop_cat + fac_left := by aesop_cat (add norm fstProj) fac_right := by intro c simp only [fan_snd, pullbackMap, ε, ev, ← assoc, ← comp_left] @@ -303,6 +302,7 @@ abbrev lift {Γ X : C} (P : UvPoly E B) (b : Γ ⟶ B) (e : pullback b P.p ⟶ X Γ ⟶ P @ X := partialProd.lift ⟨fan P X, isLimitFan P X⟩ b e +@[simp] theorem lift_fst {Γ X : C} {P : UvPoly E B} {b : Γ ⟶ B} {e : pullback b P.p ⟶ X} : P.lift b e ≫ P.fstProj X = b := by unfold lift