Polynomial Functors, Lens, and Charts

This file defines polynomial functors, lenses, and charts. The goal is to provide basic definitions, with their properties and categories defined in later files.

instance PFunctor.instZero_toMathlib : Zero PFunctor.{uA, uB}

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

instance PFunctor.instOne_toMathlib : One PFunctor.{uA, uB}

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

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

The monomial functor, also written P(X) = A X^ B, has A as its head type and the constant family B_a = B as the child type for each each shape a : A .

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

The monomial functor, also written P(X) = A X^ B, has A as its head type and the constant family B_a = B as the child type for each each shape a : A .

def PFunctor.C (A : Type uA) : PFunctor.{uA, uB}

The constant polynomial functor P(X) = A X^ PEmpty

def PFunctor.X : PFunctor.{uA, uB}

The variable (or indeterminate) polynomial functor X, defined as P(X) = PUnit X^ PUnit.

This is the identity with respect to tensor product and composition (up to equivalence).

def PFunctor.linear (A : Type uA) : PFunctor.{uA, uB}

The linear polynomial functor P(X) = A X

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

The self monomial polynomial functor P(X) = S X^ S

def PFunctor.purePower (B : Type uB) : PFunctor.{uA, uB}

The pure power polynomial functor P(X) = X^ B

def PFunctor.representable (B : Type uB) : PFunctor.{uA, uB}

A polynomial functor is representable if it is equivalent to X^A for some type A.

instance PFunctor.instIsEmptyAOfNat_toMathlib : IsEmpty (A 0)

instance PFunctor.instUniqueAOfNat_toMathlib : Unique (A 1)

instance PFunctor.instIsEmptyBOfNat_toMathlib {a : A 1} : IsEmpty (B 1 a)

instance PFunctor.instIsEmptyBC {α : Type u_1} (a : α) : IsEmpty ((C α).B a)

instance PFunctor.instUniqueAX : Unique X.A

instance PFunctor.instUniqueBX {a : X.A} : Unique (X.B a)

instance PFunctor.instUniqueBLinear {α : Type u_1} (a : α) : Unique ((linear α).B a)

instance PFunctor.instUniqueAPurePower {β : Type u_1} : Unique (purePower β).A

@[simp]

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

@[simp]

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

@[simp]

theorem PFunctor.C_A (A : Type u) : (C A).A = A

@[simp]

theorem PFunctor.C_B (A : Type u) (a : (C A).A) : (C A).B a = PEmpty.{u_1 + 1}

@[simp]

theorem PFunctor.X_A : X.A = PUnit.{u_1 + 1}

@[simp]

theorem PFunctor.X_B (a : X.A) : X.B a = PUnit.{u_2 + 1}

@[simp]

theorem PFunctor.linear_A (A : Type u) : (linear A).A = A

@[simp]

theorem PFunctor.linear_B (A : Type u) (a : (linear A).A) : (linear A).B a = PUnit.{u_1 + 1}

@[simp]

theorem PFunctor.selfMonomial_A (S : Type u) : (selfMonomial S).A = S

@[simp]

theorem PFunctor.selfMonomial_B (S : Type u) (a : (selfMonomial S).A) : (selfMonomial S).B a = S

@[simp]

theorem PFunctor.selfMonomial_unit : selfMonomial PUnit.{u_1 + 1} = X

@[simp]

theorem PFunctor.purePower_A (B : Type u) : (purePower B).A = PUnit.{u_1 + 1}

@[simp]

theorem PFunctor.purePower_B (B : Type u) (a : (purePower B).A) : (purePower B).B a = B

@[simp]

theorem PFunctor.purePower_unit : purePower PUnit.{u_1 + 1} = X

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

The sum (coproduct) of two polynomial functors P and Q, written as P + Q.

Defined as the sum of the head types and the sum case analysis for the child types.

Note: requires the B universe levels to be the same.

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

Addition of polynomial functors, defined as the sum construction.

instance PFunctor.instAdd_toMathlib : Add PFunctor.{uA, uB}

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

Alias of PFunctor.sum.

---

The sum (coproduct) of two polynomial functors P and Q, written as P + Q.

Defined as the sum of the head types and the sum case analysis for the child types.

Note: requires the B universe levels to be the same.

def PFunctor.sigma {I : Type v} (F : I → PFunctor.{uA, uB}) : PFunctor.{max uA v, uB}

The generalized sum (sigma type) of an indexed family of polynomial functors.

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.

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

Multiplication of polynomial functors, defined as the product construction.

instance PFunctor.instMul_toMathlib : Mul PFunctor.{uA, uB}

def PFunctor.pi {I : Type v} (F : I → PFunctor.{uA, uB}) : PFunctor.{max uA v, max uB v}

The generalized product (pi type) of an indexed family of polynomial functors.

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

The tensor (also called parallel or Dirichlet) product of two polynomial functors P and Q.

Defined as the product of the head types and the product of the child types.

def PFunctor.«term_⊗_» : Lean.TrailingParserDescr

Infix notation for tensor product P ⊗ Q

def PFunctor.tensorUnit : PFunctor.{uA, uB}

The unit for the tensor product Y

def PFunctor.«term_◃_» : Lean.TrailingParserDescr

