Node decorations as displayed families over PFunctor.FreeM

A Decoration Γ s is the canonical displayed family over a free P-tree s whose leaves carry no data and whose internal nodes carry one value of Γ a and recursively decorate every child.

It is the displayed family obtained from the shape

leaf  := fun _ => PUnit
node a child := Γ a × ((b : P.B a) → child b)

Equivalently, it is Displayed D s where D = Decoration.shape Γ. Because Decoration is literally a Displayed at a chosen Shape, every Displayed operation specializes immediately to Decoration: Displayed.map becomes Decoration.map, Displayed.Hom-actions become decoration morphisms, and so on. The lemmas in this file are exactly those specializations.

Decoration.Over is the dependent (displayed) variant: at each node, an extra fiber of type F a γ over the base decoration's value γ : Γ a, recursively over each child. It is Displayed.Over at the corresponding OverShape.

The bridge equivOver packages a decoration of an extended context Γ.extend A as a base decoration plus one Over layer.

This is the FreeM-generic substrate; protocol-flavored aliases (e.g. for Spec) live downstream.

def PFunctor.FreeM.Displayed.Decoration.shape {P : PFunctor.{u, v}} {α : Type w} (Γ : P.A → Type w₂) : Shape P α

Displayed-family shape for node-local metadata over a polynomial tree.

@[reducible, inline]

abbrev PFunctor.FreeM.Displayed.Decoration {P : PFunctor.{u, v}} {α : Type w} (Γ : P.A → Type w₂) : P.FreeM α → Type (max v w₂)

Node-local metadata over an arbitrary polynomial free tree.

At a control node a : P.A, the decoration stores one value of type Γ a and recursively decorates every abstract control continuation b : P.B a.

def PFunctor.FreeM.Displayed.Decoration.overShape {P : PFunctor.{u, v}} {α : Type w} (Γ : P.A → Type w₂) (F : (a : P.A) → Γ a → Type w₃) : OverShape (shape Γ)

Displayed-family shape for a dependent layer over a polynomial decoration.

At a node with base metadata γ : Γ a, the over-layer stores data in F a γ and recursively stores over-data over each decorated child.

@[reducible, inline]

abbrev PFunctor.FreeM.Displayed.Decoration.Over {P : PFunctor.{u, v}} {α : Type w} (Γ : P.A → Type w₂) (F : (a : P.A) → Γ a → Type w₃) (s : P.FreeM α) (d : Decoration Γ s) : Type (max v w₃)

Dependent node-local metadata over an existing polynomial decoration.

def PFunctor.FreeM.Displayed.Decoration.Context.extend {P : PFunctor.{u, v}} (Γ : P.A → Type w₂) (A : (a : P.A) → Γ a → Type w₃) : P.A → Type (max w₂ w₃)

Extend a node metadata family by one dependent field.

def PFunctor.FreeM.Displayed.Decoration.Context.extendMap {P : PFunctor.{u, v}} {Γ : P.A → Type w₂} {Δ : P.A → Type w₃} {A : (a : P.A) → Γ a → Type w₄} {B : (a : P.A) → Δ a → Type w₅} (f : (a : P.A) → Γ a → Δ a) (g : (a : P.A) → (γ : Γ a) → A a γ → B a (f a γ)) (a : P.A) : extend Γ A a → extend Δ B a

Map one extended node metadata family to another.

def PFunctor.FreeM.Displayed.Decoration.empty {P : PFunctor.{u, v}} {α : Type w} (s : P.FreeM α) : Decoration (fun (x : P.A) => PUnit.{(max v w₂) + 1}) s

The unique decoration by the everywhere-PUnit node metadata family.

def PFunctor.FreeM.Displayed.Decoration.mapLocalHom {P : PFunctor.{u, v}} {α : Type w} {Γ : P.A → Type w₂} {Δ : P.A → Type w₃} (f : (a : P.A) → Γ a → Δ a) : LocalHom (shape Γ) (shape Δ)

Constructor-local displayed morphism induced by a nodewise metadata map.

def PFunctor.FreeM.Displayed.Decoration.map {P : PFunctor.{u, v}} {α : Type w} {Γ : P.A → Type w₂} {Δ : P.A → Type w₃} (f : (a : P.A) → Γ a → Δ a) (s : P.FreeM α) : Decoration Γ s → Decoration Δ s

Natural transformation between node-local decorations, applied recursively.

@[simp]

theorem PFunctor.FreeM.Displayed.Decoration.map_pure {P : PFunctor.{u, v}} {α : Type w} {Γ : P.A → Type w₂} {Δ : P.A → Type w₃} (f : (a : P.A) → Γ a → Δ a) (x : α) (d : Decoration Γ (pure x)) : map f (pure x) d = PUnit.unit

