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.

def PFunctor.ulift (P : PFunctor.{u}) : PFunctor.{max u v}

Lift a polynomial functor to a larger universe.

Equations

• P.ulift = { A := ULift.{?u.7, ?u.8} P.A, B := fun (a : ULift.{?u.7, ?u.8} P.A) => ULift.{?u.7, ?u.8} (P.B a.down) }

def PFunctor.zero : PFunctor.{u}

The zero polynomial functor

Equations

• PFunctor.zero = { A := PEmpty.{?u.3 + 1}, B := fun (x : PEmpty.{?u.3 + 1}) => PEmpty.{?u.3 + 1} }

def PFunctor.one : PFunctor.{u}

The unit polynomial functor

Equations

• PFunctor.one = { A := PUnit.{?u.3 + 1}, B := fun (x : PUnit.{?u.3 + 1}) => PEmpty.{?u.3 + 1} }

instance PFunctor.instZero_toMathlib : Zero PFunctor.{u}

Equations

• PFunctor.instZero_toMathlib = { zero := PFunctor.zero }

instance PFunctor.instOne_toMathlib : One PFunctor.{u}

Equations

• PFunctor.instOne_toMathlib = { one := PFunctor.one }

def PFunctor.y : PFunctor.{u}

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

Equations

• PFunctor.y = { A := PUnit.{?u.3 + 1}, B := fun (x : PUnit.{?u.3 + 1}) => PUnit.{?u.3 + 1} }

instance PFunctor.instIsEmptyAZero : IsEmpty zero.A

instance PFunctor.instIsEmptyAOfNat_toMathlib : IsEmpty (A 0)

instance PFunctor.instUniqueAOne : Unique one.A

Equations

• PFunctor.instUniqueAOne = inferInstanceAs (Unique PUnit.{?u.2 + 1})

instance PFunctor.instUniqueAOfNat_toMathlib : Unique (A 1)

Equations

• PFunctor.instUniqueAOfNat_toMathlib = inferInstanceAs (Unique PUnit.{?u.2 + 1})

instance PFunctor.instUniqueAY : Unique y.A

Equations

• PFunctor.instUniqueAY = inferInstanceAs (Unique PUnit.{?u.2 + 1})

def PFunctor.monomial (A B : Type u) : PFunctor.{u}

The monomial functor P(y) = A y^B

Equations

• A y^B = { A := A, B := fun (x : A) => B }

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

The monomial functor P(y) = A y^B

Equations

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

def PFunctor.C (A : Type u) : PFunctor.{u}

The constant functor P(y) = A

Equations

• PFunctor.C A = A y^PEmpty.{?u.6 + 1}

def PFunctor.linear (A : Type u) : PFunctor.{u}

The linear functor P(y) = A y

Equations

• PFunctor.linear A = A y^PUnit.{?u.6 + 1}

def PFunctor.selfMonomial (S : Type u) : PFunctor.{u}

The self monomial functor P(y) = S y^S

Equations

• PFunctor.selfMonomial S = S y^S

def PFunctor.purePower (B : Type u) : PFunctor.{u}

The pure power functor P(y) = y^B

Equations

• PFunctor.purePower B = PUnit.{?u.6 + 1} y^B

def PFunctor.representable (B : Type u) : PFunctor.{u}

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

Equations

• PFunctor.representable = PFunctor.purePower

def PFunctor.coprod (P Q : PFunctor.{u}) : PFunctor.{u}

Coprod (sum) of polynomial functors P + Q

Equations

• P.coprod Q = { A := P.A ⊕ Q.A, B := Sum.elim P.B Q.B }

instance PFunctor.instAdd_toMathlib : Add PFunctor.{u}

Equations

• PFunctor.instAdd_toMathlib = { add := PFunctor.coprod }

def PFunctor.coprodUnit : PFunctor.{u}

Alias of PFunctor.zero.

---

The zero polynomial functor

Equations

• PFunctor.coprodUnit = PFunctor.zero

def PFunctor.sigma {I : Type v} (F : I → PFunctor.{u}) : PFunctor.{max u v}

Generalized coproduct (sigma type) of an indexed family of polynomial functors

Equations

• PFunctor.sigma F = { A := (i : I) × (F i).A, B := fun (x : (i : I) × (F i).A) => match x with | ⟨i, a⟩ => ULift.{?u.4, ?u.5} ((F i).B a) }

def PFunctor.prod (P Q : PFunctor.{u}) : PFunctor.{u}

Product of polynomial functors P * Q

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 PFunctor.instMul_toMathlib : Mul PFunctor.{u}

Equations

• PFunctor.instMul_toMathlib = { mul := PFunctor.prod }

def PFunctor.prodUnit : PFunctor.{u}

Alias of PFunctor.one.

---

The unit polynomial functor

Equations

• PFunctor.prodUnit = PFunctor.one

def PFunctor.pi {I : Type v} (F : I → PFunctor.{u}) : PFunctor.{max u v}

Generalized product (pi type) of an indexed family of polynomial functors

Equations

• PFunctor.pi F = { A := (i : I) → (F i).A, B := fun (f : (i : I) → (F i).A) => (i : I) × (F i).B (f i) }

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

Infix notation for PFunctor.comp P Q

Equations

• PFunctor.«term_◂_» = Lean.ParserDescr.trailingNode `PFunctor.«term_◂_» 80 80 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ◂ ") (Lean.ParserDescr.cat `term 81))

