Polynomial Functor

-- TODO: there are various sorry-carrying proofs in below which require instances of CartesianExponentiable for various constructions 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 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

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 }

@[simp]

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

@[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_p {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] (I : C) : (id I).p = CategoryTheory.CategoryStruct.id I

@[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_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_adj_unit_app_right_down_down {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] (I : C) (X : CategoryTheory.Over I) : ⋯ = ⋯

@[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.CategoryStruct.comp (CategoryTheory.Adjunction.id.unit.app X).left ((CategoryTheory.Adjunction.equivHomsetLeftOfNatIso (CategoryTheory.baseChange.id I)) (CategoryTheory.CategoryStruct.id ((Δ_ CategoryTheory.CategoryStruct.id I).obj X))).left

@[simp]

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

@[simp]

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

@[simp]

theorem MvPoly.id_B {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] (I : C) : (id I).B = 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

instance MvPoly.instCartesianExponentiablePId {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] (I : C) : CartesianExponentiable (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

• MvPoly.instCartesianExponentiableTo X = { functor := { obj := sorry, map := fun {X_1 Y : CategoryTheory.Over (⊥_ C)} => sorry, map_id := ⋯, map_comp := ⋯ }, adj := sorry }

def MvPoly.const {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] {I 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 O 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 O : C} [CategoryTheory.Limits.HasBinaryCoproducts C] (P 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 O : C} [CategoryTheory.Limits.HasBinaryProducts C] (P Q : MvPoly I O) : MvPoly I O

The product of two polynomials in many variables.

Equations

• P.prod Q = sorry

def MvPoly.functor {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] {I 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 O : C} (P : MvPoly I O) [CartesianExponentiable P.p] : CategoryTheory.Over I → CategoryTheory.Over O

Equations

• P.apply = 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) : (id I).apply (CategoryTheory.Over.mk q) ≅ CategoryTheory.Over.mk q

Equations

• MvPoly.id_apply I q = { hom := id (id { left := id sorry, right := sorry, w := ⋯ }), inv := sorry, hom_inv_id := ⋯, inv_hom_id := ⋯ }

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

Equations

• P.pullback_counit Q = CartesianExponentiable.adj.counit.app (CategoryTheory.Over.mk (CategoryTheory.Limits.pullback.snd P.o Q.i))

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

Equations

• P.comp Q = sorry