@[simp]

theorem PFunctor.FreeM.Displayed.Decoration.map_roll {P : PFunctor.{u, v}} {α : Type w} {Γ : P.A → Type w₂} {Δ : P.A → Type w₃} (f : (a : P.A) → Γ a → Δ a) (a : P.A) (rest : P.B a → P.FreeM α) (d : Decoration Γ (roll a rest)) : map f (roll a rest) d = (f a d.1, fun (b : P.B a) => map f (rest b) (d.2 b))

@[simp]

theorem PFunctor.FreeM.Displayed.Decoration.map_id {P : PFunctor.{u, v}} {α : Type w} {Γ : P.A → Type w₂} (s : P.FreeM α) (d : Decoration Γ s) : map (fun (x : P.A) (γ : Γ x) => γ) s d = d

theorem PFunctor.FreeM.Displayed.Decoration.map_comp {P : PFunctor.{u, v}} {α : Type w} {Γ : P.A → Type w₂} {Δ : P.A → Type w₃} {Λ : P.A → Type w₄} (g : (a : P.A) → Δ a → Λ a) (f : (a : P.A) → Γ a → Δ a) (s : P.FreeM α) (d : Decoration Γ s) : map g s (map f s d) = map (fun (a : P.A) => g a ∘ f a) s d

def PFunctor.FreeM.Displayed.Decoration.Over.mapLocalHom {P : PFunctor.{u, v}} {α : Type w} {Γ : P.A → Type w₂} {F : (a : P.A) → Γ a → Type w₃} {G : (a : P.A) → Γ a → Type w₄} (f : (a : P.A) → (γ : Γ a) → F a γ → G a γ) : Over.FiberLocalHom (overShape Γ F) (overShape Γ G)

Constructor-local displayed-over morphism induced by a fiberwise map.

def PFunctor.FreeM.Displayed.Decoration.Over.map {P : PFunctor.{u, v}} {α : Type w} {Γ : P.A → Type w₂} {F : (a : P.A) → Γ a → Type w₃} {G : (a : P.A) → Γ a → Type w₄} (f : (a : P.A) → (γ : Γ a) → F a γ → G a γ) (s : P.FreeM α) (d : Decoration Γ s) : Over Γ F s d → Over Γ G s d

Fiberwise map between dependent decoration families over the same decoration.

@[simp]

theorem PFunctor.FreeM.Displayed.Decoration.Over.map_id {P : PFunctor.{u, v}} {α : Type w} {Γ : P.A → Type w₂} {F : (a : P.A) → Γ a → Type w₃} (s : P.FreeM α) (d : Decoration Γ s) (r : Over Γ F s d) : map (fun (x : P.A) (x_1 : Γ x) (x_2 : F x x_1) => x_2) s d r = r

theorem PFunctor.FreeM.Displayed.Decoration.Over.map_comp {P : PFunctor.{u, v}} {α : Type w} {Γ : P.A → Type w₂} {F : (a : P.A) → Γ a → Type w₃} {G : (a : P.A) → Γ a → Type w₄} {H : (a : P.A) → Γ a → Type w₅} (g : (a : P.A) → (γ : Γ a) → G a γ → H a γ) (f : (a : P.A) → (γ : Γ a) → F a γ → G a γ) (s : P.FreeM α) (d : Decoration Γ s) (r : Over Γ F s d) : map g s d (map f s d r) = map (fun (a : P.A) (γ : Γ a) => g a γ ∘ f a γ) s d r

def PFunctor.FreeM.Displayed.Decoration.Over.mapBaseLocalHom {P : PFunctor.{u, v}} {α : Type w} {Γ : P.A → Type w₂} {Δ : P.A → Type w₃} {A : (a : P.A) → Γ a → Type w₄} {B : (a : P.A) → Δ a → Type w₅} (f : (a : P.A) → Γ a → Δ a) (g : (a : P.A) → (γ : Γ a) → A a γ → B a (f a γ)) : Over.LocalHom (Decoration.mapLocalHom f) (overShape Γ A) (overShape Δ B)

Constructor-local displayed-over morphism induced by a map of base metadata and a compatible map of the dependent over-layer.

def PFunctor.FreeM.Displayed.Decoration.Over.mapBase {P : PFunctor.{u, v}} {α : Type w} {Γ : P.A → Type w₂} {Δ : P.A → Type w₃} {A : (a : P.A) → Γ a → Type w₄} {B : (a : P.A) → Δ a → Type w₅} (f : (a : P.A) → Γ a → Δ a) (g : (a : P.A) → (γ : Γ a) → A a γ → B a (f a γ)) (s : P.FreeM α) (d : Decoration Γ s) : Over Γ A s d → Over Δ B s (Decoration.map f s d)