def PFunctor.compUnit : PFunctor.{u}

The unit for composition Y

Equations

• PFunctor.compUnit = PFunctor.y

def PFunctor.compNth (P : PFunctor.{u}) : ℕ → PFunctor.{u}

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

Equations

• P.compNth 0 = PFunctor.y
• P.compNth n.succ = P ◂ P.compNth n

instance PFunctor.instNatPow_toMathlib : NatPow PFunctor.{u}

Equations

• PFunctor.instNatPow_toMathlib = { pow := PFunctor.compNth }

def PFunctor.exp (P Q : PFunctor.{u}) : PFunctor.{u}

Exponential of polynomial functors P ^ Q

Equations

• P.exp Q = PFunctor.pi fun (a : Q.A) => P ◂ (PFunctor.y + PFunctor.C (Q.B a))

instance PFunctor.instPow_toMathlib : Pow PFunctor.{u} PFunctor.{u}

Equations

• PFunctor.instPow_toMathlib = { pow := PFunctor.exp }

def PFunctor.tensor (P Q : PFunctor.{u}) : PFunctor.{u}

Tensor or parallel product of polynomial functors

Equations

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

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

Infix notation for tensor product P ⊗ₚ Q

Equations

• PFunctor.«term_⊗ₚ_» = Lean.ParserDescr.trailingNode `PFunctor.«term_⊗ₚ_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊗ₚ ") (Lean.ParserDescr.cat `term 71))

def PFunctor.tensorUnit : PFunctor.{u}

The unit for the tensor product Y

Equations

• PFunctor.tensorUnit = PFunctor.y

class PFunctor.Fintype (P : PFunctor.{u}) : Type u

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.{u}} [inst : P.Fintype] : P.ulift.Fintype

Equations

• PFunctor.instFintypeUlift = { fintype_B := fun (a : P.ulift.A) => id inferInstance }

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

Equations

• PFunctor.instFintypeBOfFintype a = PFunctor.Fintype.fintype_B a

structure PFunctor.Lens (P Q : PFunctor.{u}) : Type u

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

• mapPos : P.A → Q.A
• mapDir : ∀ a, Q.B (mapPos a) → P.B a

• mapPos : P.A → Q.A
• mapDir (a : P.A) : Q.B (self.mapPos a) → P.B a

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

Infix notation for constructing a lens mapPos ⇆ mapDir

Equations

• PFunctor.«term_⇆_» = Lean.ParserDescr.trailingNode `PFunctor.«term_⇆_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇆ ") (Lean.ParserDescr.cat `term 25))

def PFunctor.Lens.id (P : PFunctor.{u}) : P.Lens P

The identity lens

Equations

• PFunctor.Lens.id P = (id ⇆ fun (x : P.A) (b : P.B (id x)) => b)

def PFunctor.Lens.comp {P Q R : PFunctor.{u}} (l : Q.Lens R) (l' : P.Lens Q) : P.Lens R

Composition of lenses

Equations

• l ∘ₗ l' = (l.mapPos ∘ l'.mapPos ⇆ fun (i : P.A) => l'.mapDir i ∘ l.mapDir (l'.mapPos i))

def PFunctor.Lens.«term_∘ₗ_» : Lean.TrailingParserDescr

Composition of lenses

Equations

• PFunctor.Lens.«term_∘ₗ_» = Lean.ParserDescr.trailingNode `PFunctor.Lens.«term_∘ₗ_» 75 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∘ₗ ") (Lean.ParserDescr.cat `term 76))

@[simp]

theorem PFunctor.Lens.id_comp {P Q : PFunctor.{u}} (f : P.Lens Q) : Lens.id Q ∘ₗ f = f

@[simp]

theorem PFunctor.Lens.comp_id {P Q : PFunctor.{u}} (f : P.Lens Q) : f ∘ₗ Lens.id P = f

theorem PFunctor.Lens.comp_assoc {P Q R S : PFunctor.{u}} (l : R.Lens S) (l' : Q.Lens R) (l'' : P.Lens Q) : l ∘ₗ l' ∘ₗ l'' = l ∘ₗ (l' ∘ₗ l'')

structure PFunctor.Lens.Equiv (P Q : PFunctor.{u}) : Type u

An equivalence between two polynomial functors P and Q, using lenses. This corresponds to an isomorphism in the category PFunctor with Lens morphisms.

• toLens : P.Lens Q
• invLens : Q.Lens P
• left_inv : self.invLens ∘ₗ self.toLens = Lens.id P
• right_inv : self.toLens ∘ₗ self.invLens = Lens.id Q

theorem PFunctor.Lens.Equiv.ext_iff {P Q : PFunctor.{u}} {x y : P ≃ₗ Q} : x = y ↔ x.toLens = y.toLens ∧ x.invLens = y.invLens

theorem PFunctor.Lens.Equiv.ext {P Q : PFunctor.{u}} {x y : P ≃ₗ Q} (toLens : x.toLens = y.toLens) (invLens : x.invLens = y.invLens) : x = y

def PFunctor.Lens.«term_≃ₗ_» : Lean.TrailingParserDescr

An equivalence between two polynomial functors P and Q, using lenses. This corresponds to an isomorphism in the category PFunctor with Lens morphisms.

Equations

• PFunctor.Lens.«term_≃ₗ_» = Lean.ParserDescr.trailingNode `PFunctor.Lens.«term_≃ₗ_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃ₗ ") (Lean.ParserDescr.cat `term 51))

