Geb.Mathlib.Data.PFunctor.Slice.Basic

Imports

/-
Copyright (c) 2026 Terence Rokop. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Terence Rokop
-/
module

public import Mathlib.Data.PFunctor.Univariate.Basic

Slice polynomial functors on `Type` (constructive core)

A PFunctor is the middle map of a Gambino–Hyland polynomial diagram dom ◀ r ─ Idx ─ fst ▶ A ─ q ▶ cod. Adding r : Idx → dom and q : A → cod yields a polynomial functor Type/dom → Type/cod, defined as a restriction of the interpretation P.Obj X = Σ a, B a → X to r-compatible direction assignments, each shape carrying an output index via q. This is a dependent polynomial functor [GambinoHyland2004], [GambinoKock2013], equivalently an indexed container [AltenkirchGhaniHancockMcBrideMorris2015]; that reference presents it as a two-field (shapes, positions) record with the indices folded into dependent types, whereas here the index assignments are the explicit maps q and r. The letters q (shape-output) and r (direction-input) are this development's; the polynomial-diagram sources letter the map into cod as t and the map into dom as s.

This file is the constructive core: the structures, the compatibility predicate, the curried constructor, and the object/morphism maps with their functoriality stated as plain equalities. It names no Over and no CategoryTheory.Functor, so it is Classical.choice-free. The categorical packaging is in the sibling Slice.Functor module.

Main definitions

SliceDomPFunctor, SlicePFunctor — the structures.

SliceDomPFunctor.Compatible — the direction-compatibility predicate.

SliceDomPFunctor.ofCurried / rCurried — the curried constructor and the direction-input map in dependently-curried form.

SliceDomPFunctor.DirectionOver / Direction — the direction-input-map condition on a direction of shape a, and the fiber of rCurried a over i.

SliceDomPFunctor.Obj / map — the domain-restricted functor's object and morphism maps; map_id / map_comp its functoriality.

SlicePFunctor.obj / map — the slice functor Type/dom → Type/cod: obj is the output object's structure map into cod, map the underlying function; map_w that it lies over cod, map_id / map_comp its functoriality.

SlicePFunctor.ShapeOver / Shape — the shape-output-map condition and the fiber of q over j.

SliceDomPFunctor.prod — the product of two slice-domain polynomial functors; SliceDomPFunctor.representable — the one represented by an object of Type/dom; SliceDomPFunctor.prodSlice — the product of one with a SlicePFunctor, formed on the domain side.

SlicePFunctor.coprod — the coproduct of an indexed family of slice polynomial functors; SlicePFunctor.ofFamily — the one assembled from a cod-indexed family of SliceDomPFunctors.

Main statements

SliceDomPFunctor.compatible_iff — Compatible stated pointwise.

SliceDomPFunctor.map_fst — map fixes the shape component.

SliceDomPFunctor.map_id / map_comp — functoriality of the domain-restricted action.

SlicePFunctor.map_w — the slice morphism lies over cod.

SlicePFunctor.map_id / map_comp — functoriality of the slice functor.

Implementation notes

SliceDomPFunctor.Obj is a subtype of PFunctor.Obj; map is PFunctor.map restricted; functoriality reuses PFunctor.id_map / PFunctor.map_map. The SlicePFunctor interpretation reuses these — its carrier is SliceDomPFunctor.Obj and its map the SliceDomPFunctor map — adding only the q-assigned output index (obj) and the output-index compatibility (map_w); map_id / map_comp delegate to the domain-side ones. SliceDomPFunctor.Obj and SlicePFunctor.obj, both namespaces' map, SliceDomPFunctor.Compatible / ofCurried / rCurried / DirectionOver / Direction, and SlicePFunctor.ShapeOver / Shape are @[expose] so the wrapper and tests can unfold them across the module boundary. The fiber formers DirectionOver / Direction / ShapeOver / Shape are additionally @[implicit_reducible]: they occur inside dependent types, and type-level unification compares types at implicit transparency, so without the attribute keyed matching fails on terms whose types differ only by unfolding them.

References

[AltenkirchGhaniHancockMcBrideMorris2015]

[GambinoHyland2004]

[GambinoKock2013]

Tags

polynomial functor, dependent polynomial functor, slice category, container, PFunctor

public sectionuniverse uA uA' uB uD uC uX uX' uY uZ

A polynomial functor with a direction-input map r assigning each (shape, direction) pair (an element of PFunctor.Idx) a dom-index.

The direction-input map: each direction is assigned a dom-index.

              set_option linter.checkUnivs false instructure SliceDomPFunctor (dom : Type uD) : Type (max (uA + 1) (uB + 1) uD)
    extends PFunctor.{uA, uB} where  r : toPFunctor.Idx → dom