Transport a dependent decoration across a nodewise map of base decorations.

theorem PFunctor.FreeM.Displayed.Decoration.Over.mapBase_id {P : PFunctor.{u, v}} {α : Type w} {Γ : P.A → Type w₂} {A : (a : P.A) → Γ a → Type w₃} (s : P.FreeM α) (d : Decoration Γ s) (r : Over Γ A s d) : mapBase (fun (x : P.A) (γ : Γ x) => γ) (fun (x : P.A) (x_1 : Γ x) (x_2 : A x x_1) => x_2) s d r ≍ r

theorem PFunctor.FreeM.Displayed.Decoration.Over.mapBase_comp {P : PFunctor.{u, v}} {α : Type w} {Γ : P.A → Type w₂} {Δ : P.A → Type w₃} {Λ : P.A → Type w₄} {A : (a : P.A) → Γ a → Type w₅} {B : (a : P.A) → Δ a → Type w₅} {C : (a : P.A) → Λ a → Type w₅} (f : (a : P.A) → Γ a → Δ a) (g : (a : P.A) → Δ a → Λ a) (fOver : (a : P.A) → (γ : Γ a) → A a γ → B a (f a γ)) (gOver : (a : P.A) → (δ : Δ a) → B a δ → C a (g a δ)) (s : P.FreeM α) (d : Decoration Γ s) (r : Over Γ A s d) : mapBase g gOver s (Decoration.map f s d) (mapBase f fOver s d r) ≍ mapBase (fun (a : P.A) => g a ∘ f a) (fun (a : P.A) (γ : Γ a) => gOver a (f a γ) ∘ fOver a γ) s d r

def PFunctor.FreeM.Displayed.Decoration.ofOver {P : PFunctor.{u, v}} {α : Type w} {Γ : P.A → Type w₂} {A : (a : P.A) → Γ a → Type w₃} (s : P.FreeM α) (d : Decoration Γ s) : Over Γ A s d → Decoration (Context.extend Γ A) s

Pack a base decoration and one dependent Over layer into a decoration of the extended metadata family.

theorem PFunctor.FreeM.Displayed.Decoration.map_ofOver {P : PFunctor.{u, v}} {α : Type w} {Γ : P.A → Type w₂} {Δ : P.A → Type w₃} {A : (a : P.A) → Γ a → Type w₄} {B : (a : P.A) → Δ a → Type w₅} (f : (a : P.A) → Γ a → Δ a) (g : (a : P.A) → (γ : Γ a) → A a γ → B a (f a γ)) (s : P.FreeM α) (d : Decoration Γ s) (r : Over Γ A s d) : map (Context.extendMap f g) s (ofOver s d r) = ofOver s (map f s d) (Over.mapBase f g s d r)

def PFunctor.FreeM.Displayed.Decoration.toOver {P : PFunctor.{u, v}} {α : Type w} {Γ : P.A → Type w₂} {A : (a : P.A) → Γ a → Type w₃} (s : P.FreeM α) : Decoration (Context.extend Γ A) s → (d : Decoration Γ s) × Over Γ A s d

Unpack a decoration of an extended metadata family into its base decoration and dependent over-layer.

@[simp]

theorem PFunctor.FreeM.Displayed.Decoration.toOver_ofOver {P : PFunctor.{u, v}} {α : Type w} {Γ : P.A → Type w₂} {A : (a : P.A) → Γ a → Type w₃} (s : P.FreeM α) (d : Decoration Γ s) (r : Over Γ A s d) : toOver s (ofOver s d r) = ⟨d, r⟩

@[simp]

theorem PFunctor.FreeM.Displayed.Decoration.ofOver_toOver {P : PFunctor.{u, v}} {α : Type w} {Γ : P.A → Type w₂} {A : (a : P.A) → Γ a → Type w₃} (s : P.FreeM α) (d : Decoration (Context.extend Γ A) s) : ofOver s (toOver s d).fst (toOver s d).snd = d

def PFunctor.FreeM.Displayed.Decoration.equivOver {P : PFunctor.{u, v}} {α : Type w} {Γ : P.A → Type w₂} (A : (a : P.A) → Γ a → Type w₃) (s : P.FreeM α) : Decoration (Context.extend Γ A) s ≃ (d : Decoration Γ s) × Over Γ A s d

Equivalence between decorating by an extended metadata family and pairing a base decoration with one dependent over-layer.