Charts between polynomial functors

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'')

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

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 the functor X.

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 the functor X.

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₂

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 equivalence.