Polynomial Functor

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

structure MvPoly {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] (I : C) (O : C) : Type (max u_1 u_2)

P : MvPoly I O is a multivariable polynomial with input variables in I, output variables in O, and with arities E dependent on I.

• E : C
• B : C
• i : self.E ⟶ I
• p : self.E ⟶ self.B
• exp : CartesianExponentiable self.p
• o : self.B ⟶ O

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

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

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

@[simp]

theorem MvPoly.id_exp_adj_homEquiv_apply_right {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] (I : C) (X : CategoryTheory.Over I) (Y : CategoryTheory.Over I) : ∀ (a : (Δ_ CategoryTheory.CategoryStruct.id I).obj X ⟶ Y), ((CartesianExponentiable.adj.homEquiv X Y) a).right = CategoryTheory.CategoryStruct.id X.right

@[simp]

theorem MvPoly.id_exp_adj_homEquiv_symm_apply_right_down_down {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] (I : C) (X : CategoryTheory.Over I) (Y : CategoryTheory.Over I) : ∀ (a : X ⟶ (CategoryTheory.Functor.id (CategoryTheory.Over I)).obj Y), ⋯ = ⋯

@[simp]

theorem MvPoly.id_exp_adj_unit_app_right {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] (I : C) (X : CategoryTheory.Over I) : (CartesianExponentiable.adj.unit.app X).right = CategoryTheory.CategoryStruct.id X.right

@[simp]

theorem MvPoly.id_E {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] (I : C) : (MvPoly.id I).E = I

@[simp]

theorem MvPoly.id_exp_adj_homEquiv_symm_apply_left {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] (I : C) (X : CategoryTheory.Over I) (Y : CategoryTheory.Over I) : ∀ (a : X ⟶ (CategoryTheory.Functor.id (CategoryTheory.Over I)).obj Y), ((CartesianExponentiable.adj.homEquiv X Y).symm a).left = CategoryTheory.CategoryStruct.comp ((CategoryTheory.baseChange.id I).hom.app X).left ((CategoryTheory.Adjunction.id.homEquiv X Y).symm a).left

@[simp]

theorem MvPoly.id_exp_functor_map {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] (I : C) : ∀ {X Y : CategoryTheory.Over I} (f : X ⟶ Y), (Π_ CategoryTheory.CategoryStruct.id I).map f = f

@[simp]

theorem MvPoly.id_exp_functor_obj {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] (I : C) (X : CategoryTheory.Over I) : (Π_ CategoryTheory.CategoryStruct.id I).obj X = X

@[simp]

theorem MvPoly.id_B {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] (I : C) : (MvPoly.id I).B = I

@[simp]

theorem MvPoly.id_i {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] (I : C) : (MvPoly.id I).i = CategoryTheory.CategoryStruct.id I

@[simp]

theorem MvPoly.id_exp_adj_counit_app_left {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] (I : C) (Y : CategoryTheory.Over I) : (CartesianExponentiable.adj.counit.app Y).left = CategoryTheory.CategoryStruct.comp ((CategoryTheory.baseChange.id I).hom.app Y).left ((CategoryTheory.Adjunction.id.homEquiv Y Y).symm (CategoryTheory.CategoryStruct.id Y)).left

@[simp]

theorem MvPoly.id_exp_adj_homEquiv_apply_left {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] (I : C) (X : CategoryTheory.Over I) (Y : CategoryTheory.Over I) : ∀ (a : (Δ_ CategoryTheory.CategoryStruct.id I).obj X ⟶ Y), ((CartesianExponentiable.adj.homEquiv X Y) a).left = CategoryTheory.CategoryStruct.comp ((CategoryTheory.baseChange.id I).inv.app X).left a.left

@[simp]

theorem MvPoly.id_exp_adj_unit_app_left {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] (I : C) (X : CategoryTheory.Over I) : (CartesianExponentiable.adj.unit.app X).left = ((CategoryTheory.baseChange.id I).inv.app X).left

@[simp]

theorem MvPoly.id_exp_adj_counit_app_right_down_down {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] (I : C) (Y : CategoryTheory.Over I) : ⋯ = ⋯

@[simp]

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

@[simp]

theorem MvPoly.id_o {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] (I : C) : (MvPoly.id I).o = CategoryTheory.CategoryStruct.id I

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

