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.

dt: this file is getting long and should maybe be split up more.

@[implicit_reducible]

instance PFunctor.instZero_polyFun : 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)

@[implicit_reducible]

instance PFunctor.instOne_polyFun : 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.y : PFunctor.{uA, uB}

The variable y polynomial functor. This is the unit for composition.

instance PFunctor.instIsEmptyAOfNat_polyFun : IsEmpty (A 0)

@[implicit_reducible]

instance PFunctor.instUniqueAOfNatOne : Unique (A 1)

@[implicit_reducible]

instance PFunctor.instUniqueAY : Unique y.A

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.

def PFunctor.ofFn {A : Type uA₁} (B : A → Type uB) : PFunctor.{uA₁, uB}

Construct a polynomial functor from just a function B, with A derived implicitly.

@[simp]

theorem PFunctor.ofFn_A {A : Type uA₁} (B : A → Type uB) : (ofFn B).A = A

@[simp]

theorem PFunctor.ofFn_B {A : Type uA₁} (B : A → Type uB) (a : A) : (ofFn B).B a = B a

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

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

@[implicit_reducible]

instance PFunctor.instUniqueAX : Unique X.A

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

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.

@[implicit_reducible]

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

Addition of polynomial functors, defined as the sum construction.

@[implicit_reducible]

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

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

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.

@[implicit_reducible]

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

Multiplication of polynomial functors, defined as the product construction.

@[implicit_reducible]

instance PFunctor.instMul_polyFun : 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).

@[implicit_reducible]

instance PFunctor.instNatPow_polyFun : 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

@[implicit_reducible]

instance PFunctor.instHPow_polyFun : 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)

@[implicit_reducible]

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

@[implicit_reducible]

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

@[implicit_reducible]

instance PFunctor.instFintypeOfNat : PFunctor.Fintype 0

@[implicit_reducible]

instance PFunctor.instFintypeOfNat_1 : PFunctor.Fintype 1

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

• inhabited_B (a : P.A) : Inhabited (P.B a)

@[implicit_reducible]

instance PFunctor.instInhabitedUlift {P : PFunctor.{uA, uB}} [inst : P.Inhabited] : P.ulift.Inhabited

@[implicit_reducible]

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

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

• decidableEq_A : DecidableEq P.A
• decidableEq_B (a : P.A) : DecidableEq (P.B a)

@[implicit_reducible]

instance PFunctor.instDecidableEqAOfDecidableEq {P : PFunctor.{uA, uB}} [inst : P.DecidableEq] : DecidableEq P.A

@[implicit_reducible]

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

@[implicit_reducible]

instance PFunctor.instDecidableEqUlift {P : PFunctor.{uA, uB}} [inst : P.DecidableEq] : P.ulift.DecidableEq

@[implicit_reducible]

instance PFunctor.instDecidableEqOfNat : PFunctor.DecidableEq 0

@[implicit_reducible]

instance PFunctor.instDecidableEqOfNat_1 : PFunctor.DecidableEq 1

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

PFunctor where the output type is constant over an arbitrary input type.

@[implicit_reducible]

instance PFunctor.instFintypeOfConstOfFintype (A : Type uA) (B : Type uB) [hB : Fintype B] : (ofConst A B).Fintype

@[implicit_reducible]

instance PFunctor.instDecidableEqOfConstOfDecidableEq (A : Type uA) (B : Type uB) [DecidableEq A] [DecidableEq B] : (ofConst A B).DecidableEq

@[implicit_reducible]

instance PFunctor.instInhabitedOfConstOfInhabited (A : Type uA) (B : Type uB) [Inhabited B] : (ofConst A B).Inhabited

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_iff {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {x y : P.Equiv Q} : x = y ↔ x.equivA = y.equivA ∧ x.equivB ≍ y.equivB

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

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_comp_self {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (e : P.Equiv Q) : ⇑e.symm.equivA ∘ ⇑e.equivA = id

theorem PFunctor.Equiv.eqRec_id_apply {α : Sort u} {β : α → Sort v} {a1 a0 : α} (h : a1 = a0) (x : β a0) : Eq.rec (motive := fun (y : α) (x : a1 = y) => β y → β a1) id h x = _root_.cast ⋯ x

Rewrite a dependent Eq.rec with identity to a cast on the argument.

theorem PFunctor.Equiv.equivB_symm_apply_of_eq {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (e : P.Equiv Q) {a a' : P.A} (ha : e.equivA a = e.equivA a') (b : P.B a') : (e.equivB a).symm ((_root_.Equiv.cast ⋯).symm ((e.equivB a') b)) = _root_.cast ⋯ b

Cast-normalization helper for equivB under equal equivA images.

theorem PFunctor.Equiv.symm_equivB_symm_apply_of_eq {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (e : P.Equiv Q) {a a' : Q.A} (ha : e.symm.equivA a = e.symm.equivA a') (b : Q.B a') : (e.symm.equivB a).symm ((_root_.Equiv.cast ⋯).symm ((e.symm.equivB a') b)) = _root_.cast ⋯ b

Cast-normalization helper for symm.equivB under equal symm.equivA images.

theorem PFunctor.Equiv.equivB_symm_apply {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (e : P.Equiv Q) (a : P.A) (b : P.B (e.equivA.symm (e.equivA a))) : (e.equivB a).symm ((e.symm.equivB (e.equivA a)).symm b) = _root_.cast ⋯ b

Specialized cast-normalization for e followed by e.symm.

theorem PFunctor.Equiv.symm_equivB_symm_apply {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (e : P.Equiv Q) (a : Q.A) (b : Q.B (e.equivA (e.equivA.symm a))) : (e.symm.equivB a).symm ((e.equivB (e.equivA.symm a)).symm b) = _root_.cast ⋯ b

Specialized cast-normalization for e.symm followed by e.

theorem PFunctor.Equiv.forward_equivB_roundtrip {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (e : P.Equiv Q) (a : P.A) (b : P.B a) : (e.symm.equivB (e.equivA a)) ((e.equivB a) b) = _root_.cast ⋯ b

Forward roundtrip: applying equivB then symm.equivB gives a cast.

theorem PFunctor.Equiv.reverse_equivB_roundtrip {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (e : P.Equiv Q) (a : Q.A) (b : Q.B a) : (e.equivB (e.equivA.symm a)) ((e.symm.equivB a) b) = _root_.cast ⋯ b

Reverse roundtrip: applying symm.equivB then equivB gives a cast.

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)