Charts between polynomial functors

A Chart P Q is a pair (toFunA, toFunB) where

• toFunA : P.A → Q.A is a forward map on positions, and
• toFunB : ∀ a, P.B a → Q.B (toFunA a) is a forward map on directions.

While lenses make Poly into a 2-category whose categorical product is * (positions ×, directions Σ), charts make Poly into a different category that is isomorphic to the arrow category Set^→ (squares B → A → B' → A'). A consequence is that the chart category has a different monoidal structure from the lens category.

Comparison with Lens

	Lens	Chart
Coproduct	+	+ (same)
Product	* (positions ×, directions ⊕)	⊗ (positions ×, directions ×)
Terminal	1 (positions = 1, no directions)	X = y (positions = 1, dir = 1)
Composition	compMap is natural	compMap is not natural
Sigma	sigmaExists, sigmaMap	sigmaExists, sigmaMap
Pi	piForall, piMap	only piMap

The operations missing from charts (compMap, piForall, projections from *, sigmaForall) all require contravariance and so are intrinsically lens-side. What charts do have, they have cleanly: + is the coproduct with inl/inr/sumPair, and ⊗ is the categorical product with fst/snd/tensorPair.

Layout

This file mirrors ToMathlib/PFunctor/Lens/Basic.lean for ease of cross-reference. Each section header that overlaps with Lens is named identically; the chart-specific sections (Tensor for the categorical product, Prod for the polynomial product) are documented inline.

Downstream consumers

Interface.Hom, Interface.Hom.mapPacket, and the boundary-side composition operators are intentionally thin wrappers around this file. New downstream operators on packet/index transport (e.g. parallel composition, sum routing) should be defined as wrappers, not re-implemented.

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

Identity and composition

def PFunctor.Chart.id (P : PFunctor.{uA, uB}) : P.Chart P

The identity chart

