Polynomial Functor

The Universal property of polynomial functors is mediated through the partial product diagram in below.

     X
     ^
     |
     |
     • -------fst-----> P @ X
     |                    |
     |        (pb)        | P.fstProj X
     v                    v
     E ---------------->  B
              P.p

-- TODO: there are various sorry-carrying proofs in below which require instances of ExponentiableMorphism for various constructions on morphisms. They need to be defined in Poly.Exponentiable.

structure CategoryTheory.UvPoly {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] (E B : C) : Type u_2

P : UvPoly C is a polynomial functors in a single variable

• p : E ⟶ B
• exp : ExponentiableMorphism self.p

instance CategoryTheory.UvPoly.instHasBinaryProducts {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] : Limits.HasBinaryProducts C

def CategoryTheory.UvPoly.const {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasPullbacks C] [Limits.HasInitial C] (S : C) : UvPoly (⊥_ C) S

The constant polynomial in many variables: for this we need the initial object

Equations

• CategoryTheory.UvPoly.const S = { p := CategoryTheory.Limits.initial.to S, exp := ⋯ }

def CategoryTheory.UvPoly.smul {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasPullbacks C] {E B : C} [Limits.HasBinaryProducts C] (S : C) (P : UvPoly E B) : UvPoly (S ⨯ E) (S ⨯ B)

Equations

• CategoryTheory.UvPoly.smul S P = { p := CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id S) P.p, exp := ⋯ }

