Polynomial Functors

Definitions of common PFunctor constructions:

• monomial A B: constant direction B for any shape a : A
• P + Q: shapes are a disjoint sum, directions are defined by sum elimination on a : P.A ⊕ Q.A
• P * Q: shapes are pairs of underlying shapes, directions are a disjoint sum over both shapes.

Special cases C, linear, selfMonomial, purePower, the indeterminate y, and canonical choices of 0 and 1 are defined as abbreviations or instances over monomial. The scoped notations A y^ B and y^ B denote monomial A B and purePower B, respectively.

The child-map API includes const, Unary, and DecidableEqChildren.

theorem PFunctor.ext {P Q : PFunctor.{uA, uB}} (h : P.A = Q.A) (h' : ∀ (a : P.A), P.B a = Q.B (h ▸ a)) : P = Q

Two polynomial functors are equal if their head types are equal and their child types agree over that equality.

def PFunctor.const {α : Sort u_1} {P : PFunctor.{u_2, u_3}} (a : P.A) (x : α) : P.B a → α

The constant child map for a.

Equations

• PFunctor.const a x x✝ = x

@[simp]

theorem PFunctor.const_apply {α : Sort u_1} {P : PFunctor.{u_2, u_3}} (a : P.A) (x : α) (i : P.B a) : const a x i = x

@[reducible, inline]

abbrev PFunctor.monomial (A : Type uA) (B : Type uB) : PFunctor.{uA, uB}

The monomial PFunctor with head type A and constant B for any a : A.

Equations

• PFunctor.monomial A B = { A := A, B := fun (x : A) => B }

def PFunctor.«term_Y^_» : Lean.TrailingParserDescr

The monomial PFunctor with head type A and constant B for any a : A.

Equations

• PFunctor.«term_Y^_» = Lean.ParserDescr.trailingNode `PFunctor.«term_Y^_» 82 83 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " y^ ") (Lean.ParserDescr.cat `term 82))

theorem PFunctor.monomial_A (A : Type uA) (B : Type uB) : (monomial A B).A = A

theorem PFunctor.monomial_B (A : Type uA) (B : Type uB) (a : (monomial A B).A) : (monomial A B).B a = B

@[instance_reducible]

instance PFunctor.instZeroPFunctor : Zero PFunctor.{u_2, u_1}

The zero polynomial functor, defined as A = PEmpty and B _ = PEmpty, is the identity with respect to sum (up to equivalence).

Equations

• PFunctor.instZeroPFunctor = { zero := PFunctor.monomial PEmpty.{?u.1 + 1} PEmpty.{?u.2 + 1} }

@[simp]

theorem PFunctor.zero_A : A 0 = PEmpty.{u_2 + 1}

@[simp]

theorem PFunctor.zero_B (x✝ : PEmpty.{u_2 + 1}) : B 0 x✝ = PEmpty.{u_1 + 1}

instance PFunctor.instIsEmptyZeroPFunctor : IsEmpty (A 0)

@[instance_reducible]

instance PFunctor.instOnePFunctor : One PFunctor.{u_2, u_1}

The unit polynomial functor, defined as A = PUnit and B _ = PEmpty, is the identity with respect to product (up to equivalence).

Equations

• PFunctor.instOnePFunctor = { one := PFunctor.monomial PUnit.{?u.1 + 1} PEmpty.{?u.2 + 1} }

@[simp]

theorem PFunctor.one_A : A 1 = PUnit.{u_2 + 1}

@[simp]

theorem PFunctor.one_B (x✝ : PUnit.{u_2 + 1}) : B 1 x✝ = PEmpty.{u_1 + 1}

@[instance_reducible]

instance PFunctor.instUniqueOneA : Unique (A 1)

Equations

• PFunctor.instUniqueOneA = { default := PUnit.unit, uniq := ⋯ }

instance PFunctor.instIsEmptyOneB (a : A 1) : IsEmpty (B 1 a)

@[reducible, inline]

abbrev PFunctor.C (A : Type uA) : PFunctor.{uA, u_1}

The constant polynomial functor P(y) = A y^ PEmpty = A.

Equations

• PFunctor.C A = PFunctor.monomial A PEmpty.{?u.1 + 1}

@[reducible, inline]

abbrev PFunctor.linear (A : Type uA) : PFunctor.{uA, u_1}

The linear polynomial functor P(y) = A y.

Equations

• PFunctor.linear A = PFunctor.monomial A PUnit.{?u.1 + 1}

@[reducible, inline]

abbrev PFunctor.selfMonomial (S : Type uA) : PFunctor.{uA, uA}

The self-monomial polynomial functor P(y) = S y^ S.

Equations

• PFunctor.selfMonomial S = PFunctor.monomial S S

@[reducible, inline]

abbrev PFunctor.purePower (B : Type uB) : PFunctor.{u_1, uB}

The pure-power polynomial functor y^ B, representable on B.

Equations

• PFunctor.purePower B = PFunctor.monomial PUnit.{?u.1 + 1} B

def PFunctor.«termY^_» : Lean.ParserDescr

