[Merged by Bors] - feat(algebra/group_action_hom): define equivariant maps #2866

kckennylau · 2020-05-30T11:35:34Z

No description provided.

kckennylau · 2020-05-30T13:20:46Z

In a future PR one might redefine linear_map based on R →+[M] S

jcommelin

Thanks!

src/algebra/group_action_hom.lean

urkud · 2020-06-12T09:19:10Z

LGTM but it would be nice if someone who understands has_coe vs has_coe_t rules to look at the has_coe instances.

PatrickMassot · 2020-06-12T09:15:57Z

src/algebra/group_action_hom.lean

+
+## Main definitions
+
+* `mul_action_hom M X Y`, the type of equivariant functions from `X` to `Y`.


We don't know what structures M, X and Y are meant to have here. It makes this whole docstring unusable.

PatrickMassot · 2020-06-12T09:17:57Z

src/algebra/group_action_hom.lean

+
+-/
+
+universes u v w u₁


Do we really need all those universe variables? What happens if you put Type* everywhere?

I am used to using universe variables in lieu of Type* because of leanprover-community/lean#214 but it seems like this issue is resolved now.

PatrickMassot · 2020-06-12T09:19:20Z

src/algebra/group_action_hom.lean

+@[nolint has_inhabited_instance]
+structure distrib_mul_action_hom extends A →[M] B, A →+ B.
+
+/-- Reinterpret an equivariant additive monoid homomorphism as an additive monoid homomorphism. -/


I don't understand that docstring and the line below it.

This is the make lint happy by adding a docstring to the automatically generated distrib_mul_action_hom.to_add_monoid_hom.

cf.

mathlib/src/topology/algebra/open_subgroup.lean

Lines 26 to 27 in c8c1869

/-- Reinterpret an `open_subgroup` as a `subgroup`. -/

add_decl_doc open_subgroup.to_subgroup

PatrickMassot · 2020-06-12T09:19:47Z

src/algebra/group_action_hom.lean

+
+variables {M A B}
+
+@[simp] lemma coe_fn_coe (f : A →+[M] B) : ((f : A →+ B) : A → B) = f := rfl


Should this be norm_cast?

PatrickMassot · 2020-06-12T09:20:30Z

src/algebra/group_action_hom.lean

+variables {M A B}
+
+@[simp] lemma coe_fn_coe (f : A →+[M] B) : ((f : A →+ B) : A → B) = f := rfl
+@[simp] lemma coe_fn_coe' (f : A →+[M] B) : ((f : A →[M] B) : A → B) = f := rfl


PatrickMassot · 2020-06-12T09:21:12Z

src/algebra/group_action_hom.lean

+@[simp] lemma map_zero (f : A →+[M] B) : f 0 = 0 :=
+f.map_zero'
+
+@[simp] lemma map_add (f : A →+[M] B) (x y : A) : f (x + y) = f x + f y :=


I'm always uneasy with such simp lemmas. It's not clear to me that the RHS is simpler.

But it's what we do for other "algebraic" maps in the library, and it seems to work quite well. I think that 95% of the time I'm using this direction.

PatrickMassot · 2020-06-12T09:21:40Z

src/algebra/group_action_hom.lean

+
+variables (M) {A}
+
+/-- The identity map is equivariant. -/


This docstring sounds like it describes a Prop.

PatrickMassot · 2020-06-12T09:22:17Z

src/algebra/group_action_hom.lean

+
+variables {M R S}
+
+@[simp] lemma coe_fn_coe (f : R →+*[M] S) : ((f : R →+* S) : R → S) = f := rfl


PatrickMassot · 2020-06-12T09:22:24Z

src/algebra/group_action_hom.lean

+variables {M R S}
+
+@[simp] lemma coe_fn_coe (f : R →+*[M] S) : ((f : R →+* S) : R → S) = f := rfl
+@[simp] lemma coe_fn_coe' (f : R →+*[M] S) : ((f : R →+[M] S) : R → S) = f := rfl


PatrickMassot · 2020-06-12T09:22:39Z

src/algebra/group_action_hom.lean

+
+variables (M) {R}
+
+/-- The identity map is equivariant. -/


Docstring sounds like a Prop

robertylewis · 2020-06-12T09:35:17Z

@PatrickMassot 's norm_cast suggestions sound right to me.

robertylewis · 2020-06-12T09:40:32Z

LGTM but it would be nice if someone who understands has_coe vs has_coe_t rules to look at the has_coe instances.

The use of has_coe looks correct AFAIK.

jcommelin

@kckennylau I think this mostly looks good. If you address the comments, I would say "Let's Get This Merged".

kckennylau · 2020-06-17T09:36:17Z

Done @jcommelin

jcommelin

Thanks 🎉