The identity polynomial in many variables.

Equations

• MvPoly.id I = { E := I, B := I, i := CategoryTheory.CategoryStruct.id I, p := CategoryTheory.CategoryStruct.id I, exp := CartesianExponentiable.id, o := CategoryTheory.CategoryStruct.id I }

instance MvPoly.instCartesianExponentiablePId {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] (I : C) : CartesianExponentiable (MvPoly.id I).p

Equations

• MvPoly.instCartesianExponentiablePId I = CartesianExponentiable.id

instance MvPoly.instCartesianExponentiableTo {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasInitial C] (X : C) : CartesianExponentiable (CategoryTheory.Limits.initial.to X)

Given an object X, The unique map initial.to X : ⊥_ C ⟶ X is exponentiable.

Equations

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

def MvPoly.const {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] {I : C} {O : C} [CategoryTheory.Limits.HasInitial C] (A : C) [CategoryTheory.Limits.HasBinaryProduct O A] : MvPoly I O

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

Equations

• MvPoly.const A = { E := ⊥_ C, B := O ⨯ A, i := CategoryTheory.Limits.initial.to I, p := CategoryTheory.Limits.initial.to (O ⨯ A), exp := inferInstance, o := CategoryTheory.Limits.prod.fst }

def MvPoly.monomial {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] {I : C} {O : C} {E : C} (i : E ⟶ I) (p : E ⟶ O) [CartesianExponentiable p] : MvPoly I O

The monomial polynomial in many variables.

Equations

• MvPoly.monomial i p = { E := E, B := O, i := i, p := p, exp := inferInstance, o := CategoryTheory.CategoryStruct.id O }

def MvPoly.sum {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] {I : C} {O : C} [CategoryTheory.Limits.HasBinaryCoproducts C] (P : MvPoly I O) (Q : MvPoly I O) : MvPoly I O

The sum of two polynomials in many variables.

Equations

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

def MvPoly.prod {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] {I : C} {O : C} [CategoryTheory.Limits.HasBinaryProducts C] (P : MvPoly I O) (Q : MvPoly I O) : MvPoly I O

The product of two polynomials in many variables.

Equations

• P.prod Q = sorryAx (MvPoly I O)

def MvPoly.functor {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] {I : C} {O : C} (P : MvPoly I O) : CategoryTheory.Functor (CategoryTheory.Over I) (CategoryTheory.Over O)

Equations

• P.functor = (Δ_ P.i).comp ((Π_ P.p).comp (Σ_ P.o))

def MvPoly.apply {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] (I : C) (O : C) (P : MvPoly I O) [CartesianExponentiable P.p] : CategoryTheory.Over I → CategoryTheory.Over O

Equations

• MvPoly.apply I O P = P.functor.obj

def MvPoly.id_apply {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] (I : C) {X : C} (q : X ⟶ I) : MvPoly.apply I I (MvPoly.id I) (CategoryTheory.Over.mk q) ≅ CategoryTheory.Over.mk q

Equations

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

def MvPoly.pullback_fst {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] {I : C} {J : C} {K : C} (P : MvPoly I J) (Q : MvPoly J K) : CategoryTheory.Limits.pullback P.o Q.i ⟶ P.B

Equations

• P.pullback_fst Q = CategoryTheory.Limits.pullback.fst

def MvPoly.pullback_snd {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] {I : C} {J : C} {K : C} (P : MvPoly I J) (Q : MvPoly J K) : CategoryTheory.Limits.pullback P.o Q.i ⟶ Q.E

Equations

• P.pullback_snd Q = CategoryTheory.Limits.pullback.snd

def MvPoly.pullback_counit {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] {I : C} {J : C} {K : C} (P : MvPoly I J) (Q : MvPoly J K) : (Δ_ Q.p).obj ((Π_ Q.p).obj (CategoryTheory.Over.mk (P.pullback_snd Q))) ⟶ CategoryTheory.Over.mk (P.pullback_snd Q)

Equations

• P.pullback_counit Q = CartesianExponentiable.adj.counit.app (CategoryTheory.Over.mk (P.pullback_snd Q))

def MvPoly.comp {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] {I : C} {J : C} {K : C} (P : MvPoly I J) (Q : MvPoly J K) : MvPoly I K

