structure vs class

Stream: general

[Kenny Lau]

The age-old question: when to use structure and when to use class?

[Kevin Buzzard]

You have to step back and decide whether you want a global, unique instance or not.

[Kenny Lau]

universes u v

variables (G : Type u) [group G] (X : Type v)

class group_action : Type (max u v) :=
(fn : G → X → X)
(one : ∀ x, fn 1 x = x)
(mul : ∀ g h x, fn (g * h) x = fn g (fn h x))

[Kenny Lau]

should this be a class or a structure?

[Mario Carneiro]

A class, I would think, if you want that notation to work

[Mario Carneiro]

You may also be able to make one of the two type arguments an out_param. Would you say that one (kind of) uniquely determines the other?

[Kenny Lau]

A class, I would think, if you want that notation to work

I also think so, but then the following becomes awkward, since it suggests that I can synthesize more than one group actions:

protected def trivial : group_action G S :=
⟨λ g, id, λ x, rfl, λ g h x, rfl⟩

[Kenny Lau]

You may also be able to make one of the two type arguments an out_param. Would you say that one (kind of) uniquely determines the other?

a module is just an R-action right, so maybe we can use the same strategy

[Kenny Lau]

although the set has an abelian group structure

[Kenny Lau]

I don't know in this case, what do you think?

[Mario Carneiro]

Of course there are multiple group actions in actuality, but probably you want to focus on just one in a given context. Maybe using local instance?

[Kenny Lau]

I actually just want to state it, so maybe def is fine

[Patrick Massot]

universes u v

variables (G : Type u) [group G] (X : Type v)

class group_action : Type (max u v) :=
(fn : G → X → X)
(one : ∀ x, fn 1 x = x)
(mul : ∀ g h x, fn (g * h) x = fn g (fn h x))

Why not

structure  action (G : Type*) [group G] (α : Type*) :=
(map : G → equiv.perm α)
(homo : is_group_hom map)

[Kenny Lau]

because.

[Kenny Lau]

because stating it more abstractly makes it less useful

[Kenny Lau]

conciseness c’est pas tous

[Patrick Massot]

See also https://github.com/PatrickMassot/lean-scratchpad/blob/master/subgroups.lean for related random stuff

[Patrick Massot]

Using group homomorphism should give you access to lemmas you'll need to reprove with your less abstract definition

[Mario Carneiro]

you want to restate them anyway though

[Mario Carneiro]

I think that kenny's version more accurately represents the data content, which is a single function G -> X -> X satisfying some properties, rather than a function to a pair of functions

[Mario Carneiro]

of course you want your version stated as lemmas, and then all those theorems become available in the end anyway

[Patrick Massot]

Mathematically the accurate representation of content if certainly mine. About Lean usability I don't know of course

[Mario Carneiro]

they are certainly equivalent, but the data content is different. It's like the difference between representing the integers by an integer, or by a pair of an integer and its negative. The representations are equivalent, but one has some additional redundancy

[Kenny Lau]

let’s all just represent nat by Pi X, X->(X->X)->X

[Patrick Massot]

Ok, I think I understand the confusion: we are talking about two separate issues. My claim is that the mathematically meaningful and redundancy free point of view is to define a group action as a group homomorphism. It seems you are discussing the redundancy in your definition of perm X. Now I'm even more confused. A long time ago you told I should build homeomorphisms on top of equiv. Since then I've been suffering through two levels of coercions (homeo to equiv to function). And I have loads of attempted proofs where I'm stuck with expression mixing multiplication in the group homeo X X and composition of equiv and composition of functions, which are all the same but I never know how to tell Lean. And a few days ago you proved this f '' (-s) = - f '' s by throwing away equiv and use function.bijective, so this is the second time in a couple of days where you seem to avoid equiv. I would appreciate any clue about what I should be doing with my groups of homeomorphisms.

[Kenny Lau]

@Patrick Massot How would you state a G-Set homomorphism in your definition of G-Set? In mine, f:X->Y is a homomorphism if f(gx)=gf(x)

[Patrick Massot]

I don't understand your question. If ρ_X : G → perm X and ρ_Y : G → perm Y are two G-action then f : X → Y is a G-morphism if, for all g, f ∘ ρ_X(g) = ρ_Y(g) ∘ f

[Kenny Lau]

interesting

[Patrick Massot]

Of course you could phrase this in terms of natural transformations

[Kenny Lau]

I can see a commutative diagram inside :P

[Patrick Massot]

If you want Mario to run away

[Kenny Lau]

oh really

[Patrick Massot]

Sure

[Kenny Lau]

could you enlighten me?

[Kenny Lau]

and I feel like I've seen this in group rep

[Patrick Massot]

But what I was advocating is an intermediate point of view, not going all the way to using categories to define group actions

[Kenny Lau]

I am writing a category theory repo

[Kenny Lau]

so it is helpful to me

[Kenny Lau]

https://github.com/kckennylau/category-theory

[Kenny Lau]

in fact I'm proving that the forgetful functor GSet->Set has right adjoint

[Patrick Massot]

A group is a category with one object, and morphisms given by the group element

[Patrick Massot]

then a G-set is simply a functor from G to Set

[Kenny Lau]

but it would be a fun fact to prove that that functor thing is isomorphic to the GSet in the category of categories

[Kenny Lau]

aha, so it's the slice category

[Patrick Massot]

And a morphism of G-set is a morphism in this category

[Patrick Massot]

hence a natural transformation

[Kenny Lau]