A SliceDomPFunctor with a shape-output map q assigning each shape a cod-index.

The shape-output map: each shape is assigned a cod-index.

              set_option linter.checkUnivs false instructure SlicePFunctor (dom : Type uD) (cod : Type uC) : Type (max (uA + 1) (uB + 1) uC uD)
    extends SliceDomPFunctor.{uA, uB, uD} dom where  q : toPFunctor.A → cod

attribute [ext] SliceDomPFunctor SlicePFunctornamespace SliceDomPFunctor

A direction assignment v : F.B a → X is compatible with a projection p : X → dom when, as functions F.B a → dom, p ∘ v equals the direction-input map restricted to shape a. Pointwise: p (v b) = r ⟨a, b⟩.

@[`@[expose]` has no effect outside a `module` fileexpose] def Compatible {dom : Type uD} (F : SliceDomPFunctor.{uA, uB} dom) {X : Type uX}
    (p : X → dom) (a : F.A) (v : F.B a → X) : Prop :=
  p ∘ v = F.r ∘ Sigma.mk a

Compatible stated pointwise.

theorem compatible_iff {dom : Type uD} (F : SliceDomPFunctor.{uA, uB} dom)
    {X : Type uX} (p : X → dom) (a : F.A) (v : F.B a → X) :
    F.Compatible p a v ↔ ∀ b, p (v b) = F.r ⟨a, b⟩ :=
  funext_iff

Build a SliceDomPFunctor from the dependently-curried direction-input map.

@[`@[expose]` has no effect outside a `module` fileexpose] def ofCurried (P : PFunctor.{uA, uB}) (dom : Type uD)
    (sc : (a : P.A) → P.B a → dom) : SliceDomPFunctor dom where
  toPFunctor := P
  r := fun x ↦ sc x.1 x.2

The direction-input map in dependently-curried form.

@[`@[expose]` has no effect outside a `module` fileexpose] def rCurried {dom : Type uD} (F : SliceDomPFunctor.{uA, uB} dom) (a : F.A)
    (b : F.B a) : dom :=
  F.r ⟨a, b⟩

The direction-input-map condition on a direction of shape a: that its image under rCurried a is i. Point-free as (· = i) ∘ rCurried a.

@[`@[expose]` has no effect outside a `module` fileexpose, implicit_reducible] def DirectionOver {dom : Type uD} (F : SliceDomPFunctor.{uA, uB} dom)
    (a : F.A) (i : dom) : F.B a → Prop :=
  (· = i) ∘ F.rCurried a

The directions of shape a lying over the base point i: the fiber of rCurried a over i.

@[`@[expose]` has no effect outside a `module` fileexpose, implicit_reducible] def Direction {dom : Type uD} (F : SliceDomPFunctor.{uA, uB} dom)
    (a : F.A) (i : dom) : Type uB :=
  Subtype (F.DirectionOver a i)

The product of two slice-domain polynomial functors: a shape is a pair of shapes, a direction at that pair is a direction of either factor at its own component, and the direction-input map is the cotuple of the factors'. This is the product of the functors Type/dom → Type they interpret, (Σ a, F.B a → X) × (Σ a', G.B a' → X) being Σ (a, a'), F.B a ⊕ G.B a' → X.

set_option linter.checkUnivs false in

@[`@[expose]` has no effect outside a `module` fileexpose] def prod {dom : Type uD} (F G : SliceDomPFunctor.{uA, uB, uD} dom) :
    SliceDomPFunctor.{uA, uB, uD} dom where
  toPFunctor := ⟨F.toPFunctor.A × G.toPFunctor.A,
    fun x ↦ F.toPFunctor.B x.1 ⊕ G.toPFunctor.B x.2⟩
  r := fun x ↦ Sum.elim (fun b ↦ F.r ⟨x.1.1, b⟩) (fun b ↦ G.r ⟨x.1.2, b⟩) x.2

The slice-domain polynomial functor represented by the object v : V → dom of Type/dom: one shape, whose directions are V, with v as the direction-input map. The functor Type/dom → Type it interprets is Hom_{Type/dom} ((V, v), -), its value at (X, p) being the assignments f : V → X with p ∘ f = v.

set_option linter.checkUnivs false in

@[`@[expose]` has no effect outside a `module` fileexpose] def representable {dom : Type uD} (V : Type uB) (v : V → dom) :
    SliceDomPFunctor.{uA, uB, uD} dom where
  toPFunctor := ⟨PUnit, fun _ ↦ V⟩
  r := fun x ↦ v x.2