def PFunctor.Lens.Equiv.refl (P : PFunctor.{u}) : P ≃ₗ P

Equations

• PFunctor.Lens.Equiv.refl P = { toLens := PFunctor.Lens.id P, invLens := PFunctor.Lens.id P, left_inv := ⋯, right_inv := ⋯ }

def PFunctor.Lens.Equiv.symm {P Q : PFunctor.{u}} (e : P ≃ₗ Q) : Q ≃ₗ P

Equations

• e.symm = { toLens := e.invLens, invLens := e.toLens, left_inv := ⋯, right_inv := ⋯ }

def PFunctor.Lens.Equiv.trans {P Q R : PFunctor.{u}} (e₁ : P ≃ₗ Q) (e₂ : Q ≃ₗ R) : P ≃ₗ R

Equations

• e₁.trans e₂ = { toLens := e₂.toLens ∘ₗ e₁.toLens, invLens := e₁.invLens ∘ₗ e₂.invLens, left_inv := ⋯, right_inv := ⋯ }

def PFunctor.Lens.initial {P : PFunctor.{u}} : Lens 0 P

The (unique) initial lens from the zero functor to any functor P.

Equations

• PFunctor.Lens.initial = (PEmpty.elim ⇆ fun (a : PFunctor.A 0) => PEmpty.elim a)

def PFunctor.Lens.terminal {P : PFunctor.{u}} : P.Lens 1

The (unique) terminal lens from any functor P to the unit functor 1.

Equations

• PFunctor.Lens.terminal = ((fun (x : P.A) => PUnit.unit) ⇆ fun (x : P.A) => PEmpty.elim)

def PFunctor.Lens.fromZero {P : PFunctor.{u}} : Lens 0 P

Alias of PFunctor.Lens.initial.

---

The (unique) initial lens from the zero functor to any functor P.

Equations

• @PFunctor.Lens.fromZero = @PFunctor.Lens.initial

def PFunctor.Lens.toOne {P : PFunctor.{u}} : P.Lens 1

Alias of PFunctor.Lens.terminal.

---

The (unique) terminal lens from any functor P to the unit functor 1.

Equations

• @PFunctor.Lens.toOne = @PFunctor.Lens.terminal

def PFunctor.Lens.inl {P Q : PFunctor.{u}} : P.Lens (P + Q)

Left injection lens inl : P → P + Q

Equations

• PFunctor.Lens.inl = (Sum.inl ⇆ fun (x : P.A) (d : (P + Q).B (Sum.inl x)) => d)

def PFunctor.Lens.inr {P Q : PFunctor.{u}} : Q.Lens (P + Q)

Right injection lens inr : Q → P + Q

Equations

• PFunctor.Lens.inr = (Sum.inr ⇆ fun (x : Q.A) (d : (P + Q).B (Sum.inr x)) => d)

def PFunctor.Lens.coprodPair {P Q R : PFunctor.{u}} (l₁ : P.Lens R) (l₂ : Q.Lens R) : (P + Q).Lens R

Copairing of lenses [l₁, l₂]ₗ : P + Q → R

Equations

• One or more equations did not get rendered due to their size.

def PFunctor.Lens.coprodMap {P Q R W : PFunctor.{u}} (l₁ : P.Lens R) (l₂ : Q.Lens W) : (P + Q).Lens (R + W)

Parallel application of lenses for coproduct l₁ ⊎ l₂ : P + Q → R + W

Equations

• One or more equations did not get rendered due to their size.

def PFunctor.Lens.fst {P Q : PFunctor.{u}} : (P * Q).Lens P

Projection lens fst : P * Q → P

Equations

• PFunctor.Lens.fst = (Prod.fst ⇆ fun (x : (P * Q).A) => Sum.inl)

def PFunctor.Lens.snd {P Q : PFunctor.{u}} : (P * Q).Lens Q

Projection lens snd : P * Q → Q

Equations

• PFunctor.Lens.snd = (Prod.snd ⇆ fun (x : (P * Q).A) => Sum.inr)

def PFunctor.Lens.prodPair {P Q R : PFunctor.{u}} (l₁ : P.Lens Q) (l₂ : P.Lens R) : P.Lens (Q * R)

Pairing of lenses ⟨l₁, l₂⟩ₗ : P → Q * R

Equations

• ⟨l₁,l₂⟩ₗ = ((fun (p : P.A) => (l₁.mapPos p, l₂.mapPos p)) ⇆ fun (p : P.A) => Sum.elim (l₁.mapDir p) (l₂.mapDir p))

def PFunctor.Lens.prodMap {P Q R W : PFunctor.{u}} (l₁ : P.Lens R) (l₂ : Q.Lens W) : (P * Q).Lens (R * W)

Parallel application of lenses for product l₁ ×ₗ l₂ : P * Q → R * W

Equations

• l₁ ×ₗ l₂ = ((fun (pq : (P * Q).A) => (l₁.mapPos pq.1, l₂.mapPos pq.2)) ⇆ fun (pq : (P * Q).A) => Sum.elim (Sum.inl ∘ l₁.mapDir pq.1) (Sum.inr ∘ l₂.mapDir pq.2))

def PFunctor.Lens.compMap {P Q R W : PFunctor.{u}} (l₁ : P.Lens R) (l₂ : Q.Lens W) : (P ◂ Q).Lens (R ◂ W)