The pure-power polynomial functor y^ B, representable on B.

Equations

• PFunctor.«termY^_» = Lean.ParserDescr.node `PFunctor.«termY^_» 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "y^") (Lean.ParserDescr.cat `term 100))

@[reducible, inline]

abbrev PFunctor.y : PFunctor.{u_1, u_2}

The indeterminate polynomial functor P(y) = y, the identity with respect to composition and tensor product (up to equivalence).

Equations

• PFunctor.y = PFunctor.monomial PUnit.{?u.2 + 1} PUnit.{?u.1 + 1}

@[simp]

theorem PFunctor.C_pempty : C PEmpty.{u_2 + 1} = 0

@[simp]

theorem PFunctor.C_punit : C PUnit.{u_2 + 1} = 1

@[simp]

theorem PFunctor.linear_punit : linear PUnit.{u_2 + 1} = y

@[simp]

theorem PFunctor.selfMonomial_punit : selfMonomial PUnit.{u_1 + 1} = y

@[simp]

theorem PFunctor.purePower_punit : purePower PUnit.{u_1 + 1} = y

@[implicit_reducible]

def PFunctor.add (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) : PFunctor.{max uA₁ uA₂, uB}

The sum of two polynomial functors P and Q, written as P + Q, defined as the sum of the head types and the dependent sum recursor for the child types.

The child universes must agree. The named spelling P.add Q can elaborate in contexts where P + Q fails to infer universes, such as under PFunctor.W; see CslibTests.PFunctor.

Equations

• P.add Q = { A := P.A ⊕ Q.A, B := Sum.rec P.B Q.B }

@[instance_reducible]

instance PFunctor.instHAddPFunctor : HAdd PFunctor.{uA₁, uB} PFunctor.{uA₂, uB} PFunctor.{max uA₁ uA₂, uB}

Equations

• PFunctor.instHAddPFunctor = { hAdd := PFunctor.add }

@[simp]

theorem PFunctor.hAdd_B (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) (t : P.A ⊕ Q.A) : (P + Q).B t = Sum.rec P.B Q.B t

@[simp]

theorem PFunctor.hAdd_A (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) : (P + Q).A = (P.A ⊕ Q.A)

@[simp]

theorem PFunctor.add_eq_add (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) : P.add Q = P + Q

@[implicit_reducible]

def PFunctor.prod (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) : PFunctor.{max uA₁ uA₂, max uB₁ uB₂}

The product of two polynomial functors P and Q, written as P * Q, defined as the product of the head types and the sum of the child types.

Equations

• P.prod Q = { A := P.A × Q.A, B := fun (ab : P.A × Q.A) => P.B ab.1 ⊕ Q.B ab.2 }

@[instance_reducible]

instance PFunctor.instHMulPFunctor : HMul PFunctor.{uA₁, uB₁} PFunctor.{uA₂, uB₂} PFunctor.{max uA₁ uA₂, max uB₁ uB₂}

Equations

• PFunctor.instHMulPFunctor = { hMul := PFunctor.prod }

@[simp]

theorem PFunctor.hMul_A (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) : (P * Q).A = (P.A × Q.A)

@[simp]

theorem PFunctor.hMul_B (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) (ab : P.A × Q.A) : (P * Q).B ab = (P.B ab.1 ⊕ Q.B ab.2)

@[simp]

theorem PFunctor.prod_eq_mul (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) : P.prod Q = P * Q

class PFunctor.Unary (P : PFunctor.{u_1, u_2}) : Type (max u_1 u_2)

A polynomial functor is unary if all child types have exactly one element.

• unary (a : P.A) : Unique (P.B a)

theorem PFunctor.Unary.fun_eq_const {P : PFunctor.{u_1, u_2}} {α : Sort u_3} [P.Unary] (a : P.A) (f : P.B a → α) : f = fun (x : P.B a) => f default

class PFunctor.DecidableEqChildren (P : PFunctor.{u_1, u_2}) : Type (max u_1 u_2)

A polynomial functor has children with decidable equality.

• decidableEq (a : P.A) : DecidableEq (P.B a)

@[instance_reducible]

instance PFunctor.instDecidableEqChildrenOfUnary (P : PFunctor.{u_1, u_2}) [P.Unary] : P.DecidableEqChildren

A unary polynomial functor has decidable child equality.

Equations

• P.instDecidableEqChildrenOfUnary = { decidableEq := fun (x : P.A) (x_1 x_2 : P.B x) => isTrue ⋯ }

@[reducible, inline]

abbrev PFunctor.mkUnary (A : Type u_1) : PFunctor.{u_1, 0}

Constructs a unary polynomial functor.

Equations

• PFunctor.mkUnary A = { A := A, B := fun (x : A) => Unit }

@[instance_reducible]

instance PFunctor.instUnaryLinear (A : Type uA) : (linear A).Unary

Equations

• PFunctor.instUnaryLinear A = { unary := fun (x : (PFunctor.linear A).A) => { toInhabited := instInhabitedPUnit, uniq := ⋯ } }