def CategoryTheory.UvPoly.prod {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] {E B E' B' : C} (P : UvPoly E B) (Q : UvPoly E' B') [Limits.HasBinaryCoproducts C] : UvPoly ((E ⨯ B') ⨿ B ⨯ E') (B ⨯ B')

The product of two polynomials in a single variable.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.UvPoly.functor {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasPullbacks C] {E B : C} [Limits.HasBinaryProducts C] (P : UvPoly E B) : Functor C 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.

Equations

• P.functor = (CategoryTheory.Over.star E).comp ((CategoryTheory.ExponentiableMorphism.pushforward P.p).comp (CategoryTheory.Over.forget B))

def CategoryTheory.UvPoly.apply {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] {E B : C} (P : UvPoly E B) : C → C

The evaluation function of a polynomial P at an object X.

Equations

• P.apply = P.functor.obj

def CategoryTheory.UvPoly.«term_@_» : Lean.TrailingParserDescr

The evaluation function of a polynomial P at an object X.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.UvPoly.id {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasPullbacks C] (B : C) : UvPoly B B

The identity polynomial functor in single variable.

Equations

• CategoryTheory.UvPoly.id B = { p := CategoryTheory.CategoryStruct.id B, exp := ⋯ }

@[simp]

theorem CategoryTheory.UvPoly.id_p {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasPullbacks C] (B : C) : (id B).p = CategoryStruct.id B

def CategoryTheory.UvPoly.idIso {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] (B : C) : (id B).functor ≅ (Over.star B).comp (Over.forget B)

The functor associated to the identity polynomial is isomorphic to the identity functor.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.UvPoly.idApplyIso {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] (B X : C) : id B @ X ≅ B ⨯ X

Evaluating the identity polynomial at an object X is isomorphic to B × X.

Equations

• CategoryTheory.UvPoly.idApplyIso B X = sorry

def CategoryTheory.UvPoly.fstProj {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] {E B : C} (P : UvPoly E B) (X : C) : P @ X ⟶ B

The fstProjection morphism from ∑ b : B, X ^ (E b) to B again.

Equations

• P.fstProj X = (((CategoryTheory.Over.star E).comp (CategoryTheory.ExponentiableMorphism.pushforward P.p)).obj X).hom

@[simp]

theorem CategoryTheory.UvPoly.map_fstProj {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] {E B X Y : C} (P : UvPoly E B) (f : X ⟶ Y) : CategoryStruct.comp (P.functor.map f) (P.fstProj Y) = P.fstProj X

@[simp]

theorem CategoryTheory.UvPoly.map_fstProj_assoc {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] {E B X Y : C} (P : UvPoly E B) (f : X ⟶ Y) {Z : C} (h : B ⟶ Z) : CategoryStruct.comp (P.functor.map f) (CategoryStruct.comp (P.fstProj Y) h) = CategoryStruct.comp (P.fstProj X) h

def CategoryTheory.UvPoly.verticalNatTrans {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] {E B F : C} (P : UvPoly E B) (Q : UvPoly F B) (ρ : E ⟶ F) (h : P.p = CategoryStruct.comp ρ Q.p) : Q.functor ⟶ P.functor

A vertical map ρ : P.p ⟶ Q.p of polynomials (i.e. a commutative triangle)

    ρ
E ----> F
 \     /
  \   /
   \ /
    B

induces a natural transformation Q.functor ⟶ P.functor obtained by pasting the following 2-cells

              Q.p
C --- >  C/F ----> C/B -----> C
|         |          |        |
|   ↙     | ρ*  ≅    |   =    |
|         v          v        |
C --- >  C/E ---->  C/B ----> C
              P.p

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.UvPoly.cartesianNaturalTrans {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasPullbacks C] {E B D F : C} [Limits.HasBinaryProducts C] (P : UvPoly E B) (Q : UvPoly F D) (δ : B ⟶ D) (φ : E ⟶ F) (pb : IsPullback P.p φ δ Q.p) : P.functor ⟶ Q.functor

A cartesian map of polynomials

           P.p
      E -------->  B
      |            |
   φ  |            | δ
      v            v
      F -------->  D
           Q.p

induces a natural transformation between their associated functors obtained by pasting the following 2-cells

              Q.p
C --- >  C/F ----> C/D -----> C
|         |          |        |
|   ↗     | φ*  ≅    | δ* ↗   |
|         v          v        |
C --- >  C/E ---->  C/B ----> C
              P.p

Equations

• One or more equations did not get rendered due to their size.

structure CategoryTheory.UvPoly.Hom {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasPullbacks C] {E B F D : C} (P : UvPoly E B) (Q : UvPoly F D) : Type (max u_2 u_3)

A morphism from a polynomial P to a polynomial Q is a pair of morphisms e : E ⟶ E' and b : B ⟶ B' such that the diagram

      E -- P.p ->  B
      ^            |
   ρ  |            |
      |     ψ      |
      Pb --------> B
      |            |
   φ  |            | δ
      v            v
      F -- Q.p ->  D

is a pullback square.

• Pb : C
• δ : B ⟶ D
• φ : self.Pb ⟶ F
• ψ : self.Pb ⟶ B
• ρ : self.Pb ⟶ E
• is_pb : IsPullback self.ψ self.φ self.δ Q.p
• w : CategoryStruct.comp self.ρ P.p = self.ψ

def CategoryTheory.UvPoly.Hom.id {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasPullbacks C] {E B : C} (P : UvPoly E B) : P.Hom P

The identity morphism in the category of polynomials.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.UvPoly.Hom.comp {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasPullbacks C] {E B F D N M : C} {P : UvPoly E B} {Q : UvPoly F D} {R : UvPoly N M} (f : P.Hom Q) (g : Q.Hom R) : P.Hom R

The composition of morphisms in the category of polynomials.

Equations

• f.comp g = sorry

structure CategoryTheory.UvPoly.Total (C : Type u_3) [Category.{u_4, u_3} C] [Limits.HasPullbacks C] : Type (max u_3 u_4)

Bundling up the the polynomials over different bases to form the underlying type of the category of polynomials.

• E : C
• B : C
• poly : UvPoly self.E self.B

def CategoryTheory.UvPoly.Total.of {C : Type u_2} [Category.{u_3, u_2} C] [Limits.HasPullbacks C] {E B : C} (P : UvPoly E B) : Total C

Equations

• CategoryTheory.UvPoly.Total.of P = { E := E, B := B, poly := P }

instance CategoryTheory.instCategoryTotal {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] : Category.{max u_2 u_1, max u_2 u_1} (UvPoly.Total C)

The category of polynomial functors in a single variable.

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Total.ofHom {C : Type u_1} [Category.{u_2, u_1} C] [Limits.HasPullbacks C] {E B E' B' : C} (P : UvPoly E B) (Q : UvPoly E' B') (α : P.Hom Q) : UvPoly.Total.of P ⟶ UvPoly.Total.of Q

Equations

• CategoryTheory.Total.ofHom P Q α = sorry

instance CategoryTheory.UvPoly.instSMulTotal {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] : SMul C (Total C)

Equations

• CategoryTheory.UvPoly.instSMulTotal = { smul := fun (S : C) (P : CategoryTheory.UvPoly.Total C) => CategoryTheory.UvPoly.Total.of (CategoryTheory.UvPoly.smul S P.poly) }

def CategoryTheory.UvPoly.smul_eq_prod_const {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] [Limits.HasBinaryCoproducts C] [Limits.HasInitial C] (S : C) (P : Total C) : S • P ≅ Total.of ((const S).prod P.poly)

Scaling a polynomial P by an object S is isomorphic to the product of const S and the polynomial P.

Equations

• CategoryTheory.UvPoly.smul_eq_prod_const S P = { hom := sorry, inv := sorry, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.UvPoly.smul_eq_prod_const_hom {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] [Limits.HasBinaryCoproducts C] [Limits.HasInitial C] (S : C) (P : Total C) : (smul_eq_prod_const S P).hom = sorry

@[simp]

theorem CategoryTheory.UvPoly.smul_eq_prod_const_inv {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] [Limits.HasBinaryCoproducts C] [Limits.HasInitial C] (S : C) (P : Total C) : (smul_eq_prod_const S P).inv = sorry

def CategoryTheory.UvPoly.PartialProduct.ε {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] {E B : C} (P : UvPoly E B) (X : C) : Limits.pullback (P.fstProj X) P.p ⟶ E ⨯ X

The counit of the adjunction pullback P.p ⊣ pushforward P.p evaluated (star E).obj X.

Equations

• CategoryTheory.UvPoly.PartialProduct.ε P X = ((CategoryTheory.ExponentiableMorphism.ev P.p).app ((CategoryTheory.Over.star E).obj X)).left

def CategoryTheory.UvPoly.PartialProduct.fan {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] {E B : C} (P : UvPoly E B) (X : C) : PartialProduct.Fan P.p X

The partial product fan associated to a polynomial P : UvPoly E B and an object X : C.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.UvPoly.PartialProduct.fan_fst {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] {E B : C} (P : UvPoly E B) (X : C) : (fan P X).fst = P.fstProj X

@[simp]

theorem CategoryTheory.UvPoly.PartialProduct.fan_pt {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] {E B : C} (P : UvPoly E B) (X : C) : (fan P X).pt = P @ X

@[simp]

theorem CategoryTheory.UvPoly.PartialProduct.fan_snd {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] {E B : C} (P : UvPoly E B) (X : C) : (fan P X).snd = CategoryStruct.comp (ε P X) Limits.prod.snd

def CategoryTheory.UvPoly.PartialProduct.isLimitFan {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] {E B : C} (P : UvPoly E B) (X : C) : PartialProduct.IsLimit (fan P X)

P.PartialProduct.fan is in fact a limit fan; this provides the univeral mapping property of the polynomial functor.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev CategoryTheory.UvPoly.lift {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] {E B Γ X : C} (P : UvPoly E B) (b : Γ ⟶ B) (e : Limits.pullback b P.p ⟶ X) : Γ ⟶ P @ X

Morphisms b : Γ ⟶ B and e : pullback b P.p ⟶ X induce a morphism Γ ⟶ P @ X which is the lift of the partial product fan.

Equations

• P.lift b e = CategoryTheory.partialProd.lift { cone := CategoryTheory.UvPoly.PartialProduct.fan P X, isLimit := CategoryTheory.UvPoly.PartialProduct.isLimitFan P X } b e

@[simp]

theorem CategoryTheory.UvPoly.lift_fst {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] {E B Γ X : C} {P : UvPoly E B} {b : Γ ⟶ B} {e : Limits.pullback b P.p ⟶ X} : CategoryStruct.comp (P.lift b e) (P.fstProj X) = b

theorem CategoryTheory.UvPoly.lift_snd {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] {E B Γ X : C} {P : UvPoly E B} {b : Γ ⟶ B} {e : Limits.pullback b P.p ⟶ X} : CategoryStruct.comp (PartialProduct.comparison (P.lift b e)) (CategoryStruct.comp (PartialProduct.ε P X) Limits.prod.snd) = CategoryStruct.comp (Limits.pullback.congrHom ⋯ ⋯).hom e

theorem CategoryTheory.UvPoly.lift_snd_assoc {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] {E B Γ X : C} {P : UvPoly E B} {b : Γ ⟶ B} {e : Limits.pullback b P.p ⟶ X} {Z : C} (h : X ⟶ Z) : CategoryStruct.comp (PartialProduct.comparison (P.lift b e)) (CategoryStruct.comp (PartialProduct.ε P X) (CategoryStruct.comp Limits.prod.snd h)) = CategoryStruct.comp (Limits.pullback.congrHom ⋯ ⋯).hom (CategoryStruct.comp e h)

def CategoryTheory.UvPoly.proj {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] {E B Γ X : C} (P : UvPoly E B) (f : Γ ⟶ P @ X) : (b : Γ ⟶ B) × (Limits.pullback b P.p ⟶ X)

A morphism f : Γ ⟶ P @ X projects to a morphism b : Γ ⟶ B and a morphism e : pullback b P.p ⟶ X.

Equations

• P.proj f = ⟨((CategoryTheory.UvPoly.PartialProduct.fan P X).extend f).fst, ((CategoryTheory.UvPoly.PartialProduct.fan P X).extend f).snd⟩

@[simp]

theorem CategoryTheory.UvPoly.proj_fst {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] {E B Γ X : C} {P : UvPoly E B} {f : Γ ⟶ P @ X} : (P.proj f).fst = CategoryStruct.comp f (P.fstProj X)

@[simp]

theorem CategoryTheory.UvPoly.proj_snd {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] {E B Γ X : C} {P : UvPoly E B} {f : Γ ⟶ P @ X} : (P.proj f).snd = CategoryStruct.comp (Limits.pullback.map (P.proj f).fst P.p (P.fstProj X) P.p f (CategoryStruct.id E) (CategoryStruct.id B) ⋯ ⋯) (CategoryStruct.comp (PartialProduct.ε P X) Limits.prod.snd)

The second component of proj is a comparison map of pullbacks composed with ε P X ≫ prod.snd

def CategoryTheory.UvPoly.compDom {C : Type u} [Category.{v, u} C] [Limits.HasTerminal C] [Limits.HasPullbacks C] {E B D A : C} (P : UvPoly E B) (Q : UvPoly D A) : C

The domain of the composition of two polynomials. See UvPoly.comp.

Equations

• P.compDom Q = CategoryTheory.Limits.pullback Q.p (CategoryTheory.UvPoly.PartialProduct.fan P A).snd

def CategoryTheory.UvPoly.comp {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] [Limits.HasTerminal C] {E B D A : C} (P : UvPoly E B) (Q : UvPoly D A) : UvPoly (P.compDom Q) (P @ A)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.UvPoly.comp_p {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] [Limits.HasTerminal C] {E B D A : C} (P : UvPoly E B) (Q : UvPoly D A) : (P.comp Q).p = CategoryStruct.comp (Limits.pullback.snd Q.p (CategoryStruct.comp (PartialProduct.ε P A) Limits.prod.snd)) (Limits.pullback.fst (P.fstProj A) P.p)

def CategoryTheory.UvPoly.compFunctorIso {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] [Limits.HasTerminal C] {E B D C✝ : C} (P : UvPoly E B) (Q : UvPoly D C✝) : P.functor.comp Q.functor ≅ (P.comp Q).functor

The associated functor of the composition of two polynomials is isomorphic to the composition of the associated functors.

Equations

• P.compFunctorIso Q = sorry

instance CategoryTheory.UvPoly.monoidal {C : Type u} [Category.{v, u} C] [Limits.HasPullbacks C] [Limits.HasTerminal C] : MonoidalCategory (Total C)

Equations

• One or more equations did not get rendered due to their size.