References #

[Steve Awodey, Natural models of homotopy type theory][Awodey2017]

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.

source

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

Instances For

source

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

Instances For

source

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 }

Instances For

source

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

source

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

source

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

source

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

⋯ = ⋯

source

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

source

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

source

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

source

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

⋯ = ⋯

source

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

source

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

source

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

source

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

source

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 }

source

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 }

Instances For

source

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 }

Instances For

source

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.

Instances For

source

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 = sorry

Instances For

source

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))

Instances For

source

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

P.apply = P.functor.obj

Instances For

source

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.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 := ⋯ }

Instances For

source

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 (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))

Instances For

source

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 = sorry

Instances For

source

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

Equations

⋯ = ⋯

source

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 }

Instances For

source

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

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

Instances For

source

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

Instances For

source

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))

Instances For

source

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 }

Instances For

source

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

Instances For

source

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

Instances For

source

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 exponentials.

Equations

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

Instances For

source

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

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

Instances For

source

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 : 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

Instances For

source

@[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 : C} {B : C} {X : C} {Y : C} (P : UvPoly E B) (f : X ⟶ Y) :

CategoryTheory.CategoryStruct.comp (P.functor.map f) (P.proj Y) = P.proj X

source

@[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 : C} {B : C} {X : C} {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

source

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

Instances For

source

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 }

Instances For

source

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

source

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

⋯ = ⋯

source

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

source

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

source

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

source

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

⋯ = ⋯

source

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

source

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

(UvPoly.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 := ⋯ }

Instances For

source

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

Instances For

source

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

source

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 := ⋯ }

Instances For

source

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 := ⋯ }

Instances For

source

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

Instances For

source

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 }

Instances For

source

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 ⋯ ⋯ ⋯

source

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 := ⋯ }

Instances For

source

instance UvPoly.instSMulTotal {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasTerminal 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) }

source

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 : 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

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

Instances For

source

@[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 : UvPoly.Total C) :

(UvPoly.smul_eq_prod_const S P).inv = sorry

source

@[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 : UvPoly.Total C) :

(UvPoly.smul_eq_prod_const S P).hom = sorry

source

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

Instances For

source

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

Instances For

Generic pullback #

source

def UvPoly.genPb {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 : 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

Instances For

source

def UvPoly.genPb.fst {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 : C) :

P.genPb X ⟶ P.functor.obj X

Equations

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

Instances For

source

def UvPoly.genPb.u₂ {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 : 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

Instances For

source

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 : C} {B : C} {Γ : C} {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) ⋯ ⋯) (UvPoly.genPb.u₂ P X)

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

source

def UvPoly.equiv {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) (Γ : 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.

Instances For

source

@[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 : C} {B : C} (P : UvPoly E B) (Γ : C) (X : C) (be : Γ ⟶ P.functor.obj X) :

(P.equiv Γ X) be = P.polyPair be

source

@[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 : 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 b e

source

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 : 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.CategoryStruct.comp σ b) P.p) σ) (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp σ b) P.p) ⋯) e⟩

UvPoly.equiv is natural in Γ.

source

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 : C} {B : C} {Γ : C} {X : C} {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.

source

def UvPoly.foo {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} 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 ⋯

Instances For

source

def UvPoly.bar {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} 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 = CategoryTheory.asIso (CategoryTheory.Over.pullbackBeckChevalleyNatTrans P.poly.p f.b f.e Q.poly.p ⋯)

Instances For

source

def UvPoly.bar' {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} 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 = sorry

Instances For

source

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

Instances For

Documentation

Poly.Polynomial

References #

Polynomial Functor #

Generic pullback #