Apply lenses to both sides of a composition: l₁ ◂ₗ l₂ : (P ◂ Q ⇆ R ◂ W)

Equations

• One or more equations did not get rendered due to their size.

def PFunctor.Lens.tensorMap {P Q R W : PFunctor.{u}} (l₁ : P.Lens R) (l₂ : Q.Lens W) : (P ⊗ₚ Q).Lens (R ⊗ₚ W)

Apply lenses to both sides of a tensor / parallel product: l₁ ⊗ₗ l₂ : (P ⊗ₚ Q ⇆ R ⊗ₚ W)

Equations

• One or more equations did not get rendered due to their size.

def PFunctor.Lens.tildeR {P : PFunctor.{u}} : P.Lens (P ◂ y)

Lens to introduce y on the right: P → P ◂ y

Equations

• One or more equations did not get rendered due to their size.

def PFunctor.Lens.tildeL {P : PFunctor.{u}} : P.Lens (y ◂ P)

Lens to introduce y on the left: P → y ◂ P

Equations

• One or more equations did not get rendered due to their size.

def PFunctor.Lens.invTildeR {P : PFunctor.{u}} : (P ◂ y).Lens P

Lens from P ◂ y to P

Equations

• PFunctor.Lens.invTildeR = ((fun (a : (P ◂ PFunctor.y).A) => a.fst) ⇆ fun (x : (P ◂ PFunctor.y).A) (b : P.B ((fun (a : (P ◂ PFunctor.y).A) => a.fst) x)) => ⟨b, PUnit.unit⟩)

def PFunctor.Lens.invTildeL {P : PFunctor.{u}} : (y ◂ P).Lens P

Lens from y ◂ P to P

Equations

• One or more equations did not get rendered due to their size.

def PFunctor.Lens.«term_◂ₗ_» : Lean.TrailingParserDescr

Apply lenses to both sides of a composition: l₁ ◂ₗ l₂ : (P ◂ Q ⇆ R ◂ W)

Equations

• PFunctor.Lens.«term_◂ₗ_» = Lean.ParserDescr.trailingNode `PFunctor.Lens.«term_◂ₗ_» 75 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ◂ₗ ") (Lean.ParserDescr.cat `term 76))

def PFunctor.Lens.«term_×ₗ_» : Lean.TrailingParserDescr

Parallel application of lenses for product l₁ ×ₗ l₂ : P * Q → R * W

Equations

• PFunctor.Lens.«term_×ₗ_» = Lean.ParserDescr.trailingNode `PFunctor.Lens.«term_×ₗ_» 75 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ×ₗ ") (Lean.ParserDescr.cat `term 76))

def PFunctor.Lens.«term_⊎ₗ_» : Lean.TrailingParserDescr

Parallel application of lenses for coproduct l₁ ⊎ l₂ : P + Q → R + W

Equations

• PFunctor.Lens.«term_⊎ₗ_» = Lean.ParserDescr.trailingNode `PFunctor.Lens.«term_⊎ₗ_» 75 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊎ₗ ") (Lean.ParserDescr.cat `term 76))

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

Apply lenses to both sides of a tensor / parallel product: l₁ ⊗ₗ l₂ : (P ⊗ₚ Q ⇆ R ⊗ₚ W)

Equations

• PFunctor.Lens.«term_⊗ₗ_» = Lean.ParserDescr.trailingNode `PFunctor.Lens.«term_⊗ₗ_» 75 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊗ₗ ") (Lean.ParserDescr.cat `term 76))

def PFunctor.Lens.«term[_,_]ₗ» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def PFunctor.Lens.«term⟨_,_⟩ₗ» : Lean.ParserDescr

Equations

• One or more equations did not get rendered due to their size.

def PFunctor.Lens.enclose (P : PFunctor.{u}) : Type u

The type of lenses from a polynomial functor P to y

Equations

• PFunctor.Lens.enclose P = P.Lens PFunctor.y

def PFunctor.Lens.fixState {S : Type u} : (selfMonomial S).Lens (selfMonomial S ◂ selfMonomial S)

Helper lens for speedup

Equations

• One or more equations did not get rendered due to their size.

def PFunctor.Lens.speedup {S : Type u} {P : PFunctor.{u}} (l : (selfMonomial S).Lens P) : (selfMonomial S).Lens (P ◂ P)

The speedup lens operation: Lens (S y^S) P → Lens (S y^S) (P ◂ P)

Equations

• l.speedup = l ◂ₗ l ∘ₗ PFunctor.Lens.fixState

structure PFunctor.Chart (P Q : PFunctor.{u}) : Type u

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

• mapPos : P.A → Q.A
• mapDir : ∀ a, P.B a → Q.B (mapPos a)

• mapPos : P.A → Q.A
• mapDir (a : P.A) : P.B a → Q.B (self.mapPos a)

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

Infix notation for constructing a chart mapPos ⇉ mapDir

Equations

• PFunctor.«term_⇉_» = Lean.ParserDescr.trailingNode `PFunctor.«term_⇉_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇉ ") (Lean.ParserDescr.cat `term 25))

def PFunctor.Chart.id (P : PFunctor.{u}) : P.Chart P

The identity chart

Equations

• PFunctor.Chart.id P = (id ⇉ fun (x : P.A) => id)

