Zulip Chat Archive
Stream: general
Topic: structure vs class
Kenny Lau (Apr 02 2018 at 04:17):
The age-old question: when to use structure
and when to use class
?
Kevin Buzzard (Apr 02 2018 at 11:45):
You have to step back and decide whether you want a global, unique instance or not.
Kenny Lau (Apr 03 2018 at 03:41):
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 (Apr 03 2018 at 03:41):
should this be a class
or a structure
?
Mario Carneiro (Apr 03 2018 at 03:42):
A class, I would think, if you want that notation to work
Mario Carneiro (Apr 03 2018 at 03:43):
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 (Apr 03 2018 at 03:44):
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 (Apr 03 2018 at 03:44):
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 (Apr 03 2018 at 03:44):
although the set has an abelian group structure
Kenny Lau (Apr 03 2018 at 03:45):
I don't know in this case, what do you think?
Mario Carneiro (Apr 03 2018 at 03:45):
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 (Apr 03 2018 at 03:46):
I actually just want to state it, so maybe def
is fine
Patrick Massot (Apr 03 2018 at 05:45):
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 (Apr 03 2018 at 05:46):
because.
Kenny Lau (Apr 03 2018 at 05:46):
because stating it more abstractly makes it less useful
Kenny Lau (Apr 03 2018 at 05:46):
conciseness c’est pas tous
Patrick Massot (Apr 03 2018 at 05:48):
See also https://github.com/PatrickMassot/lean-scratchpad/blob/master/subgroups.lean for related random stuff
Patrick Massot (Apr 03 2018 at 05:48):
Using group homomorphism should give you access to lemmas you'll need to reprove with your less abstract definition
Mario Carneiro (Apr 03 2018 at 05:49):
you want to restate them anyway though
Mario Carneiro (Apr 03 2018 at 05:50):
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 (Apr 03 2018 at 05:50):
of course you want your version stated as lemmas, and then all those theorems become available in the end anyway
Patrick Massot (Apr 03 2018 at 05:58):
Mathematically the accurate representation of content if certainly mine. About Lean usability I don't know of course
Mario Carneiro (Apr 03 2018 at 06:12):
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 (Apr 03 2018 at 06:13):
let’s all just represent nat by Pi X, X->(X->X)->X
Patrick Massot (Apr 03 2018 at 12:56):
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 (Apr 03 2018 at 12:57):
@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 (Apr 03 2018 at 13:02):
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 (Apr 03 2018 at 13:02):
interesting
Patrick Massot (Apr 03 2018 at 13:02):
Of course you could phrase this in terms of natural transformations
Kenny Lau (Apr 03 2018 at 13:02):
I can see a commutative diagram inside :P
Patrick Massot (Apr 03 2018 at 13:02):
If you want Mario to run away
Kenny Lau (Apr 03 2018 at 13:03):
oh really
Patrick Massot (Apr 03 2018 at 13:03):
Sure
Kenny Lau (Apr 03 2018 at 13:03):
could you enlighten me?
Kenny Lau (Apr 03 2018 at 13:04):
and I feel like I've seen this in group rep
Patrick Massot (Apr 03 2018 at 13:05):
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 (Apr 03 2018 at 13:06):
I am writing a category theory repo
Kenny Lau (Apr 03 2018 at 13:06):
so it is helpful to me
Kenny Lau (Apr 03 2018 at 13:06):
https://github.com/kckennylau/category-theory
Kenny Lau (Apr 03 2018 at 13:06):
in fact I'm proving that the forgetful functor GSet->Set has right adjoint
Patrick Massot (Apr 03 2018 at 13:06):
A group is a category with one object, and morphisms given by the group element
Patrick Massot (Apr 03 2018 at 13:07):
then a G-set is simply a functor from G to Set
Kenny Lau (Apr 03 2018 at 13:07):
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 (Apr 03 2018 at 13:07):
aha, so it's the slice category
Patrick Massot (Apr 03 2018 at 13:07):
And a morphism of G-set is a morphism in this category
Patrick Massot (Apr 03 2018 at 13:07):
hence a natural transformation
Kenny Lau (Apr 03 2018 at 13:07):
very interesting
Patrick Massot (Apr 03 2018 at 13:08):
It's meant to be the very first exercise you do after reading the definition of a natural transformation
Kenny Lau (Apr 03 2018 at 13:08):
where do you learn category theory?
Patrick Massot (Apr 03 2018 at 13:08):
Are you talkin to Scott about this repo?
Kenny Lau (Apr 03 2018 at 13:08):
I'm not; he hasn't replied to my message
Kenny Lau (Apr 03 2018 at 13:08):
I don't think I've seen him here for a while
Patrick Massot (Apr 03 2018 at 13:09):
He was probably captured by real life
Patrick Massot (Apr 03 2018 at 13:09):
This happened to me during the last couple of weeks
Patrick Massot (Apr 03 2018 at 13:10):
And actually students will probably invade my office soon, and I'll have to let you do your category theory exercises
Kenny Lau (Apr 03 2018 at 13:10):
alright
Kevin Buzzard (Apr 03 2018 at 14:59):
I don't think I've seen him here for a while
Scott is on holiday at the minute.
Scott Morrison (Apr 03 2018 at 23:29):
I am back, but actual maths has captured my attention for a moment --- a collaborator is here this week.
Kenny Lau (Apr 03 2018 at 23:30):
omg you're back
Scott Morrison (Apr 03 2018 at 23:30):
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 (Apr 03 2018 at 23:30):
hope you don't mind the fact that i'm creating another
Scott Morrison (Apr 03 2018 at 23:30):
No, not at all.
Scott Morrison (Apr 03 2018 at 23:30):
If you would like to join forces, however, I would be very happy.
Kenny Lau (Apr 03 2018 at 23:31):
sure
Scott Morrison (Apr 03 2018 at 23:31):
I think it is good to have different eyes and different opinions on projects.
Scott Morrison (Apr 03 2018 at 23:31):
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 (Apr 03 2018 at 23:31):
If you would like to add material, however, that is certainly fine.
Scott Morrison (Apr 03 2018 at 23:32):
Also, if you have comments and criticisms of the basics, I'm very happy to hear them concurrently with preparing to PR.
Kenny Lau (Apr 03 2018 at 23:32):
have you looked at mine?
Scott Morrison (Apr 03 2018 at 23:32):
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 (Apr 03 2018 at 23:32):
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 (Apr 03 2018 at 23:32):
well you would need to fix your repo first, I heard it doesn't work well with the latest mathlib
Scott Morrison (Apr 03 2018 at 23:33):
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 (Apr 03 2018 at 23:42):
Besides irrelevant problems in mathlib, lean-category-theory builds fine against the HEAD of Lean at the moment.
Kevin Buzzard (Apr 04 2018 at 09:34):
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 (Apr 04 2018 at 09:34):
right, there's mechanics
Kevin Buzzard (Apr 04 2018 at 09:34):
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 (Apr 04 2018 at 09:35):
and the sooner I can do sheaves of objects the better
Patrick Massot (Apr 04 2018 at 09:49):
Exams are in mid-May and they are already revising?
Patrick Massot (Apr 04 2018 at 09:49):
That's even more amazing than first year students using Lean!
Kenny Lau (Apr 04 2018 at 09:50):
"they are already revising", more like "they are already being told to revise"
Patrick Massot (Apr 04 2018 at 09:54):
This afternoon I will attend a talk whose title is: "Perfectoid spaces and us"
Patrick Massot (Apr 04 2018 at 09:55):
for a general mathematical audience
Kenny Lau (Apr 04 2018 at 09:55):
by thomas hales?
Patrick Massot (Apr 04 2018 at 09:55):
Did you make any progress in formalizing perfectoid spaces
Kenny Lau (Apr 04 2018 at 09:55):
aucun
Patrick Massot (Apr 04 2018 at 09:55):
No, by Ariane Mézard
Kevin Buzzard (Apr 04 2018 at 14:54):
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 (Apr 04 2018 at 14:57):
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 (Apr 04 2018 at 14:57):
by thomas hales?
Kenny, I don't think Tom Hales knows too much about perfectoid spaces.
Patrick Massot (Apr 04 2018 at 17:54):
I was sitting next to Fontaine during that talk and, according to him, Ariane also doesn't know much about perfectoid spaces.
Patrick Massot (Apr 04 2018 at 17:54):
Which probably means we are lucky Mézard gave this talk instead of Fontaine :smile:
Patrick Massot (Apr 04 2018 at 17:55):
Also, I didn't tell Fontaine about schemes without example
Patrick Massot (Apr 04 2018 at 17:55):
But I confess I told this story to François Charles a couple of days ago
Patrick Massot (Apr 04 2018 at 17:56):
He agrees the fact that affine schemes are schemes is not trivial, but still disapproves having defined schemes with no example
Patrick Massot (Apr 04 2018 at 17:57):
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 (Apr 04 2018 at 18:02):
Then a colleague asked me why I was talking to her, and I may have found one new recruit for Lean
Kevin Buzzard (Apr 04 2018 at 19:54):
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 (Apr 04 2018 at 21:27):
I once opened this Bourbaki seminar and decided it was not written for me :wink:
Patrick Massot (Apr 04 2018 at 21:28):
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.
Last updated: Dec 20 2023 at 11:08 UTC