Finite colimits in Action

Stream: Is there code for X?

[Christian Merten]

Is there a reason why there are no instances:

import Mathlib

universe u

open CategoryTheory Limits

variable (V : Type (u + 1)) [LargeCategory V] (G : MonCat.{u})

instance [HasFiniteColimits V] : HasFiniteColimits (Action V G) where
  out _ _ _ :=
    Adjunction.hasColimitsOfShape_of_equivalence (Action.functorCategoryEquivalence _ _).functor

instance [HasFiniteCoproducts V] : HasFiniteCoproducts (Action V G) where
  out _ :=
    Adjunction.hasColimitsOfShape_of_equivalence (Action.functorCategoryEquivalence _ _).functor

in Mathlib.RepresentationTheory.Action analogous to docs#Action.instHasFiniteLimitsActionInstCategoryAction ?

[Scott Morrison]

No reason except that you haven't done it yet. :-)

[Scott Morrison]

(I think I wrote the first cut of that file, and I'm sure I left a lot out. Also --- it is already a rather large file, so if you see any good points to split it that would be lovely too.)

[Christian Merten]

I'll split in definitions / generalities and permanence properties. This roughly halves the file, are you happy with that? Should I make a new file Mathlib.RepresentationTheory.ActionPermanence? Or should I create a new folder Mathilb/RepresentationTheory/Action and then two files Basic and Permanence?

[Scott Morrison]

What does "permanence" mean here?

[Christian Merten]

Ah, I mean: Specific properties of Action G V that are induced by specific properties of V, e.g. if V has all limits, then Action G V has all limits, if V is abelian, then Action G V is abelian, etc.

[Christian Merten]

i.e. properties that are preserved under the replacement V by Action G V.

[Scott Morrison]

Great, yes. Feel free to split up these properties even further (e.g. monoidal/braided/symmetric/duality stuff somewhere, limits/abelianness elsewhere, etc). I was lazy setting up this file and made it a big bag.

[Joël Riou]

I am wondering whether we could generalize Action V G to allow arbitrary universe parameters for the category V? (This would require changing Action.ρ using MonoidHom directly, and maybe unbundling G : MonCat to a type G equipped with [Monoid G].) In the future, I might want to develop a bit the notion of symmetric objects (presheaves over the category of nonemtpy finite sets), and in that context, a more general Action would be useful.

[Julian Külshammer]

To me Preservation sounds more standard terminology than Permanence?

[Joël Riou]

"Permanence" is probably a Frenchism: this is found for example in the Elements of Algebraic Geometry by Grothendieck and Dieudonné.

[Christian Merten]

Joël Riou said:

I am wondering whether we could generalize Action V G to allow arbitrary universe parameters for the category V? (This would require changing Action.ρ using MonoidHom directly, and maybe unbundling G : MonCat to a type G equipped with [Monoid G].) In the future, I might want to develop a bit the notion of symmetric objects (presheaves over the category of nonemtpy finite sets), and in that context, a more general Action would be useful.

Let's do the split first to get this out of the way and then think about extending the notion? I need Action for V = FintypeCat which is not a LargeCategory either, although Lean does not seem to care.
Related: Maybe we can extend this in such a way such that restricting to the category of continuous G-sets (for a topological group G), i.e. where the action additionally satisfies G × A → A continuous when A is equipped with the discrete topology (or maybe not necessarily discrete, but some topology), is natural?

[Christian Merten]

#8660

[Kevin Buzzard]

Just to say that I am actively interested in the case where G has a topology and A has the discrete topology and the action is continuous.

[Adam Topaz]

mumble mumble mumble internal group object mumble mumble mumble

[Adam Topaz]

@Qi Ge you might find this thread interesting as well.

[Christian Merten]

@Amelia Livingston offered in https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Galois.20categories that she could port her definition from Lean3.

[Christian Merten]

Adam Topaz said:

mumble mumble mumble internal group object mumble mumble mumble

How is the category of representations a category of internal group objects? Or did I misunderstand?

[Adam Topaz]

See docs#Mod_ for example

[Adam Topaz]

if you use this in the case of the category of topological spaces with the Cartesian monoidal structure, then this would become the category of topological spaces with a continuous action of a topological monoid

[Adam Topaz]

Where you would use a term of docs#Mon_ to represent the topological monoid.

[Christian Merten]

But it needs a monoidal structure on C, so it can't be a replacement of Action G V, right?

[Adam Topaz]

If you use the cartesian monoidal structure, then I think it could be? How is docs#Action defined?

[Adam Topaz]

Ah you're right it won't be as general.

[Adam Topaz]

But in order to state something like "the action is continuous" you at least need products to even write down a map $G \times A \to A$.

[Christian Merten]

As elements of a type V with a monoid homomorphism from G to the endomorphisms of each object.

[Adam Topaz]

The two should be equivalent in the case where the category is cartesian closed

[Christian Merten]

Adam Topaz said:

But in order to state something like "the action is continuous" you at least need products to even write down a map $G \times A \to A$.

Yes, my use case (which is still the one of V = FintypeCat and G the automorphism group of a fibre functor) would fit in the docs#Mod_ setting.

[Christian Merten]

Although I am hesitant to formulate this in terms of Mod_ as I fear that the API is still a bit lacking. It would be convenient to have one structure that naturally fits the general use case of Action G V and of these more specialized situations. Then I would be willing to invest in adding API for that.

[Yaël Dillies]

Christian Merten said:

As elements of a type V with a monoid homomorphism from G to the endomorphisms of each object.

This approach doesn't work for continuous actions since the category of topological spaces is not cartesian-closed.

[Qi Ge]

Adam Topaz said:

But in order to state something like "the action is continuous" you at least need products to even write down a map $G \times A \to A$.

One definition for the type class of continuous group action would be the type such a map :smile:. But I don't think it is the right thing to do in Lean as it does not extend MulAction for example... So maybe it should be something like this:

import Mathlib.Topology.Basic
import Mathlib.Topology.Algebra.MulAction

class ContinuousMulAction (M S : Type*) [Monoid M] [TopologicalSpace M] [TopologicalSpace S] extends MulAction M S, ContinuousSMul M S where

(Is there a diamond happening here? I'm still not entirely clear on how lean deals with inheritance and I'm not through reading about old_structure_cmd from earlier...)

[Adam Topaz]

I think we have docs#ContinuousMulAction

[Adam Topaz]

Oh sorry it is just ContinuousSmul

[Qi Ge]

Yeah we still need MulAction for group action

[Adam Topaz]

There’s no need to introduce a new class, just use ContinuousSmul as a “mixin”

[Adam Topaz]

Same for docs#ContinuousMul

[Qi Ge]

Adam Topaz said:

There’s no need to introduce a new class, just use ContinuousSmul as a “mixin”

What does it mean for a "mixin"?

[Adam Topaz]

a mixin is a class that gets introduced in an ad-hoc way. For example, if you want to prove a lemma about a topological space with a continuous action of a topological monoid you could formulate it as (untested):

lemma foobbar (M X : Type*) [TopologicalSpace M] [TopologicalSpace X] [Monoid M] [ContinunousMul M] [MulAction M X] [ContinuousSMul M X] ...`

[Adam Topaz]

https://en.wikipedia.org/wiki/Mixin