def PFunctor.Chart.comp {P Q R : PFunctor.{u}} (c' : Q.Chart R) (c : P.Chart Q) : P.Chart R

Composition of charts

Equations

• c' ∘c c = (c'.mapPos ∘ c.mapPos ⇉ fun (i : P.A) => c'.mapDir (c.mapPos i) ∘ c.mapDir i)

def PFunctor.Chart.«term_∘c_» : Lean.TrailingParserDescr

Infix notation for chart composition c' ∘c c

Equations

• PFunctor.Chart.«term_∘c_» = Lean.ParserDescr.trailingNode `PFunctor.Chart.«term_∘c_» 75 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∘c ") (Lean.ParserDescr.cat `term 76))

@[simp]

theorem PFunctor.Chart.id_comp {P Q : PFunctor.{u}} (f : P.Chart Q) : Chart.id Q ∘c f = f

@[simp]

theorem PFunctor.Chart.comp_id {P Q : PFunctor.{u}} (f : P.Chart Q) : f ∘c Chart.id P = f

theorem PFunctor.Chart.comp_assoc {P Q R S : PFunctor.{u}} (c : R.Chart S) (c' : Q.Chart R) (c'' : P.Chart Q) : c ∘c c' ∘c c'' = c ∘c (c' ∘c c'')

structure PFunctor.Chart.Equiv (P Q : PFunctor.{u}) : Type u

An equivalence between two polynomial functors P and Q, using charts. This corresponds to an isomorphism in the category PFunctor with Chart morphisms.

• toChart : P.Chart Q
• invChart : Q.Chart P
• left_inv : self.invChart ∘c self.toChart = Chart.id P
• right_inv : self.toChart ∘c self.invChart = Chart.id Q

theorem PFunctor.Chart.Equiv.ext {P Q : PFunctor.{u}} {x y : P ≃c Q} (toChart : x.toChart = y.toChart) (invChart : x.invChart = y.invChart) : x = y

theorem PFunctor.Chart.Equiv.ext_iff {P Q : PFunctor.{u}} {x y : P ≃c Q} : x = y ↔ x.toChart = y.toChart ∧ x.invChart = y.invChart

def PFunctor.Chart.«term_≃c_» : Lean.TrailingParserDescr

Infix notation for chart equivalence P ≃c Q

Equations

• PFunctor.Chart.«term_≃c_» = Lean.ParserDescr.trailingNode `PFunctor.Chart.«term_≃c_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃c ") (Lean.ParserDescr.cat `term 51))

def PFunctor.Chart.Equiv.refl (P : PFunctor.{u}) : P ≃c P

Equations

• PFunctor.Chart.Equiv.refl P = { toChart := PFunctor.Chart.id P, invChart := PFunctor.Chart.id P, left_inv := ⋯, right_inv := ⋯ }

def PFunctor.Chart.Equiv.symm {P Q : PFunctor.{u}} (e : P ≃c Q) : Q ≃c P

Equations

• e.symm = { toChart := e.invChart, invChart := e.toChart, left_inv := ⋯, right_inv := ⋯ }

def PFunctor.Chart.Equiv.trans {P Q R : PFunctor.{u}} (e₁ : P ≃c Q) (e₂ : Q ≃c R) : P ≃c R

Equations

• e₁.trans e₂ = { toChart := e₂.toChart ∘c e₁.toChart, invChart := e₁.invChart ∘c e₂.invChart, left_inv := ⋯, right_inv := ⋯ }

def PFunctor.Chart.initial {P : PFunctor.{u}} : Chart 0 P

The (unique) initial chart from the zero functor to any functor P.

Equations

• PFunctor.Chart.initial = (PEmpty.elim ⇉ fun (x : PFunctor.A 0) => PEmpty.elim)

def PFunctor.Chart.terminal {P : PFunctor.{u}} : P.Chart y

The (unique) terminal chart from any functor P to the functor Y.

Equations

• PFunctor.Chart.terminal = ((fun (x : P.A) => PUnit.unit) ⇉ fun (x : P.A) (x : P.B x) => PUnit.unit)

def PFunctor.Chart.fromZero {P : PFunctor.{u}} : Chart 0 P

Alias of PFunctor.Chart.initial.

---

The (unique) initial chart from the zero functor to any functor P.

Equations

• @PFunctor.Chart.fromZero = @PFunctor.Chart.initial

def PFunctor.Chart.toOne {P : PFunctor.{u}} : P.Chart y

Alias of PFunctor.Chart.terminal.

---

The (unique) terminal chart from any functor P to the functor Y.

Equations

• @PFunctor.Chart.toOne = @PFunctor.Chart.terminal

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

theorem PFunctor.Lens.ext {P Q : PFunctor.{u}} (l₁ l₂ : P.Lens Q) (h₁ : ∀ (a : P.A), l₁.mapPos a = l₂.mapPos a) (h₂ : ∀ (a : P.A), l₁.mapDir a = Eq.rec (motive := fun (x : Q.A) (h : l₂.mapPos a = x) => Q.B x → P.B a) (l₂.mapDir a) ⋯) : l₁ = l₂

theorem PFunctor.Chart.ext {P Q : PFunctor.{u}} (c₁ c₂ : P.Chart Q) (h₁ : ∀ (a : P.A), c₁.mapPos a = c₂.mapPos a) (h₂ : ∀ (a : P.A), c₁.mapDir a = Eq.rec (motive := fun (x : Q.A) (h : c₂.mapPos a = x) => P.B a → Q.B x) (c₂.mapDir a) ⋯) : c₁ = c₂