def PFunctor.Chart.comp {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} (c' : Q.Chart R) (c : P.Chart Q) : P.Chart R

Composition of charts

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

Infix notation for chart composition c' ∘c c

@[simp]

theorem PFunctor.Chart.id_comp {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (f : P.Chart Q) : Chart.id Q ∘c f = f

@[simp]

theorem PFunctor.Chart.comp_id {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (f : P.Chart Q) : f ∘c Chart.id P = f

theorem PFunctor.Chart.comp_assoc {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} {S : PFunctor.{uA₄, uB₄}} (c : R.Chart S) (c' : Q.Chart R) (c'' : P.Chart Q) : c ∘c c' ∘c c'' = c ∘c (c' ∘c c'')

Equivalences

structure PFunctor.Chart.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, 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_iff {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {x y : P ≃c Q} : x = y ↔ x.toChart = y.toChart ∧ x.invChart = y.invChart

theorem PFunctor.Chart.Equiv.ext {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {x y : P ≃c Q} (toChart : x.toChart = y.toChart) (invChart : x.invChart = y.invChart) : x = y

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

Infix notation for chart equivalence P ≃c Q

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

def PFunctor.Chart.Equiv.symm {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (e : P ≃c Q) : Q ≃c P

def PFunctor.Chart.Equiv.trans {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} (e₁ : P ≃c Q) (e₂ : Q ≃c R) : P ≃c R

Initial and terminal

def PFunctor.Chart.initial {P : PFunctor.{uA, uB}} : Chart 0 P

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

def PFunctor.Chart.terminal {P : PFunctor.{uA, uB}} : P.Chart X

The (unique) terminal chart from any functor P to X = y.

X is the terminal object of the chart category — a single position with a single direction — corresponding to the identity arrow 1 → 1 in Set^→. This differs from the lens-side terminal 1 (positions 1, no directions).

def PFunctor.Chart.fromZero {P : PFunctor.{uA, uB}} : Chart 0 P

Alias of PFunctor.Chart.initial.

---

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

def PFunctor.Chart.toOne {P : PFunctor.{uA, uB}} : P.Chart X

Alias of PFunctor.Chart.terminal.

---

The (unique) terminal chart from any functor P to X = y.

X is the terminal object of the chart category — a single position with a single direction — corresponding to the identity arrow 1 → 1 in Set^→. This differs from the lens-side terminal 1 (positions 1, no directions).

Coproduct (+)

+ is the coproduct in the chart category (as it is in the lens category). The two inclusions inl/inr plus the copairing sumPair realise the universal property of +. The parallel-sum sumMap is then a derived construction.

def PFunctor.Chart.inl {P : PFunctor.{uA₁, uB}} {Q : PFunctor.{uA₂, uB}} : P.Chart (P + Q)

Left injection chart inl : P → P + Q.

def PFunctor.Chart.inr {P : PFunctor.{uA₁, uB}} {Q : PFunctor.{uA₂, uB}} : Q.Chart (P + Q)

Right injection chart inr : Q → P + Q.

def PFunctor.Chart.sumPair {P : PFunctor.{uA₁, uB}} {Q : PFunctor.{uA₂, uB}} {R : PFunctor.{uA₃, uB₃}} (c₁ : P.Chart R) (c₂ : Q.Chart R) : (P + Q).Chart R

Copairing of charts [c₁, c₂]c : P + Q → R.

def PFunctor.Chart.sumMap {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₁}} {R : PFunctor.{uA₃, uB₃}} {W : PFunctor.{uA₄, uB₃}} (c₁ : P.Chart R) (c₂ : Q.Chart W) : (P + Q).Chart (R + W)

Parallel application of charts for coproduct c₁ ⊎c c₂ : P + Q → R + W.

Tensor (⊗) — the chart category's binary product

⊗ is the categorical binary product in the chart category, with projections fst/snd and pairing tensorPair. (For lenses, the categorical product is *, not ⊗.)

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

Projection chart fst : P ⊗ Q → P.

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

Projection chart snd : P ⊗ Q → Q.

def PFunctor.Chart.tensorPair {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} (c₁ : P.Chart Q) (c₂ : P.Chart R) : P.Chart (Q.tensor R)

Pairing of charts ⟨c₁, c₂⟩c : P → Q ⊗ R.

def PFunctor.Chart.tensorMap {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} {W : PFunctor.{uA₄, uB₄}} (c₁ : P.Chart R) (c₂ : Q.Chart W) : (P.tensor Q).Chart (R.tensor W)

Parallel application of charts for tensor c₁ ⊗c c₂ : P ⊗ Q → R ⊗ W.

Polynomial product (*) — not the chart categorical product

The polynomial product * is not the categorical product in the chart category: there is no natural chart P * Q → P because the source has direction type P.B a₁ ⊕ Q.B a₂ and we cannot project a Q.B a₂ to a P.B a₁. We provide only the parallel-map operation.

For categorical projections / pairing, use ⊗ instead.

def PFunctor.Chart.prodMap {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} {W : PFunctor.{uA₄, uB₄}} (c₁ : P.Chart R) (c₂ : Q.Chart W) : (P * Q).Chart (R * W)

Parallel application of charts for polynomial product c₁ ×c c₂ : P * Q → R * W.

Indexed colimits and limits

The chart category has Sigma-eliminations (sigmaExists/sigmaMap) but only the parametric Pi-map (piMap); piForall is intrinsically a lens-side construction because it requires "choosing an index" in the chart direction, which has no canonical choice in Set^→.

def PFunctor.Chart.sigmaExists {I : Type v} {F : I → PFunctor.{uA₁, uB₁}} {R : PFunctor.{uA₂, uB₂}} (c : (i : I) → (F i).Chart R) : (sigma F).Chart R

Dependent copairing of charts over sigma: (Σ i, F i) → R.

def PFunctor.Chart.sigmaMap {I : Type v} {F : I → PFunctor.{uA₁, uB₁}} {G : I → PFunctor.{uA₂, uB₂}} (c : (i : I) → (F i).Chart (G i)) : (sigma F).Chart (sigma G)

Pointwise mapping of charts over sigma.

def PFunctor.Chart.piMap {I : Type v} {F : I → PFunctor.{uA₁, uB₁}} {G : I → PFunctor.{uA₂, uB₂}} (c : (i : I) → (F i).Chart (G i)) : (pi F).Chart (pi G)

Pointwise mapping of charts over pi.

Action on indices

A chart φ : P → Q acts on Idx P = Σ a : P.A, P.B a by sending ⟨a, b⟩ ↦ ⟨φ.toFunA a, φ.toFunB a b⟩. This is the underlying function on positions; Trace.mapChart (in ToMathlib.PFunctor.Trace) uses it to push event traces along charts.

def PFunctor.Chart.mapIdx {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (φ : P.Chart Q) (i : P.Idx) : Q.Idx

Push an Idx P along a chart P → Q to an Idx Q.

@[simp]

theorem PFunctor.Chart.mapIdx_id {P : PFunctor.{uA₁, uB₁}} (i : P.Idx) : (Chart.id P).mapIdx i = i

@[simp]

theorem PFunctor.Chart.mapIdx_comp {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} (g : Q.Chart R) (f : P.Chart Q) (i : P.Idx) : (g ∘c f).mapIdx i = g.mapIdx (f.mapIdx i)

Special charts

def PFunctor.Chart.enclose (P : PFunctor.{uA, uB}) : Type (max uA uA₁ uB uB₁)

The type of charts from a polynomial functor P to X.

A chart P → X is equivalent to a function (a : P.A) → P.B a → PUnit, i.e. a boundary valuation that picks out a single direction at every position. Analogous to Lens.enclose.

Notations for binary operations

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

Parallel application of charts for coproduct c₁ ⊎c c₂ : P + Q → R + W.

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

Parallel application of charts for tensor c₁ ⊗c c₂ : P ⊗ Q → R ⊗ W.

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

Parallel application of charts for polynomial product c₁ ×c c₂ : P * Q → R * W.

def PFunctor.Chart.«term[_,_]c» : Lean.ParserDescr

def PFunctor.Chart.«term⟨_,_⟩c» : Lean.ParserDescr

Coproduct coherence

@[simp]

theorem PFunctor.Chart.sumMap_comp_inl {P : PFunctor.{uA₁, uB}} {Q : PFunctor.{uA₂, uB}} {R : PFunctor.{uA₃, uB₃}} {W : PFunctor.{uA₄, uB₃}} (c₁ : P.Chart R) (c₂ : Q.Chart W) : c₁ ⊎c c₂ ∘c inl = inl ∘c c₁

@[simp]

theorem PFunctor.Chart.sumMap_comp_inr {P : PFunctor.{uA₁, uB}} {Q : PFunctor.{uA₂, uB}} {R : PFunctor.{uA₃, uB₃}} {W : PFunctor.{uA₄, uB₃}} (c₁ : P.Chart R) (c₂ : Q.Chart W) : c₁ ⊎c c₂ ∘c inr = inr ∘c c₂

theorem PFunctor.Chart.sumPair_comp_sumMap {P : PFunctor.{uA₁, uB}} {Q : PFunctor.{uA₂, uB}} {R : PFunctor.{uA₃, uB₃}} {W : PFunctor.{uA₄, uB₃}} {S : PFunctor.{uA₅, uB₅}} (c₁ : P.Chart R) (c₂ : Q.Chart W) (f : R.Chart S) (g : W.Chart S) : [f,g]c ∘c (c₁ ⊎c c₂) = [f ∘c c₁,g ∘c c₂]c

@[simp]

theorem PFunctor.Chart.sumPair_comp_inl {P : PFunctor.{uA₁, uB}} {Q : PFunctor.{uA₂, uB}} {R : PFunctor.{uA₃, uB₃}} (f : P.Chart R) (g : Q.Chart R) : [f,g]c ∘c inl = f

@[simp]

theorem PFunctor.Chart.sumPair_comp_inr {P : PFunctor.{uA₁, uB}} {Q : PFunctor.{uA₂, uB}} {R : PFunctor.{uA₃, uB₃}} (f : P.Chart R) (g : Q.Chart R) : [f,g]c ∘c inr = g

theorem PFunctor.Chart.comp_inl_inr {P : PFunctor.{uA₁, uB}} {Q : PFunctor.{uA₂, uB}} {R : PFunctor.{uA₃, uB₃}} (h : (P + Q).Chart R) : [h ∘c inl,h ∘c inr]c = h

@[simp]

theorem PFunctor.Chart.sumMap_id {P : PFunctor.{uA₁, uB}} {Q : PFunctor.{uA₂, uB}} : Chart.id P ⊎c Chart.id Q = Chart.id (P + Q)

@[simp]

theorem PFunctor.Chart.sumPair_inl_inr {P : PFunctor.{uA₁, uB}} {Q : PFunctor.{uA₂, uB}} : [inl,inr]c = Chart.id (P + Q)

theorem PFunctor.Chart.sumMap_comp_sumMap {P : PFunctor.{uA₁, uB}} {Q : PFunctor.{uA₂, uB}} {R : PFunctor.{uA₃, uB₃}} {W : PFunctor.{uA₄, uB₃}} {S : PFunctor.{uA₅, uB₅}} {T : PFunctor.{uA₆, uB₅}} (c₁ : P.Chart R) (c₂ : Q.Chart W) (c₁' : R.Chart S) (c₂' : W.Chart T) : c₁' ⊎c c₂' ∘c (c₁ ⊎c c₂) = c₁' ∘c c₁ ⊎c (c₂' ∘c c₂)

def PFunctor.Chart.Equiv.sumComm (P : PFunctor.{uA₁, uB}) (Q : PFunctor.{uA₂, uB}) : P + Q ≃c Q + P

Commutativity of coproduct

@[simp]

theorem PFunctor.Chart.Equiv.sumComm_symm {P : PFunctor.{uA₁, uB}} {Q : PFunctor.{uA₂, uB}} : (sumComm P Q).symm = sumComm Q P

def PFunctor.Chart.Equiv.sumAssoc {P : PFunctor.{uA₁, uB}} {Q : PFunctor.{uA₂, uB}} {R : PFunctor.{uA₃, uB}} : P + Q + R ≃c P + (Q + R)

Associativity of coproduct

def PFunctor.Chart.Equiv.sumZero {P : PFunctor.{uA₁, uB}} : P + 0 ≃c P

Coproduct with 0 is identity (right)

def PFunctor.Chart.Equiv.zeroSum {P : PFunctor.{uA₁, uB}} : 0 + P ≃c P

Coproduct with 0 is identity (left)

def PFunctor.Chart.Equiv.sumCongr {P : PFunctor.{uA₁, uB}} {Q : PFunctor.{uA₂, uB}} {P' : PFunctor.{uA₃, uB}} {Q' : PFunctor.{uA₄, uB}} (e₁ : P ≃c P') (e₂ : Q ≃c Q') : P + Q ≃c P' + Q'

Coproduct preserves equivalences: P ≃c P' → Q ≃c Q' → P + Q ≃c P' + Q'.

Tensor coherence

@[simp]

theorem PFunctor.Chart.fst_comp_tensorMap {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} {W : PFunctor.{uA₄, uB₄}} (c₁ : P.Chart R) (c₂ : Q.Chart W) : fst ∘c (c₁ ⊗c c₂) = c₁ ∘c fst

@[simp]

theorem PFunctor.Chart.snd_comp_tensorMap {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} {W : PFunctor.{uA₄, uB₄}} (c₁ : P.Chart R) (c₂ : Q.Chart W) : snd ∘c (c₁ ⊗c c₂) = c₂ ∘c snd

theorem PFunctor.Chart.tensorMap_comp_tensorPair {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} {W : PFunctor.{uA₄, uB₄}} {S : PFunctor.{uA₅, uB₅}} (c₁ : Q.Chart W) (c₂ : R.Chart S) (f : P.Chart Q) (g : P.Chart R) : c₁ ⊗c c₂ ∘c ⟨f,g⟩c = ⟨c₁ ∘c f,c₂ ∘c g⟩c

@[simp]

theorem PFunctor.Chart.fst_comp_tensorPair {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} (f : P.Chart Q) (g : P.Chart R) : fst ∘c ⟨f,g⟩c = f

@[simp]

theorem PFunctor.Chart.snd_comp_tensorPair {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} (f : P.Chart Q) (g : P.Chart R) : snd ∘c ⟨f,g⟩c = g

theorem PFunctor.Chart.comp_fst_snd {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} (h : P.Chart (Q.tensor R)) : ⟨fst ∘c h,snd ∘c h⟩c = h

@[simp]

theorem PFunctor.Chart.tensorMap_id {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} : Chart.id P ⊗c Chart.id Q = Chart.id (P.tensor Q)

theorem PFunctor.Chart.tensorMap_comp {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} {W : PFunctor.{uA₄, uB₄}} {P' : PFunctor.{uA₅, uB₅}} {Q' : PFunctor.{uA₆, uB₆}} (c₁ : P.Chart P') (c₂ : Q.Chart Q') (c₁' : P'.Chart R) (c₂' : Q'.Chart W) : c₁' ∘c c₁ ⊗c (c₂' ∘c c₂) = c₁' ⊗c c₂' ∘c (c₁ ⊗c c₂)

theorem PFunctor.Chart.tensorMap_comp_tensorMap {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} {W : PFunctor.{uA₄, uB₄}} {P' : PFunctor.{uA₅, uB₅}} {Q' : PFunctor.{uA₆, uB₆}} (c₁ : P.Chart R) (c₂ : Q.Chart W) (c₁' : R.Chart P') (c₂' : W.Chart Q') : c₁' ⊗c c₂' ∘c (c₁ ⊗c c₂) = c₁' ∘c c₁ ⊗c (c₂' ∘c c₂)

@[simp]

theorem PFunctor.Chart.tensorPair_fst_snd {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} : ⟨fst,snd⟩c = Chart.id (P.tensor Q)

def PFunctor.Chart.Equiv.tensorComm (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) : P.tensor Q ≃c Q.tensor P

Commutativity of tensor product

@[simp]

theorem PFunctor.Chart.Equiv.tensorComm_symm {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} : (tensorComm P Q).symm = tensorComm Q P

def PFunctor.Chart.Equiv.tensorAssoc {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} : (P.tensor Q).tensor R ≃c P.tensor (Q.tensor R)

Associativity of tensor product

def PFunctor.Chart.Equiv.tensorX {P : PFunctor.{uA₁, uB₁}} : P.tensor X ≃c P

Tensor product with X is identity (right)

def PFunctor.Chart.Equiv.xTensor {P : PFunctor.{uA₁, uB₁}} : X.tensor P ≃c P

Tensor product with X is identity (left)

def PFunctor.Chart.Equiv.zeroTensor {P : PFunctor.{uA₁, uB₁}} : tensor 0 P ≃c 0

Tensor product with 0 is zero (left)

def PFunctor.Chart.Equiv.tensorZero {P : PFunctor.{uA₁, uB₁}} : P.tensor 0 ≃c 0

Tensor product with 0 is zero (right)

def PFunctor.Chart.Equiv.tensorCongr {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {P' : PFunctor.{uA₃, uB₃}} {Q' : PFunctor.{uA₄, uB₄}} (e₁ : P ≃c P') (e₂ : Q ≃c Q') : P.tensor Q ≃c P'.tensor Q'

Tensor product preserves equivalences: P ≃c P' → Q ≃c Q' → P ⊗ Q ≃c P' ⊗ Q'.

def PFunctor.Chart.Equiv.tensorSumDistrib {P : PFunctor.{uA₁, uB₁}} {Q R : PFunctor.{uA₂, uB₂}} : P.tensor (Q + R) ≃c P.tensor Q + P.tensor R

Left distributivity of tensor product over coproduct.

P ⊗ (Q + R) ≃c (P ⊗ Q) + (P ⊗ R).

def PFunctor.Chart.Equiv.sumTensorDistrib {P : PFunctor.{uA₁, uB₁}} {Q R : PFunctor.{uA₂, uB₂}} : (Q + R).tensor P ≃c Q.tensor P + R.tensor P

Right distributivity of tensor product over coproduct.

(Q + R) ⊗ P ≃c (Q ⊗ P) + (R ⊗ P).

Polynomial-product coherence

Even though * is not the categorical product in the chart category, it is still a functor and admits coherent equivalences (commutativity, associativity, units, zeros, congruence, distributivity over +). These mirror the PFunctor.Equiv.prod* lemmas.

@[simp]

theorem PFunctor.Chart.prodMap_id {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} : Chart.id P ×c Chart.id Q = Chart.id (P * Q)

theorem PFunctor.Chart.prodMap_comp_prodMap {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} {W : PFunctor.{uA₄, uB₄}} {S : PFunctor.{uA₅, uB₅}} {T : PFunctor.{uA₆, uB₆}} (c₁ : P.Chart R) (c₂ : Q.Chart W) (c₁' : R.Chart S) (c₂' : W.Chart T) : c₁' ×c c₂' ∘c (c₁ ×c c₂) = c₁' ∘c c₁ ×c (c₂' ∘c c₂)

def PFunctor.Chart.Equiv.prodCongr {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {P' : PFunctor.{uA₃, uB₃}} {Q' : PFunctor.{uA₄, uB₄}} (e₁ : P ≃c P') (e₂ : Q ≃c Q') : P * Q ≃c P' * Q'

Polynomial-product preserves equivalences: P ≃c P' → Q ≃c Q' → P * Q ≃c P' * Q'.

def PFunctor.Chart.Equiv.prodComm (P : PFunctor.{uA₁, uB₁}) (Q : PFunctor.{uA₂, uB₂}) : P * Q ≃c Q * P

Commutativity of the polynomial product.

def PFunctor.Chart.Equiv.prodAssoc {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} {R : PFunctor.{uA₃, uB₃}} : P * Q * R ≃c P * (Q * R)

Associativity of the polynomial product.

def PFunctor.Chart.Equiv.prodZero {P : PFunctor.{uA₁, uB₁}} : P * 0 ≃c 0

Polynomial-product with 0 is 0 (right).

def PFunctor.Chart.Equiv.zeroProd {P : PFunctor.{uA₁, uB₁}} : 0 * P ≃c 0

Polynomial-product with 0 is 0 (left).

def PFunctor.Chart.Equiv.prodSumDistrib {P : PFunctor.{uA₁, uB₁}} {Q R : PFunctor.{uA₂, uB₂}} : P * (Q + R) ≃c P * Q + P * R

Left distributivity of polynomial product over coproduct.

P * (Q + R) ≃c (P * Q) + (P * R).

def PFunctor.Chart.Equiv.sumProdDistrib {P : PFunctor.{uA₁, uB₁}} {Q R : PFunctor.{uA₂, uB₂}} : (Q + R) * P ≃c Q * P + R * P

Right distributivity of polynomial product over coproduct.

(Q + R) * P ≃c (Q * P) + (R * P).

ULift

def PFunctor.Chart.Equiv.ulift {P : PFunctor.{uA, uB}} : P.ulift ≃c P

ULift equivalence for charts.

def PFunctor.Equiv.toChart {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (e : P.Equiv Q) : P.Chart Q

Convert an equivalence between two polynomial functors P and Q to a chart.

Bridge PFunctor.Equiv → Chart.Equiv

Every polynomial-functor equivalence yields a chart equivalence: the forward chart uses e.equivA / e.equivB, and the inverse chart uses their symmetric counterparts. The proofs of left_inv / right_inv need the cast machinery from forward_equivB_roundtrip / reverse_equivB_roundtrip because e.symm.equivA (e.equivA a) and a are only propositionally equal.

This is the chart analogue of Equiv.toLensEquiv and is the standard way to derive sigma / distributivity equivalences from their PFunctor.Equiv counterparts.

@[simp]

theorem PFunctor.Equiv.symm_toChart_comp_toChart {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (e : P.Equiv Q) : e.symm.toChart ∘c e.toChart = Chart.id P

@[simp]

theorem PFunctor.Equiv.toChart_comp_symm_toChart {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (e : P.Equiv Q) : e.toChart ∘c e.symm.toChart = Chart.id Q

def PFunctor.Equiv.toChartEquiv {P : PFunctor.{uA₁, uB₁}} {Q : PFunctor.{uA₂, uB₂}} (e : P.Equiv Q) : P ≃c Q

Convert an equivalence between two polynomial functors to a chart equivalence.

Chart-side analogue of Equiv.toLensEquiv. Together with Chart.Equiv.refl, symm, and trans, this establishes a faithful functor PFunctor.Equiv → Chart.Equiv.

Sigma equivalences

These are derived from PFunctor.Equiv.toChartEquiv applied to the corresponding PFunctor.Equiv constructions. They mirror the PFunctor.Lens.Equiv.sigma* family.

def PFunctor.Chart.Equiv.sigmaEmpty {I : Type v} [IsEmpty I] {F : I → PFunctor.{uA, uB}} : sigma F ≃c 0

Sigma of an empty family is the zero functor.

def PFunctor.Chart.Equiv.sigmaUnit {F : PUnit.{u_1 + 1} → PFunctor.{uA, uB}} : sigma F ≃c (F PUnit.unit).ulift

Sigma of a PUnit-indexed family is equivalent to the functor itself (up to ulift).

def PFunctor.Chart.Equiv.sigmaOfUnique {I : Type v} [Unique I] {F : I → PFunctor.{uA, uB}} : sigma F ≃c (F default).ulift

Sigma of a unique-indexed family is equivalent to the default fiber (up to ulift).

def PFunctor.Chart.Equiv.prodSigmaDistrib {I : Type v} {P : PFunctor.{uA₁, uB₁}} {F : I → PFunctor.{uA₂, uB₂}} : P * sigma F ≃c sigma fun (i : I) => P * F i

Left distributivity of polynomial product over sigma.

def PFunctor.Chart.Equiv.sigmaProdDistrib {I : Type v} {P : PFunctor.{uA₁, uB₁}} {F : I → PFunctor.{uA₂, uB₂}} : sigma F * P ≃c sigma fun (i : I) => F i * P

Right distributivity of polynomial product over sigma.

def PFunctor.Chart.Equiv.tensorSigmaDistrib {I : Type v} {P : PFunctor.{uA₁, uB₁}} {F : I → PFunctor.{uA₂, uB₂}} : P.tensor (sigma F) ≃c sigma fun (i : I) => P.tensor (F i)

Left distributivity of tensor product over sigma.

def PFunctor.Chart.Equiv.sigmaTensorDistrib {I : Type v} {P : PFunctor.{uA₂, uB₂}} {F : I → PFunctor.{uA₁, uB₁}} : (sigma F).tensor P ≃c sigma fun (i : I) => (F i).tensor P

Right distributivity of tensor product over sigma.

Pi equivalences

piMap lives in the operations section, but unlike lenses, charts admit no piForall (Pi-elimination requires direction-contravariance). What we get cleanly here is piUnit and piZero.

def PFunctor.Chart.Equiv.piUnit {P : PFunctor.{uA, uB}} : (pi fun (x : PUnit.{u_1 + 1}) => P) ≃c P

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

def PFunctor.Chart.Equiv.piZero {I : Type v} [Inhabited I] {F : I → PFunctor.{uA, uB}} (F_zero : ∀ (i : I), F i = 0) : pi F ≃c 0

Pi of a family of zero functors over an inhabited type is the zero functor.