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 UvPoly {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Limits.HasPullbacks C] (E 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

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

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 B : C} [CategoryTheory.Limits.HasBinaryProducts C] (S : C) (P : UvPoly E B) : UvPoly (S ⨯ E) (S ⨯ B)

Equations

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

def UvPoly.prod {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] {E B E' 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 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 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 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 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 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 exponentials.

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 B : C} [CategoryTheory.Limits.HasBinaryProducts C] (P : UvPoly E B) : P.functor ≅ P.functor'

Equations

• P.functorIsoFunctor' = id (id (id (id (id (id sorry)))))

def UvPoly.proj {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] {E 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

@[simp]

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

@[simp]

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

def UvPoly.star {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] {E B 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.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 }

@[simp]

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

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

@[simp]

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

@[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

@[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_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

def UvPoly.id_apply {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] (B X : C) : (id B).functor.obj 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 B E' 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

def UvPoly.Hom.id {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] {E 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 B E' B' E'' 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 B : C} (P : UvPoly E B) : 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 B E' 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_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] : SMul C (Total C)

Equations

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

def UvPoly.smul_eq_prod_const {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.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

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

@[simp]

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

@[simp]

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

def UvPoly.polyPair {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] {E B Γ X : C} (P : UvPoly E B) (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_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] {E B Γ X : C} (P : UvPoly E B) (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.

Generic pullback

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

The UP of polynomial functors is mediated by a "generic pullback" [Awodey2017, p. 10, fig. 6].

     X
     ^
     | u₂
   genPb ---------------> E
 fst | ┘                  | p
     v                    v
P.functor.obj X --------> B
                P.proj X

Equations

• P.genPb X = CategoryTheory.Limits.pullback (P.proj X) P.p

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

Equations

• UvPoly.genPb.fst P X = CategoryTheory.Limits.pullback.fst (P.proj X) P.p

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

Equations

• UvPoly.genPb.u₂ P X = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.congrHom ⋯ ⋯).hom (P.polyPair (CategoryTheory.CategoryStruct.id (P.functor.obj X))).snd

theorem UvPoly.genPb.polyPair_snd_eq_comp_u₂' {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] {E B Γ X : C} (P : UvPoly E B) (be : Γ ⟶ P.functor.obj X) : (P.polyPair be).snd = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.map (P.polyPair be).fst P.p (P.proj X) P.p be (CategoryTheory.CategoryStruct.id E) (CategoryTheory.CategoryStruct.id B) ⋯ ⋯) (u₂ P X)

The second component of polyPair is a comparison map of pullbacks composed with genPb.u₂.

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

@[simp]

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

@[simp]

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

theorem UvPoly.equiv_naturality_left {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] {E B Δ Γ : 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.CategoryStruct.comp σ b) P.p) σ) (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp σ b) P.p) ⋯) e⟩

UvPoly.equiv is natural in Γ.

theorem UvPoly.equiv_naturality_right {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasPullbacks C] {E B Γ X Y : C} (P : UvPoly E B) (be : Γ ⟶ P.functor.obj X) (f : X ⟶ Y) : (P.equiv Γ Y) (CategoryTheory.CategoryStruct.comp be (P.functor.map f)) = match (P.equiv Γ X) be with | ⟨b, e⟩ => ⟨b, CategoryTheory.CategoryStruct.comp e f⟩

UvPoly.equiv is natural in X.

def UvPoly.foo {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasBinaryProducts C] {P Q : 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_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasBinaryProducts C] {P Q : Total C} (f : P ⟶ Q) : (Δ_ f.e).comp (Σ_ P.poly.p) ≅ (Σ_ Q.poly.p).comp (Δ_ f.b)

Equations

• UvPoly.bar f = CategoryTheory.asIso (CategoryTheory.Over.pullbackBeckChevalleyNatTrans P.poly.p f.b f.e Q.poly.p ⋯)

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

Equations

• UvPoly.bar' f = sorry

def UvPoly.naturality {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasBinaryProducts C] {P Q : 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 = sorry

def UvPoly.compDom {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.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 (UvPoly.genPb.u₂ P A)

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

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

Equations

• P.compCod x✝ = P.functor.obj A

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

Equations

• P.comp Q = { p := CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd Q.p (UvPoly.genPb.u₂ P A)) (UvPoly.genPb.fst P A), exp := sorry }

@[simp]

theorem UvPoly.comp_exp {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasTerminal C] {E B D A : C} (P : UvPoly E B) (Q : UvPoly D A) : (P.comp Q).exp = sorry

@[simp]

theorem UvPoly.comp_p {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.Limits.HasTerminal C] {E B D A : C} (P : UvPoly E B) (Q : UvPoly D A) : (P.comp Q).p = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd Q.p (genPb.u₂ P A)) (genPb.fst P A)

def UvPoly.compFunctorIso {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasPullbacks C] [CategoryTheory.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