Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: what kind of thing is a Chart between polynomial functors?

André Muricy Santos (Apr 24 2023 at 10:37):

I'm working on a formalization of Poly for my master's thesis with agda-categories and cubical agda and decided to write a little isomorphism from polynomials to functors and lenses to natural transformations, which are both pretty trivial but then I thought... is a chart also a NT? it is a map between functors after all... But it seems like it's not. So what kind of thing are charts? :thinking:

F-resp : {p : Polynomial} {A B : Set} {f g : A → B} {x : p ⦅ A ⦆ } → f ≡ g → applyFn p f x ≡ applyFn p g x --
F-resp {x = posApp , dirApp} pr = λ i → posApp , (pr i) ∘  dirApp

conv : {A B : Set} {f g : A → B} → ({x : A} → f x ≡p g x) → f ≡ g
conv p = funExt λ x → ptoc $ p

asEndo : (p : Polynomial) → Functor (Sets zero) (Sets zero)
asEndo p = record
    { F₀ = λ x → p ⦅ x ⦆
    ; F₁ = λ f → applyFn p f
    ; identity = Eq.refl
    ; homomorphism = Eq.refl
    ; F-resp-≈ = λ {_} {_} {f} {g} proof → ctop (F-resp {f = f} {g = g} (conv proof))
    }

asNatTransArr : {p q : Polynomial} → Lens p q → NaturalTransformation (asEndo p) (asEndo q)
asNatTransArr (f ⇆ f♯) = record {
    η = λ { X (posP , dirP) → f posP , dirP ∘ f♯ posP } ;
    commute = λ f₁ → Eq.refl ;
    sym-commute = λ f₁ → Eq.refl
    }

asNatTransChart : {p q : Polynomial} → Chart p q → NaturalTransformation (asEndo p) (asEndo q)
asNatTransChart (f ⇉ f♭) = record {
    η = λ { X (posP , dirP) → {!   !}} ;
    commute = {!   !} ;
    sym-commute = {!   !}
  }

Jules Hedges (Apr 24 2023 at 10:44):

This is a very good question, and I'd like to know the answer too... I'd bet nobody knows

Morgan Rogers (he/him) (Apr 24 2023 at 10:44):

What is (the definition of) a chart between polynomial functors?

Jules Hedges (Apr 24 2023 at 10:45):

I think the "chart" terminology exists exclusively in the categorical systems theory book by David Jaz Myers (which itself is pretty hard to find, it's only on Github)

Jules Hedges (Apr 24 2023 at 10:46):

It means a morphism in the fibrewise opposite of categories of lenses, ie. "like a lens except the backwards pass also goes forwards"

Jules Hedges (Apr 24 2023 at 10:46):

There's the isomorphism of categories $\mathbf{Poly} (\mathcal C) \cong \int_{X : \mathcal C} (\mathcal C / X)^\mathrm{op}$, so the question is, what happens if you remove the op from the right hand side

Jules Hedges (Apr 24 2023 at 10:48):

Since objects can still be seen as polynomial functors, the answer is that it's some kind of morphism between polynomial functors that's different to natural transformations

André Muricy Santos (Apr 24 2023 at 10:50):

I've only seen DJM talk about charts too, but the CSS book doesn't go into what kind of categorical thing it is. The definition is this:

record Chart (p q : Polynomial) : Set where
    constructor _⇉_
    field
        mapPos : position p → position q
        mapDir : (i : position p) → direction p i → direction q (mapPos i)

∘c : {p q r : Polynomial} → Chart q r → Chart p q → Chart p r
∘c (f ⇉ f♭) (g ⇉ g♭) = (f ∘ g) ⇉ λ i x → f♭ (g i) (g♭ i x)

idChart : {p : Polynomial} → Chart p p
idChart = id ⇉ λ _ → id

defs for Poly and Lens for completeness:

record Polynomial : Set₁ where
    constructor mkpoly
    field
        position : Set
        direction : position → Set
open Polynomial public

record Lens (from to : Polynomial) : Set where
    constructor _⇆_
    open Polynomial
    field
        mapPosition : position from → position to
        mapDirection : (fromPos : position from) → direction to (mapPosition fromPos) → direction from fromPos
open Lens public

André Muricy Santos (Apr 24 2023 at 10:53):

Jules Hedges said:

There's the isomorphism of categories $\mathbf{Poly} (\mathcal C) \cong \int_{X : \mathcal C} (\mathcal C / X)^\mathrm{op}$, so the question is, what happens if you remove the op from the right hand side

Jules, what do the symbols on the right mean? I recognize the integral as an indexed category except the X:C would be on top. and then C / X is slice?

Jules Hedges (Apr 24 2023 at 10:56):

Yes, this is the Grothendieck construction of the indexed category given by the opposite of slice categories

Reid Barton (Apr 24 2023 at 11:19):

Is this answer wrong, too trivial, or otherwise unwanted?
A polynomial functor is an object of the arrow category of Set; a chart is a morphism of that category.

Reid Barton (Apr 24 2023 at 11:21):

I'm just looking at the Agda definition and substituting the names Polynomial -> family, position -> base, direction -> fiber, etc.

André Muricy Santos (Apr 24 2023 at 11:22):

I don't know much about arrow categories, but don't the morphisms correspond to natural transformations? they'd be lenses in that case. i'm reasonably confident charts are not natural transformations.

Reid Barton (Apr 24 2023 at 11:24):

I'm ignoring everything associated with the phrase "polynomial functor" and instead building the map $E \to B$ of sets where $B$ is position and $E$ is the sigma type of direction, together with its projection to the first component $B$.

Reid Barton (Apr 24 2023 at 11:25):

Then in Chart I see if we have two of these $E \to B$, $E' \to B'$ then we ask for a map $f : B \to B'$ together with, for each $b \in B$ and element of $E_b$, an element of $E'_{f(b)}$; those assemble into a map $g : E \to E'$ lying over $f$, i.e., a commutative square. (Or indeed a natural transformation of diagrams from the category $\bullet \to \bullet$ to Set.)

Reid Barton (Apr 24 2023 at 11:27):

I assume this is somehow missing the point of the original question, because it doesn't have any direct relationship to the actual polynomial functor associated to the data Polynomial.