@[simp]

theorem PFunctor.C_zero : C PEmpty.{u_1 + 1} = 0

@[simp]

theorem PFunctor.C_one : C PUnit.{u_1 + 1} = 1

@[simp]

theorem PFunctor.zero_A : zero.A = PEmpty.{u_1 + 1}

@[simp]

theorem PFunctor.zero_B (a : zero.A) : zero.B a = PEmpty.{u_1 + 1}

@[simp]

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

@[simp]

theorem PFunctor.one_B (a : one.A) : one.B a = PEmpty.{u_1 + 1}

@[simp]

theorem PFunctor.y_A : y.A = PUnit.{u_1 + 1}

@[simp]

theorem PFunctor.y_B (a : y.A) : y.B a = PUnit.{u_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}

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

@[simp]

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

@[simp]

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

theorem PFunctor.y_eq_linear_pUnit : y = linear PUnit.{u_1 + 1}

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

@[simp]

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

@[simp]

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

def PFunctor.Lens.Equiv.ulift {P : PFunctor.{u}} : P.ulift ≃ₗ P

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PFunctor.Lens.coprodMap_comp_inl {P Q R W : PFunctor.{u}} (l₁ : P.Lens R) (l₂ : Q.Lens W) : l₁ ⊎ₗ l₂ ∘ₗ inl = inl ∘ₗ l₁

@[simp]

theorem PFunctor.Lens.coprodMap_comp_inr {P Q R W : PFunctor.{u}} (l₁ : P.Lens R) (l₂ : Q.Lens W) : l₁ ⊎ₗ l₂ ∘ₗ inr = inr ∘ₗ l₂

theorem PFunctor.Lens.coprodPair_comp_coprodMap {P Q R W X : PFunctor.{u}} (l₁ : P.Lens R) (l₂ : Q.Lens W) (f : R.Lens X) (g : W.Lens X) : [f,g]ₗ ∘ₗ (l₁ ⊎ₗ l₂) = [f ∘ₗ l₁,g ∘ₗ l₂]ₗ

@[simp]

theorem PFunctor.Lens.coprodPair_comp_inl {P Q R : PFunctor.{u}} (f : P.Lens R) (g : Q.Lens R) : [f,g]ₗ ∘ₗ inl = f

@[simp]

theorem PFunctor.Lens.coprodPair_comp_inr {P Q R : PFunctor.{u}} (f : P.Lens R) (g : Q.Lens R) : [f,g]ₗ ∘ₗ inr = g

theorem PFunctor.Lens.comp_inl_inr {P Q R : PFunctor.{u}} (h : (P + Q).Lens R) : [h ∘ₗ inl,h ∘ₗ inr]ₗ = h

@[simp]

theorem PFunctor.Lens.coprodMap_id {P Q : PFunctor.{u}} : Lens.id P ⊎ₗ Lens.id Q = Lens.id (P + Q)

@[simp]

theorem PFunctor.Lens.coprodPair_inl_inr {P Q : PFunctor.{u}} : [inl,inr]ₗ = Lens.id (P + Q)

def PFunctor.Lens.Equiv.coprodComm (P Q : PFunctor.{u}) : P + Q ≃ₗ Q + P

Commutativity of coproduct

Equations