Equations

• P.comp Q = sorryAx (MvPoly I K)

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

Equations

• ⋯ = ⋯

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

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

Equations

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

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

Equations

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

def UvPoly.prod {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] {E : C} {B : C} {E' : C} {B' : C} (P : UvPoly E B) (Q : UvPoly E' B') [CategoryTheory.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 UvPoly.functor {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] {E : C} {B : C} [CategoryTheory.Limits.HasBinaryProducts C] (P : UvPoly E B) : CategoryTheory.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 = (Δ_ E).comp ((Π_ P.p).comp (Σ_ B))

def UvPoly.toMvPoly {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] {E : C} {B : C} (P : UvPoly E B) : MvPoly (⊤_ C) (⊤_ C)

Equations

• P.toMvPoly = { E := E, B := B, i := CategoryTheory.Limits.terminal.from E, p := P.p, exp := P.exp, o := CategoryTheory.Limits.terminal.from B }

def UvPoly.proj' {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] {E : C} {B : C} (P : UvPoly E B) (X : CategoryTheory.Over (⊤_ C)) : ((Π_ P.p).obj ((Δ_ CategoryTheory.Limits.terminal.from E).obj X)).left ⟶ B

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

Equations

• P.proj' X = (((Δ_ CategoryTheory.Limits.terminal.from E).comp (Π_ P.p)).obj X).hom

def UvPoly.auxFunctor {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] {E : C} {B : C} (P : UvPoly E B) : CategoryTheory.Functor (CategoryTheory.Over (⊤_ C)) (CategoryTheory.Over (⊤_ C))

Equations

• P.auxFunctor = P.toMvPoly.functor

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

We use the equivalence between Over (⊤_ C) and C to get functor : C ⥤ C. Alternatively we can give a direct definition of functor in terms of exponetials.

Equations

• P.functor' = CategoryTheory.equivOverTerminal.functor.comp (P.auxFunctor.comp CategoryTheory.equivOverTerminal.inverse)

def UvPoly.functorIsoFunctor' {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] {E : C} {B : C} [CategoryTheory.Limits.HasBinaryProducts C] (P : UvPoly E B) : P.functor ≅ P.functor'

Equations

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

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

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

Equations

• P.proj X = (((Δ_ E).comp (Π_ P.p)).obj X).hom

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

Essentially star is just the pushforward Beck-Chevalley natural transformation associated to the square defined by g, but you have to compose with various natural isomorphisms.

Equations

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

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

Evaluating a single variable polynomial at an object X

Equations

• P.apply X = P.functor.obj X

@[simp]

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

@[simp]

theorem UvPoly.id_exp_adj_homEquiv_apply_left {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] (B : C) (X : CategoryTheory.Over B) (Y : CategoryTheory.Over B) : ∀ (a : (Δ_ CategoryTheory.CategoryStruct.id B).obj X ⟶ Y), ((CartesianExponentiable.adj.homEquiv X Y) a).left = CategoryTheory.CategoryStruct.comp ((CategoryTheory.baseChange.id B).inv.app X).left a.left

@[simp]

theorem UvPoly.id_exp_adj_unit_app_left {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] (B : C) (X : CategoryTheory.Over B) : (CartesianExponentiable.adj.unit.app X).left = ((CategoryTheory.baseChange.id B).inv.app X).left

@[simp]

theorem UvPoly.id_exp_adj_counit_app_right_down_down {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] (B : C) (Y : CategoryTheory.Over B) : ⋯ = ⋯

@[simp]

theorem UvPoly.id_exp_adj_homEquiv_symm_apply_left {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] (B : C) (X : CategoryTheory.Over B) (Y : CategoryTheory.Over B) : ∀ (a : X ⟶ (CategoryTheory.Functor.id (CategoryTheory.Over B)).obj Y), ((CartesianExponentiable.adj.homEquiv X Y).symm a).left = CategoryTheory.CategoryStruct.comp ((CategoryTheory.baseChange.id B).hom.app X).left ((CategoryTheory.Adjunction.id.homEquiv X Y).symm a).left

@[simp]

theorem UvPoly.id_exp_adj_homEquiv_apply_right {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] (B : C) (X : CategoryTheory.Over B) (Y : CategoryTheory.Over B) : ∀ (a : (Δ_ CategoryTheory.CategoryStruct.id B).obj X ⟶ Y), ((CartesianExponentiable.adj.homEquiv X Y) a).right = CategoryTheory.CategoryStruct.id X.right

@[simp]

theorem UvPoly.id_exp_functor_obj {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] (B : C) (X : CategoryTheory.Over B) : (Π_ CategoryTheory.CategoryStruct.id B).obj X = X

@[simp]

theorem UvPoly.id_exp_adj_counit_app_left {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] (B : C) (Y : CategoryTheory.Over B) : (CartesianExponentiable.adj.counit.app Y).left = CategoryTheory.CategoryStruct.comp ((CategoryTheory.baseChange.id B).hom.app Y).left ((CategoryTheory.Adjunction.id.homEquiv Y Y).symm (CategoryTheory.CategoryStruct.id Y)).left

@[simp]

theorem UvPoly.id_exp_adj_unit_app_right {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] (B : C) (X : CategoryTheory.Over B) : (CartesianExponentiable.adj.unit.app X).right = CategoryTheory.CategoryStruct.id X.right

@[simp]

theorem UvPoly.id_exp_adj_homEquiv_symm_apply_right_down_down {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] (B : C) (X : CategoryTheory.Over B) (Y : CategoryTheory.Over B) : ∀ (a : X ⟶ (CategoryTheory.Functor.id (CategoryTheory.Over B)).obj Y), ⋯ = ⋯

@[simp]

theorem UvPoly.id_exp_functor_map {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] (B : C) : ∀ {X Y : CategoryTheory.Over B} (f : X ⟶ Y), (Π_ CategoryTheory.CategoryStruct.id B).map f = f

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

The identity polynomial functor in single variable.

Equations

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

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

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

Equations

• UvPoly.id_apply B X = { hom := CategoryTheory.CategoryStruct.id (B ⨯ X), inv := CategoryTheory.CategoryStruct.id (B ⨯ X), hom_inv_id := ⋯, inv_hom_id := ⋯ }

structure UvPoly.Hom {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] {E : C} {B : C} {E' : C} {B' : C} (P : UvPoly E B) (Q : UvPoly E' B') : Type 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
  |           |
  e           b
  |           |
  v           v
  E' --Q.p--> B'

is a pullback square.

• e : E ⟶ E'
• b : B ⟶ B'
• is_pullback : CategoryTheory.IsPullback P.p self.e self.b Q.p

theorem UvPoly.Hom.is_pullback {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] {E : C} {B : C} {E' : C} {B' : C} {P : UvPoly E B} {Q : UvPoly E' B'} (self : P.Hom Q) : CategoryTheory.IsPullback P.p self.e self.b Q.p

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

Equations

• UvPoly.Hom.id P = { e := CategoryTheory.CategoryStruct.id E, b := CategoryTheory.CategoryStruct.id B, is_pullback := ⋯ }

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

Equations

• f.comp g = { e := CategoryTheory.CategoryStruct.comp f.e g.e, b := CategoryTheory.CategoryStruct.comp f.b g.b, is_pullback := ⋯ }

structure UvPoly.Total (C : Type u_3) [CategoryTheory.Category.{u_4, u_3} C] [CategoryTheory.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 UvPoly.Total.of {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] {E : C} {B : C} (P : UvPoly E B) : UvPoly.Total C

Equations

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

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

The category of polynomial functors in a single variable.

Equations

• instCategoryTotal = CategoryTheory.Category.mk ⋯ ⋯ ⋯

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

Equations

• Total.ofHom P Q α = { e := α.e, b := α.b, is_pullback := ⋯ }

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

Equations

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

@[simp]

theorem UvPoly.smul_eq_prod_const_hom {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasInitial C] (S : C) (P : UvPoly.Total C) : (UvPoly.smul_eq_prod_const S P).hom = sorryAx (S • P ⟶ UvPoly.Total.of ((UvPoly.const S).prod P.poly))

@[simp]

theorem UvPoly.smul_eq_prod_const_inv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasInitial C] (S : C) (P : UvPoly.Total C) : (UvPoly.smul_eq_prod_const S P).inv = sorryAx (UvPoly.Total.of ((UvPoly.const S).prod P.poly) ⟶ S • P)

def UvPoly.smul_eq_prod_const {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasInitial C] (S : C) (P : UvPoly.Total C) : S • P ≅ UvPoly.Total.of ((UvPoly.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

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

def UvPoly.polyPair {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {E : C} {B : C} (P : UvPoly E B) (Γ : C) (X : C) (be : Γ ⟶ P.functor.obj X) : (b : Γ ⟶ B) × (CategoryTheory.Limits.pullback b P.p ⟶ X)

Equations

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

def UvPoly.pairPoly {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {E : C} {B : C} (P : UvPoly E B) (Γ : C) (X : C) (b : Γ ⟶ B) (e : CategoryTheory.Limits.pullback b P.p ⟶ X) : Γ ⟶ P.functor.obj X

Equations

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

@[simp]

theorem UvPoly.equiv_apply {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {E : C} {B : C} (P : UvPoly E B) (Γ : C) (X : C) (be : Γ ⟶ P.functor.obj X) : (P.equiv Γ X) be = P.polyPair Γ X be

@[simp]

theorem UvPoly.equiv_symm_apply {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {E : C} {B : C} (P : UvPoly E B) (Γ : C) (X : C) : ∀ (x : (b : Γ ⟶ B) × (CategoryTheory.Limits.pullback b P.p ⟶ X)), (P.equiv Γ X).symm x = match x with | ⟨b, e⟩ => P.pairPoly Γ X b e

def UvPoly.equiv {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {E : C} {B : C} (P : UvPoly E B) (Γ : C) (X : C) : (Γ ⟶ P.functor.obj X) ≃ (b : Γ ⟶ B) × (CategoryTheory.Limits.pullback b P.p ⟶ X)

Universal property of the polynomial functor.

Equations

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

theorem UvPoly.equiv_naturality {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] {E : C} {B : C} {Δ : C} {Γ : C} (σ : Δ ⟶ Γ) (P : UvPoly E B) (X : C) (be : Γ ⟶ P.functor.obj X) : (P.equiv Δ X) (CategoryTheory.CategoryStruct.comp σ be) = match (P.equiv Γ X) be with | ⟨b, e⟩ => ⟨CategoryTheory.CategoryStruct.comp σ b, CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pullback.fst σ) CategoryTheory.Limits.pullback.snd ⋯) e⟩

UvPoly.equiv is natural in Γ.

def UvPoly.foo {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasBinaryProducts C] {P : UvPoly.Total C} {Q : UvPoly.Total C} (f : P ⟶ Q) : (Σ_ P.poly.p).comp (Σ_ f.b) ≅ (Σ_ f.e).comp (Σ_ Q.poly.p)

Equations

• UvPoly.foo f = CategoryTheory.Over.mapSquareIso P.poly.p f.b f.e Q.poly.p ⋯

def UvPoly.bar {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasBinaryProducts C] {P : UvPoly.Total C} {Q : UvPoly.Total C} (f : P ⟶ Q) : (Δ_ f.e).comp (Σ_ P.poly.p) ≅ (Σ_ Q.poly.p).comp (Δ_ f.b)

Equations

• UvPoly.bar f = let l := CategoryTheory.Over.pullbackBeckChevalleyNatTrans P.poly.p f.b f.e Q.poly.p ⋯; let_fun this := ⋯; CategoryTheory.asIso l

def UvPoly.bar' {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasBinaryProducts C] {P : UvPoly.Total C} {Q : UvPoly.Total C} (f : P ⟶ Q) : (Δ_ P.poly.p).comp (Σ_ f.e) ≅ (Σ_ f.b).comp (Δ_ Q.poly.p)

Equations

• UvPoly.bar' f = sorryAx ((Δ_ P.poly.p).comp (Σ_ f.e) ≅ (Σ_ f.b).comp (Δ_ Q.poly.p))

def UvPoly.naturality {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasBinaryProducts C] {P : UvPoly.Total C} {Q : UvPoly.Total C} (f : P ⟶ Q) : P.poly.functor ⟶ Q.poly.functor

A map of polynomials induces a natural transformation between their associated functors.

Equations

• UvPoly.naturality f = sorryAx (P.poly.functor ⟶ Q.poly.functor)