The product of G with a slice polynomial functor F, formed on the domain side: prod on the SliceDomPFunctors, with F's shape-output map read off the second shape component. Under the equivalence of Type/cod with cod-indexed families (SlicePFunctor.ofFamily), this is the cod-way product of the products of G with each member of F's family; forming it here avoids the Σ over cod that transporting across the equivalence would introduce, and with it the raising of the shape universe by cod's.

set_option linter.checkUnivs false in

@[`@[expose]` has no effect outside a `module` fileexpose] def prodSlice {dom : Type uD} {cod : Type uC}
    (G : SliceDomPFunctor.{uA, uB, uD} dom) (F : SlicePFunctor.{uA, uB, uD, uC} dom cod) :
    SlicePFunctor.{uA, uB, uD, uC} dom cod where
  toSliceDomPFunctor := G.prod F.toSliceDomPFunctor
  q := fun x ↦ F.q x.2

Value of the domain-restricted functor on (X, p): the compatibility subtype of the PFunctor interpretation.

@[`@[expose]` has no effect outside a `module` fileexpose] def Obj {dom : Type uD} (F : SliceDomPFunctor.{uA, uB} dom) {X : Type uX}
    (p : X → dom) : Type (max uA uB uX) :=
  { x : F.toPFunctor.Obj X // F.Compatible p x.1 x.2 }

Action on a slice morphism f (with p' ∘ f = p): PFunctor.map f restricted to the compatibility subtype.

@[`@[expose]` has no effect outside a `module` fileexpose] def map {dom : Type uD} (F : SliceDomPFunctor.{uA, uB} dom)
    {X : Type uX} {X' : Type uX'}
    {p : X → dom} {p' : X' → dom} (f : X → X') (hf : p' ∘ f = p) :
    F.Obj p → F.Obj p' :=
  fun x ↦ ⟨F.toPFunctor.map f x.1, bydom:Type uDF:SliceDomPFunctor domX:Type uXX':Type uX'p:X → domp':X' → domf:X → X'hf:p' ∘ f = px:F.Obj p⊢ F.Compatible p' (F.map f ↑x).fst (F.map f ↑x).snd
    obtain ⟨⟨a, v⟩, hx⟩ := xdom:Type uDF:SliceDomPFunctor domX:Type uXX':Type uX'p:X → domp':X' → domf:X → X'hf:p' ∘ f = pa:F.Av:F.B a → Xhx:F.Compatible p ⟨a, v⟩.fst ⟨a, v⟩.snd⊢ F.Compatible p' (F.map f ↑⟨⟨a, v⟩, hx⟩).fst (F.map f ↑⟨⟨a, v⟩, hx⟩).snd
    change p' ∘ (f ∘ v) = F.r ∘ Sigma.mk adom:Type uDF:SliceDomPFunctor domX:Type uXX':Type uX'p:X → domp':X' → domf:X → X'hf:p' ∘ f = pa:F.Av:F.B a → Xhx:F.Compatible p ⟨a, v⟩.fst ⟨a, v⟩.snd⊢ p' ∘ f ∘ v = F.r ∘ Sigma.mk a
    rw [← Function.comp_assoc,dom:Type uDF:SliceDomPFunctor domX:Type uXX':Type uX'p:X → domp':X' → domf:X → X'hf:p' ∘ f = pa:F.Av:F.B a → Xhx:F.Compatible p ⟨a, v⟩.fst ⟨a, v⟩.snd⊢ (p' ∘ f) ∘ v = F.r ∘ Sigma.mk a hfdom:Type uDF:SliceDomPFunctor domX:Type uXX':Type uX'p:X → domp':X' → domf:X → X'hf:p' ∘ f = pa:F.Av:F.B a → Xhx:F.Compatible p ⟨a, v⟩.fst ⟨a, v⟩.snd⊢ p ∘ v = F.r ∘ Sigma.mk a]dom:Type uDF:SliceDomPFunctor domX:Type uXX':Type uX'p:X → domp':X' → domf:X → X'hf:p' ∘ f = pa:F.Av:F.B a → Xhx:F.Compatible p ⟨a, v⟩.fst ⟨a, v⟩.snd⊢ p ∘ v = F.r ∘ Sigma.mk a
    exact hxAll goals completed! 🐙⟩

map fixes the shape component.

theorem map_fst {dom : Type uD} (F : SliceDomPFunctor.{uA, uB} dom)
    {X : Type uX} {X' : Type uX'}
    {p : X → dom} {p' : X' → dom} (f : X → X') (hf : p' ∘ f = p)
    (x : F.Obj p) : (F.map f hf x).1.1 = x.1.1 := rfl

Functoriality: identity.

theorem map_id {dom : Type uD} (F : SliceDomPFunctor.{uA, uB} dom) {X : Type uX}
    (p : X → dom) : F.map id (bydom:Type uDF:SliceDomPFunctor domX:Type uXp:X → dom⊢ p ∘ id = p simpAll goals completed! 🐙) = (id : F.Obj p → F.Obj p) :=
  funext fun x ↦ Subtype.ext (F.toPFunctor.id_map x.1)

Functoriality: composition.

theorem map_comp {dom : Type uD} (F : SliceDomPFunctor.{uA, uB} dom)
    {X : Type uX} {Y : Type uY} {Z : Type uZ}
    {p : X → dom} {p' : Y → dom} {p'' : Z → dom} (f : X → Y) (g : Y → Z)
    (hf : p' ∘ f = p) (hg : p'' ∘ g = p') :
    F.map (g ∘ f) (bydom:Type uDF:SliceDomPFunctor domX:Type uXY:Type uYZ:Type uZp:X → domp':Y → domp'':Z → domf:X → Yg:Y → Zhf:p' ∘ f = phg:p'' ∘ g = p'⊢ p'' ∘ g ∘ f = p rw [← hf,dom:Type uDF:SliceDomPFunctor domX:Type uXY:Type uYZ:Type uZp:X → domp':Y → domp'':Z → domf:X → Yg:Y → Zhf:p' ∘ f = phg:p'' ∘ g = p'⊢ p'' ∘ g ∘ f = p' ∘ f ← hg,dom:Type uDF:SliceDomPFunctor domX:Type uXY:Type uYZ:Type uZp:X → domp':Y → domp'':Z → domf:X → Yg:Y → Zhf:p' ∘ f = phg:p'' ∘ g = p'⊢ p'' ∘ g ∘ f = (p'' ∘ g) ∘ f Function.comp_assocdom:Type uDF:SliceDomPFunctor domX:Type uXY:Type uYZ:Type uZp:X → domp':Y → domp'':Z → domf:X → Yg:Y → Zhf:p' ∘ f = phg:p'' ∘ g = p'⊢ p'' ∘ g ∘ f = p'' ∘ g ∘ f]All goals completed! 🐙) =
      F.map g hg ∘ F.map f hf :=
  funext fun x ↦ Subtype.ext (F.toPFunctor.map_map f g x.1).symm

end SliceDomPFunctornamespace SlicePFunctor

The slice functor's value on (X, p), as an object of Type/cod: its structure map into cod, the shape-output map applied to each shape. The carrier is the SliceDomPFunctor value F.toSliceDomPFunctor.Obj p.

@[`@[expose]` has no effect outside a `module` fileexpose] def obj {dom : Type uD} {cod : Type uC} (F : SlicePFunctor.{uA, uB, uD, uC} dom cod)
    {X : Type uX} (p : X → dom) : F.toSliceDomPFunctor.Obj p → cod :=
  fun z ↦ F.q z.1.1

The slice functor's action on a morphism: the SliceDomPFunctor morphism map underlying it.

@[`@[expose]` has no effect outside a `module` fileexpose] def map {dom : Type uD} {cod : Type uC} (F : SlicePFunctor.{uA, uB, uD, uC} dom cod)
    {X : Type uX} {X' : Type uX'} {p : X → dom} {p' : X' → dom} (f : X → X') (hf : p' ∘ f = p) :
    F.toSliceDomPFunctor.Obj p → F.toSliceDomPFunctor.Obj p' :=
  F.toSliceDomPFunctor.map f hf

map lies over cod: it commutes with the obj structure maps.

theorem map_w {dom : Type uD} {cod : Type uC} (F : SlicePFunctor.{uA, uB, uD, uC} dom cod)
    {X : Type uX} {X' : Type uX'} {p : X → dom} {p' : X' → dom} (f : X → X') (hf : p' ∘ f = p) :
    F.obj p' ∘ F.map f hf = F.obj p :=
  funext fun z ↦ congrArg F.q (F.toSliceDomPFunctor.map_fst f hf z)

Functoriality: identity.

theorem map_id {dom : Type uD} {cod : Type uC} (F : SlicePFunctor.{uA, uB, uD, uC} dom cod)
    {X : Type uX} (p : X → dom) :
    F.map id (bydom:Type uDcod:Type uCF:SlicePFunctor dom codX:Type uXp:X → dom⊢ p ∘ id = p simpAll goals completed! 🐙) = (id : F.toSliceDomPFunctor.Obj p → F.toSliceDomPFunctor.Obj p) :=
  F.toSliceDomPFunctor.map_id p

Functoriality: composition.

theorem map_comp {dom : Type uD} {cod : Type uC} (F : SlicePFunctor.{uA, uB, uD, uC} dom cod)
    {X : Type uX} {Y : Type uY} {Z : Type uZ}
    {p : X → dom} {p' : Y → dom} {p'' : Z → dom} (f : X → Y) (g : Y → Z)
    (hf : p' ∘ f = p) (hg : p'' ∘ g = p') :
    F.map (g ∘ f) (bydom:Type uDcod:Type uCF:SlicePFunctor dom codX:Type uXY:Type uYZ:Type uZp:X → domp':Y → domp'':Z → domf:X → Yg:Y → Zhf:p' ∘ f = phg:p'' ∘ g = p'⊢ p'' ∘ g ∘ f = p rw [← hf,dom:Type uDcod:Type uCF:SlicePFunctor dom codX:Type uXY:Type uYZ:Type uZp:X → domp':Y → domp'':Z → domf:X → Yg:Y → Zhf:p' ∘ f = phg:p'' ∘ g = p'⊢ p'' ∘ g ∘ f = p' ∘ f ← hg,dom:Type uDcod:Type uCF:SlicePFunctor dom codX:Type uXY:Type uYZ:Type uZp:X → domp':Y → domp'':Z → domf:X → Yg:Y → Zhf:p' ∘ f = phg:p'' ∘ g = p'⊢ p'' ∘ g ∘ f = (p'' ∘ g) ∘ f Function.comp_assocdom:Type uDcod:Type uCF:SlicePFunctor dom codX:Type uXY:Type uYZ:Type uZp:X → domp':Y → domp'':Z → domf:X → Yg:Y → Zhf:p' ∘ f = phg:p'' ∘ g = p'⊢ p'' ∘ g ∘ f = p'' ∘ g ∘ f]All goals completed! 🐙) = F.map g hg ∘ F.map f hf :=
  F.toSliceDomPFunctor.map_comp f g hf hg

The shape-output-map condition on a shape: that its image under q is j. Point-free as (· = j) ∘ q.

@[`@[expose]` has no effect outside a `module` fileexpose, implicit_reducible] def ShapeOver {dom : Type uD} {cod : Type uC}
    (F : SlicePFunctor.{uA, uB, uD, uC} dom cod) (j : cod) : F.A → Prop :=
  (· = j) ∘ F.q

The shapes lying over j: the fiber of q over j.

@[`@[expose]` has no effect outside a `module` fileexpose, implicit_reducible] def Shape {dom : Type uD} {cod : Type uC}
    (F : SlicePFunctor.{uA, uB, uD, uC} dom cod) (j : cod) : Type uA :=
  Subtype (F.ShapeOver j)

The coproduct of a family of slice polynomial functors indexed by A: shapes are the disjoint union of the summands' shapes, and the directions, the direction-input map, and the shape-output map are those of the summand a shape came from. The index type's universe is independent of the summands' shape universe, so the result's shape universe is their maximum.

set_option linter.checkUnivs false in

@[`@[expose]` has no effect outside a `module` fileexpose] def coprod {dom : Type uD} {cod : Type uC} (A : Type uA')
    (sub : A → SlicePFunctor.{uA, uB, uD, uC} dom cod) :
    SlicePFunctor.{max uA' uA, uB, uD, uC} dom cod where
  toPFunctor := ⟨Σ a, (sub a).toPFunctor.A, fun x ↦ (sub x.1).toPFunctor.B x.2⟩
  r := fun x ↦ (sub x.1.1).r ⟨x.1.2, x.2⟩
  q := fun x ↦ (sub x.1).q x.2

The slice polynomial functor Type/dom → Type/cod assembled from a cod-indexed family of functors Type/dom → Type, transporting the family across the equivalence of Type/cod with cod-indexed families: a shape is a shape of one member tagged with that member's index, and the shape-output map returns the tag. It is the coproduct of the members, each given the constant shape-output map at its own index, so the shape universe rises by cod's.

set_option linter.checkUnivs false in

@[`@[expose]` has no effect outside a `module` fileexpose] def ofFamily {dom : Type uD} {cod : Type uC}
    (fam : cod → SliceDomPFunctor.{uA, uB, uD} dom) :
    SlicePFunctor.{max uC uA, uB, uD, uC} dom cod :=
  coprod cod fun o ↦ { toSliceDomPFunctor := fam o, q := fun _ ↦ o }

end SlicePFunctor

Slice polynomial functors on Type (constructive core)

Main definitions

Main statements

Implementation notes

References

Tags

Slice polynomial functors on `Type` (constructive core)