very interesting

[Patrick Massot]

It's meant to be the very first exercise you do after reading the definition of a natural transformation

[Kenny Lau]

where do you learn category theory?

[Patrick Massot]

Are you talkin to Scott about this repo?

[Kenny Lau]

I'm not; he hasn't replied to my message

[Kenny Lau]

I don't think I've seen him here for a while

[Patrick Massot]

He was probably captured by real life

[Patrick Massot]

This happened to me during the last couple of weeks

[Patrick Massot]

And actually students will probably invade my office soon, and I'll have to let you do your category theory exercises

[Kenny Lau]

alright

[Kevin Buzzard]

I don't think I've seen him here for a while

Scott is on holiday at the minute.

[Scott Morrison]

I am back, but actual maths has captured my attention for a moment --- a collaborator is here this week.

[Kenny Lau]

omg you're back

[Scott Morrison]

I am definitely still working on getting my category theory library reading for a PR, but there is still some work to do, which I haven't been finding a lot of time for.

[Kenny Lau]

hope you don't mind the fact that i'm creating another

[Scott Morrison]

No, not at all.

[Scott Morrison]

If you would like to join forces, however, I would be very happy.

[Kenny Lau]

sure

[Scott Morrison]

I think it is good to have different eyes and different opinions on projects.

[Scott Morrison]

I think my focus for category theory for a while will be not adding new material, but rather getting the basics PR'd into mathlib.

[Scott Morrison]

If you would like to add material, however, that is certainly fine.

[Scott Morrison]

Also, if you have comments and criticisms of the basics, I'm very happy to hear them concurrently with preparing to PR.

[Kenny Lau]

have you looked at mine?

[Scott Morrison]

I'm happy to just give you commit access on the repository if you'd like, or I'll merge PRs as they come.

[Scott Morrison]

Looking at yours is on my todo list, but Lean is not getting to the top of the todo list again until next week.

[Kenny Lau]

well you would need to fix your repo first, I heard it doesn't work well with the latest mathlib

[Scott Morrison]

It was working after the "monad merge" on Lean, and the subsequent update to Lean. I will check again in a moment. Hopefully it is okay, however.

[Scott Morrison]

Besides irrelevant problems in mathlib, lean-category-theory builds fine against the HEAD of Lean at the moment.

[Kevin Buzzard]

Kenny's top priority at the minute is revising for mechanics, but let me give a huge +1 to the idea of you two collaborating on category theory. Kenny seems to understand all the standard category theoretic notions well now, and has a bunch of examples in his head, so whilst he might not yet be at the stage of doing infinity-1 categories or whatever, he will almost certainly have more time to work on categories in the near future (e.g. after his mechanics exam in mid-May)

[Kenny Lau]

right, there's mechanics

[Kevin Buzzard]

And I am doing my schemes library by proving lots of things about sheaves and presheaves of types, and then writing ad hoc extensions to sheaves of rings

[Kevin Buzzard]

and the sooner I can do sheaves of objects the better

[Patrick Massot]

Exams are in mid-May and they are already revising?

[Patrick Massot]

That's even more amazing than first year students using Lean!

[Kenny Lau]

"they are already revising", more like "they are already being told to revise"

[Patrick Massot]

This afternoon I will attend a talk whose title is: "Perfectoid spaces and us"

[Patrick Massot]

for a general mathematical audience

[Kenny Lau]

by thomas hales?

[Patrick Massot]

Did you make any progress in formalizing perfectoid spaces

[Kenny Lau]

aucun

[Patrick Massot]

No, by Ariane Mézard

[Kevin Buzzard]

Our progress so far is a new empty repository, and Kenny wrote some stuff about valuations and then found he didn't have push access.

[Kevin Buzzard]

I think that claiming that we "did" schemes but not even being able to construct one example is not such a great advertisement, so when I write Lean code I typically try and fix this problem. We are nearly there. I broke the problem down into three parts; part (3) is basically done, part (1) Chris Hughes has nearly finished and part (2) should be easy (and I will start on it soon, hopefully). When we can prove that an affine scheme is a scheme I will get back to perfectoid spaces.

[Kevin Buzzard]

by thomas hales?

Kenny, I don't think Tom Hales knows too much about perfectoid spaces.

[Patrick Massot]

I was sitting next to Fontaine during that talk and, according to him, Ariane also doesn't know much about perfectoid spaces.

[Patrick Massot]

Which probably means we are lucky Mézard gave this talk instead of Fontaine :smile:

[Patrick Massot]

Also, I didn't tell Fontaine about schemes without example

[Patrick Massot]

But I confess I told this story to François Charles a couple of days ago

[Patrick Massot]

He agrees the fact that affine schemes are schemes is not trivial, but still disapproves having defined schemes with no example

[Patrick Massot]

During that inauguration thing I also got the opportunity of chatting a bit with Christine Paulin (the dean of my university, who was involved in the theoretical foundations of Coq).

[Patrick Massot]

Then a colleague asked me why I was talking to her, and I may have found one new recruit for Lean

[Kevin Buzzard]

Which probably means we are lucky Mézard gave this talk instead of Fontaine :smile:

Anyone who wants to hear Fontaine's opinion can just read his Sem Bourbaki :-)

[Patrick Massot]

I once opened this Bourbaki seminar and decided it was not written for me :wink:

[Patrick Massot]

But, to be honest, I don't think Fontaine would say the Bourbaki I wrote about flexibility of contact structures in higher dimensions was written for him.