• PFunctor.Lens.Equiv.coprodComm P Q = { toLens := [PFunctor.Lens.inr,PFunctor.Lens.inl]ₗ, invLens := [PFunctor.Lens.inr,PFunctor.Lens.inl]ₗ, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem PFunctor.Lens.Equiv.coprodComm_symm {P Q : PFunctor.{u}} : (coprodComm P Q).symm = coprodComm Q P

def PFunctor.Lens.Equiv.coprodAssoc {P Q R : PFunctor.{u}} : P + Q + R ≃ₗ P + (Q + R)

Associativity of coproduct

Equations

• One or more equations did not get rendered due to their size.

def PFunctor.Lens.Equiv.coprodZero {P : PFunctor.{u}} : P + 0 ≃ₗ P

Coproduct with 0 is identity (right)

Equations

• PFunctor.Lens.Equiv.coprodZero = { toLens := [PFunctor.Lens.id P,PFunctor.Lens.initial]ₗ, invLens := PFunctor.Lens.inl, left_inv := ⋯, right_inv := ⋯ }

def PFunctor.Lens.Equiv.zeroCoprod {P : PFunctor.{u}} : 0 + P ≃ₗ P

Coproduct with 0 is identity (left)

Equations

• PFunctor.Lens.Equiv.zeroCoprod = { toLens := [PFunctor.Lens.initial,PFunctor.Lens.id P]ₗ, invLens := PFunctor.Lens.inr, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem PFunctor.Lens.fst_comp_prodMap {P Q R W : PFunctor.{u}} (l₁ : P.Lens R) (l₂ : Q.Lens W) : fst ∘ₗ (l₁ ×ₗ l₂) = l₁ ∘ₗ fst

@[simp]

theorem PFunctor.Lens.snd_comp_prodMap {P Q R W : PFunctor.{u}} (l₁ : P.Lens R) (l₂ : Q.Lens W) : snd ∘ₗ (l₁ ×ₗ l₂) = l₂ ∘ₗ snd

theorem PFunctor.Lens.prodMap_comp_prodPair {P Q R W X : PFunctor.{u}} (l₁ : Q.Lens W) (l₂ : R.Lens X) (f : P.Lens Q) (g : P.Lens R) : l₁ ×ₗ l₂ ∘ₗ ⟨f,g⟩ₗ = ⟨l₁ ∘ₗ f,l₂ ∘ₗ g⟩ₗ

@[simp]

theorem PFunctor.Lens.fst_comp_prodPair {P Q R : PFunctor.{u}} (f : P.Lens Q) (g : P.Lens R) : fst ∘ₗ ⟨f,g⟩ₗ = f

@[simp]

theorem PFunctor.Lens.snd_comp_prodPair {P Q R : PFunctor.{u}} (f : P.Lens Q) (g : P.Lens R) : snd ∘ₗ ⟨f,g⟩ₗ = g

theorem PFunctor.Lens.comp_fst_snd {P Q R : PFunctor.{u}} (h : P.Lens (Q * R)) : ⟨fst ∘ₗ h,snd ∘ₗ h⟩ₗ = h

@[simp]

theorem PFunctor.Lens.prodMap_id {P Q : PFunctor.{u}} : Lens.id P ×ₗ Lens.id Q = Lens.id (P * Q)

@[simp]

theorem PFunctor.Lens.prodPair_fst_snd {P Q : PFunctor.{u}} : ⟨fst,snd⟩ₗ = Lens.id (P * Q)

def PFunctor.Lens.Equiv.prodComm (P Q : PFunctor.{u}) : P * Q ≃ₗ Q * P

Commutativity of product

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PFunctor.Lens.Equiv.prodComm_symm {P Q : PFunctor.{u}} : (prodComm P Q).symm = prodComm Q P

def PFunctor.Lens.Equiv.prodAssoc {P Q R : PFunctor.{u}} : P * Q * R ≃ₗ P * (Q * R)

Associativity of product

Equations

• One or more equations did not get rendered due to their size.

def PFunctor.Lens.Equiv.prodOne {P : PFunctor.{u}} : P * 1 ≃ₗ P

Product with 1 is identity (right)

Equations

• One or more equations did not get rendered due to their size.

def PFunctor.Lens.Equiv.oneProd {P : PFunctor.{u}} : 1 * P ≃ₗ P

Product with 1 is identity (left)

Equations

• One or more equations did not get rendered due to their size.

def PFunctor.Lens.Equiv.prodZero {P : PFunctor.{u}} : P * 0 ≃ₗ 0

Product with 0 is zero (right)

Equations

• One or more equations did not get rendered due to their size.

def PFunctor.Lens.Equiv.zeroProd {P : PFunctor.{u}} : 0 * P ≃ₗ 0

Product with 0 is zero (left)

Equations

• One or more equations did not get rendered due to their size.

def PFunctor.Lens.Equiv.prodCoprodDistrib {P Q R : PFunctor.{u}} : P * (Q + R) ≃ₗ P * Q + P * R

Left distributive law for product over coproduct

Equations

• One or more equations did not get rendered due to their size.

def PFunctor.Lens.Equiv.coprodProdDistrib {P Q R : PFunctor.{u}} : (Q + R) * P ≃ₗ Q * P + R * P

Right distributive law for coproduct over product

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PFunctor.Lens.compMap_id {P Q : PFunctor.{u}} : Lens.id P ◂ₗ Lens.id Q = Lens.id (P ◂ Q)

theorem PFunctor.Lens.compMap_comp {P Q R P' Q' R' : PFunctor.{u}} (l₁ : P.Lens P') (l₂ : Q.Lens Q') (l₁' : P'.Lens R) (l₂' : Q'.Lens R') : l₁' ∘ₗ l₁ ◂ₗ (l₂' ∘ₗ l₂) = l₁' ◂ₗ l₂' ∘ₗ (l₁ ◂ₗ l₂)

def PFunctor.Lens.Equiv.compAssoc {P Q R : PFunctor.{u}} : P ◂ Q ◂ R ≃ₗ P ◂ (Q ◂ R)

Associativity of composition

Equations

• One or more equations did not get rendered due to their size.

def PFunctor.Lens.Equiv.compY {P : PFunctor.{u}} : P ◂ y ≃ₗ P

Composition with y is identity (right)

Equations

• PFunctor.Lens.Equiv.compY = { toLens := PFunctor.Lens.invTildeR, invLens := PFunctor.Lens.tildeR, left_inv := ⋯, right_inv := ⋯ }

def PFunctor.Lens.Equiv.yComp {P : PFunctor.{u}} : y ◂ P ≃ₗ P

Composition with y is identity (left)

Equations

• PFunctor.Lens.Equiv.yComp = { toLens := PFunctor.Lens.invTildeL, invLens := PFunctor.Lens.tildeL, left_inv := ⋯, right_inv := ⋯ }

def PFunctor.Lens.Equiv.coprodCompDistrib {P Q R : PFunctor.{u}} : (Q + R) ◂ P ≃ₗ Q ◂ P + R ◂ P

Distributivity of composition over coproduct on the right

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem PFunctor.Lens.tensorMap_id {P Q : PFunctor.{u}} : Lens.id P ⊗ₗ Lens.id Q = Lens.id (P ⊗ₚ Q)

theorem PFunctor.Lens.tensorMap_comp {P Q R P' Q' R' : PFunctor.{u}} (l₁ : P.Lens P') (l₂ : Q.Lens Q') (l₁' : P'.Lens R) (l₂' : Q'.Lens R') : l₁' ∘ₗ l₁ ⊗ₗ (l₂' ∘ₗ l₂) = l₁' ⊗ₗ l₂' ∘ₗ (l₁ ⊗ₗ l₂)