Infix notation for PFunctor.comp P Q

def PFunctor.compUnit : PFunctor.{uA, uB}

The unit for composition Y

def PFunctor.compNth (P : PFunctor.{uA, uB}) : ℕ → PFunctor.{max uA uB, uB}

Repeated composition P ◃ P ◃ ... ◃ P (n times).

instance PFunctor.instNatPow_toMathlib : NatPow PFunctor.{max uA uB, uB}

def PFunctor.ulift (P : PFunctor.{uA, uB}) : PFunctor.{max uA vA, max uB vB}

Lift a polynomial functor P to a pair of larger universes.

def PFunctor.exp (P Q : PFunctor.{uA, uB}) : PFunctor.{max uA uB, max uA uB}

Exponential of polynomial functors P ^ Q

instance PFunctor.instHPow_toMathlib : HPow PFunctor.{uA, uB} PFunctor.{uA, uB} PFunctor.{max uA uB, max uA uB}

class PFunctor.Fintype (P : PFunctor.{uA, uB}) : Type (max uA uB)

A polynomial functor is finitely branching if each of its branches is a finite type.

• fintype_B (a : P.A) : Fintype (P.B a)

instance PFunctor.instFintypeUlift {P : PFunctor.{uA, uB}} [inst : P.Fintype] : P.ulift.Fintype

instance PFunctor.instFintypeBOfFintype {P : PFunctor.{uA, uB}} [inst : P.Fintype] (a : P.A) : Fintype (P.B a)

structure PFunctor.Equiv (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) : Type (max (max (max uA₁ uA₂) uB₁) uB₂)

An equivalence between two polynomial functors P and Q, written P ≃ₚ Q, is given by an equivalence of the A types and an equivalence between the B types for each a : A.

• equivA : P.A ≃ Q.A

  An equivalence between the A types

• equivB (a : P.A) : P.B a ≃ Q.B (self.equivA a)

  An equivalence between the B types for each a : A

theorem PFunctor.Equiv.ext {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {x y : P.Equiv Q} (equivA : x.equivA = y.equivA) (equivB : x.equivB ≍ y.equivB) : x = y

theorem PFunctor.Equiv.ext_iff {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {x y : P.Equiv Q} : x = y ↔ x.equivA = y.equivA ∧ x.equivB ≍ y.equivB

def PFunctor.«term_≃ₚ_» : Lean.TrailingParserDescr

An equivalence between two polynomial functors P and Q, written P ≃ₚ Q, is given by an equivalence of the A types and an equivalence between the B types for each a : A.

def PFunctor.Equiv.refl (P : PFunctor.{uA, uB}) : P.Equiv P

The identity equivalence between a polynomial functor P and itself.

def PFunctor.Equiv.symm {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (E : P.Equiv Q) : Q.Equiv P

The inverse of an equivalence between polynomial functors.

def PFunctor.Equiv.trans {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} (E : P.Equiv Q) (F : Q.Equiv R) : P.Equiv R

The composition of two equivalences between polynomial functors.

def PFunctor.Equiv.cast {P Q : PFunctor.{uA, uB}} (hA : P.A = Q.A) (hB : ∀ (a : P.A), P.B a = Q.B (_root_.cast hA a)) : P.Equiv Q

Equivalence between two polynomial functors P and Q that are equal.

@[simp]

theorem PFunctor.Equiv.symm_symm {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (e : P.Equiv Q) : e.symm.symm = e

@[simp]

theorem PFunctor.Equiv.symm_comp_self {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (e : P.Equiv Q) : ⇑e.symm.equivA ∘ ⇑e.equivA = id

structure PFunctor.Lens (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) : Type (max (max (max uA₁ uA₂) uB₁) uB₂)

A lens between two polynomial functors P and Q is a pair of a function:

• toFunA : P.A → Q.A
• toFunB : ∀ a, Q.B (toFunA a) → P.B a

• toFunA : P.A → Q.A
• toFunB (a : P.A) : Q.B (self.toFunA a) → P.B a

def PFunctor.«term_⇆_» : Lean.TrailingParserDescr

Infix notation for constructing a lens toFunA ⇆ toFunB

structure PFunctor.Chart (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) : Type (max (max (max uA₁ uA₂) uB₁) uB₂)

A chart between two polynomial functors P and Q is a pair of a function:

• toFunA : P.A → Q.A
• toFunB : ∀ a, P.B a → Q.B (toFunA a)

• toFunA : P.A → Q.A
• toFunB (a : P.A) : P.B a → Q.B (self.toFunA a)

def PFunctor.«term_⇉_» : Lean.TrailingParserDescr

Infix notation for constructing a chart toFunA ⇉ toFunB

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

theorem PFunctor.X_eq_linear_pUnit : X = linear PUnit.{u_2 + 1}

theorem PFunctor.X_eq_purePower_pUnit : X = purePower PUnit.{u_1 + 1}

@[simp]

theorem PFunctor.ulift_A {P : PFunctor.{uA, uB}} : P.ulift.A = ULift.{u_1, uA} P.A

@[simp]

theorem PFunctor.ulift_B {P : PFunctor.{uA, uB}} {a : P.A} : P.ulift.B { down := a } = ULift.{u_1, uB} (P.B a)