bors merge

bors · 2020-06-17T09:56:19Z

👎 Rejected by label

jcommelin · 2020-06-17T09:57:32Z

bors again
bors go ahead
bors don't complain
bors merge

bors · 2020-06-17T10:37:02Z

Pull request successfully merged into master.

Build succeeded:

…ommunity#2866)

feat(algebra/group_action_hom) define equivariant maps

b163916

kckennylau added the WIP Work in progress label May 30, 2020

rwbarton changed the title ~~feat(algebra/group_action_hom) define equivariant maps~~ feat(algebra/group_action_hom): define equivariant maps May 30, 2020

kckennylau added 2 commits May 31, 2020 05:02

distrib_mul_action_hom

5581bb9

finished

1439b92

kckennylau added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels May 30, 2020

id_comp and comp_id and main docstring

88f6506

jcommelin reviewed Jun 1, 2020

View reviewed changes

jcommelin added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jun 3, 2020

per comments

20a2931

jcommelin requested a review from urkud June 8, 2020 09:56

bryangingechen added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jun 10, 2020

PatrickMassot reviewed Jun 12, 2020

View reviewed changes

robertylewis added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jun 13, 2020

jcommelin reviewed Jun 16, 2020

View reviewed changes

per comments

e91ecaf

jcommelin approved these changes Jun 17, 2020

View reviewed changes

github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Jun 17, 2020

jcommelin removed the awaiting-author A reviewer has asked the author a question or requested changes label Jun 17, 2020

bors bot pushed a commit that referenced this pull request Jun 17, 2020

feat(algebra/group_action_hom): define equivariant maps (#2866)

54441b5

bors bot changed the title ~~feat(algebra/group_action_hom): define equivariant maps~~ [Merged by Bors] - feat(algebra/group_action_hom): define equivariant maps Jun 17, 2020

bors bot closed this Jun 17, 2020

bors bot deleted the group-action-hom branch June 17, 2020 10:37

cipher1024 pushed a commit to cipher1024/mathlib that referenced this pull request Mar 15, 2022

feat(algebra/group_action_hom): define equivariant maps (leanprover-c…

4d397e7

…ommunity#2866)

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(algebra/group_action_hom): define equivariant maps #2866

[Merged by Bors] - feat(algebra/group_action_hom): define equivariant maps #2866

kckennylau commented May 30, 2020 •

edited

kckennylau commented May 30, 2020

jcommelin left a comment

urkud commented Jun 12, 2020 •

edited

PatrickMassot Jun 12, 2020

PatrickMassot Jun 12, 2020

kckennylau Jun 17, 2020

PatrickMassot Jun 12, 2020

kckennylau Jun 17, 2020

PatrickMassot Jun 12, 2020

PatrickMassot Jun 12, 2020

PatrickMassot Jun 12, 2020

jcommelin Jun 12, 2020

PatrickMassot Jun 12, 2020

PatrickMassot Jun 12, 2020

PatrickMassot Jun 12, 2020

PatrickMassot Jun 12, 2020

robertylewis commented Jun 12, 2020

robertylewis commented Jun 12, 2020

jcommelin left a comment

kckennylau commented Jun 17, 2020

jcommelin left a comment

bors bot commented Jun 17, 2020

jcommelin commented Jun 17, 2020

bors bot commented Jun 17, 2020


		## Main definitions

		* `mul_action_hom M X Y`, the type of equivariant functions from `X` to `Y`.

	/-- Reinterpret an `open_subgroup` as a `subgroup`. -/
	add_decl_doc open_subgroup.to_subgroup


		variables {M A B}

		@[simp] lemma coe_fn_coe (f : A →+[M] B) : ((f : A →+ B) : A → B) = f := rfl


		variables {M R S}

		@[simp] lemma coe_fn_coe (f : R →+[M] S) : ((f : R →+ S) : R → S) = f := rfl


		-/

		universes u v w u₁

[Merged by Bors] - feat(algebra/group_action_hom): define equivariant maps #2866

[Merged by Bors] - feat(algebra/group_action_hom): define equivariant maps #2866

Conversation

kckennylau commented May 30, 2020 • edited

kckennylau commented May 30, 2020

jcommelin left a comment

Choose a reason for hiding this comment

urkud commented Jun 12, 2020 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

robertylewis commented Jun 12, 2020

robertylewis commented Jun 12, 2020

jcommelin left a comment

Choose a reason for hiding this comment

kckennylau commented Jun 17, 2020

jcommelin left a comment

Choose a reason for hiding this comment

bors bot commented Jun 17, 2020

jcommelin commented Jun 17, 2020

bors bot commented Jun 17, 2020

kckennylau commented May 30, 2020 •

edited

urkud commented Jun 12, 2020 •

edited