def PFunctor.Lens.Equiv.tensorComm (P Q : PFunctor.{u}) : P ⊗ₚ Q ≃ₗ Q ⊗ₚ P

Commutativity of tensor product

Equations

• PFunctor.Lens.Equiv.tensorComm P Q = { toLens := Prod.swap ⇆ fun (x : (P ⊗ₚ Q).A) => Prod.swap, invLens := Prod.swap ⇆ fun (x : (Q ⊗ₚ P).A) => Prod.swap, left_inv := ⋯, right_inv := ⋯ }

def PFunctor.Lens.Equiv.tensorAssoc {P Q R : PFunctor.{u}} : P ⊗ₚ Q ⊗ₚ R ≃ₗ P ⊗ₚ (Q ⊗ₚ R)

Associativity of tensor product

Equations

• One or more equations did not get rendered due to their size.

def PFunctor.Lens.Equiv.tensorY {P : PFunctor.{u}} : P ⊗ₚ y ≃ₗ P

Tensor product with y is identity (right)

Equations

• One or more equations did not get rendered due to their size.

def PFunctor.Lens.Equiv.yTensor {P : PFunctor.{u}} : y ⊗ₚ P ≃ₗ P

Tensor product with y is identity (left)

Equations

• One or more equations did not get rendered due to their size.

def PFunctor.Lens.Equiv.zeroTensor {P : PFunctor.{u}} : 0 ⊗ₚ P ≃ₗ 0

Tensor product with 0 is zero (left)

Equations

• One or more equations did not get rendered due to their size.

def PFunctor.Lens.Equiv.tensorZero {P : PFunctor.{u}} : P ⊗ₚ 0 ≃ₗ 0

Tensor product with 0 is zero (right)

Equations

• One or more equations did not get rendered due to their size.

def PFunctor.Lens.Equiv.tensorCoprodDistrib {P Q R : PFunctor.{u}} : P ⊗ₚ (Q + R) ≃ₗ P ⊗ₚ Q + P ⊗ₚ R

Left distributivity of tensor product over coproduct

Equations

• One or more equations did not get rendered due to their size.

def PFunctor.Lens.Equiv.coprodTensorDistrib {P Q R : PFunctor.{u}} : (Q + R) ⊗ₚ P ≃ₗ Q ⊗ₚ P + R ⊗ₚ P

Right distributivity of tensor product over coproduct

Equations

• One or more equations did not get rendered due to their size.

instance PFunctor.Lens.instIsEmptyASigma {I : Type v} [IsEmpty I] {F : I → PFunctor.{u}} : IsEmpty (sigma F).A

instance PFunctor.Lens.instIsEmptyBSigma {I : Type v} [IsEmpty I] {F : I → PFunctor.{u}} {a : (sigma F).A} : IsEmpty ((sigma F).B a)

def PFunctor.Lens.sigmaEmpty {I : Type v} [IsEmpty I] {F : I → PFunctor.{u}} : sigma F ≃ₗ 0

Sigma of an empty family is the zero functor.

Equations

• One or more equations did not get rendered due to their size.

def PFunctor.Lens.sigmaUnit {F : PUnit.{u_1 + 1} → PFunctor.{u}} : sigma F ≃ₗ (F PUnit.unit).ulift

Sigma of a PUnit-indexed family is equivalent to the functor itself.

Equations

• One or more equations did not get rendered due to their size.

def PFunctor.Lens.sigmaOfUnique {I : Type v} [Unique I] {F : I → PFunctor.{u}} : sigma F ≃ₗ (F default).ulift

Sigma of an I-indexed family, where I is unique, is equivalent to the functor itself.

Equations

• One or more equations did not get rendered due to their size.

def PFunctor.Lens.prodSigmaDistrib {P : PFunctor.{u}} {I : Type u} {F : I → PFunctor.{u}} : P * sigma F ≃ₗ sigma fun (i : I) => P * F i

Left distributivity of product over sigma.

Equations

• One or more equations did not get rendered due to their size.

def PFunctor.Lens.sigmaProdDistrib {P : PFunctor.{u}} {I : Type u} {F : I → PFunctor.{u}} : sigma F * P ≃ₗ sigma fun (i : I) => F i * P

Right distributivity of product over sigma.

Equations

• One or more equations did not get rendered due to their size.

def PFunctor.Lens.tensorSigmaDistrib {P : PFunctor.{u}} {I : Type u} {F : I → PFunctor.{u}} : P ⊗ₚ sigma F ≃ₗ sigma fun (i : I) => P ⊗ₚ F i

Left distributivity of tensor product over sigma.

Equations

• One or more equations did not get rendered due to their size.

def PFunctor.Lens.sigmaTensorDistrib {P : PFunctor.{u}} {I : Type u} {F : I → PFunctor.{u}} : sigma F ⊗ₚ P ≃ₗ sigma fun (i : I) => F i ⊗ₚ P

Right distributivity of tensor product over sigma.

Equations

• One or more equations did not get rendered due to their size.

def PFunctor.Lens.piUnit {P : PFunctor.{u}} : (pi fun (x : PUnit.{u + 1}) => P) ≃ₗ P

Pi over a PUnit-indexed family is equivalent to the functor itself.

Equations

• One or more equations did not get rendered due to their size.