feat(group_theory/monoid_localization): some homs induced on localizations: lift, map by 101damnations · Pull Request #2118 · leanprover-community/mathlib3

101damnations · 2020-03-09T23:52:56Z

The second third of monoid_localization. The linter complained about loads of @[simp]s and I don't understand why (including some that made it through on the last PR). Maybe I need to experiment or read up on the linter, but I've removed the @[simp]s for now, anyway.

The additive versions of the away_map stuff will be in the next PR.

TO CONTRIBUTORS:

Make sure you have:

reviewed and applied the coding style: coding, naming
reviewed and applied the documentation requirements
for tactics:
- added or adapted documentation in tactics.md
- write an example of use of the new feature in tactics.lean
make sure definitions and lemmas are put in the right files
make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

into mon_loc

101damnations · 2020-03-10T08:42:19Z

I have no idea why this is failing to build due to 'deep recursion' in algebra.category.Mon.basic and I'm not sure what to do about it either. I haven't touched that file. It compiles when I checkout to master though. I dunno what I've done.

Edit: Wow, doing what errors say really does work. Increased stack size and it seems to compile now

jcommelin

On first reading, this looks really good. @ChrisHughes24 do you have some comments?

src/group_theory/monoid_localization.lean

jcommelin · 2020-03-10T09:46:17Z

src/group_theory/monoid_localization.lean

+/-- If `f : M →* N` is a localization map for a submonoid `S` and `k : N ≃* P` is an isomorphism
+    of `comm_monoid`s, `k ∘ f` is a localization map for `M` at `S`. -/
+@[to_additive "If `f : M →+ N` is a localization map for a submonoid `S` and `k : N ≃+ P` is an isomorphism of `add_comm_monoid`s, `k ∘ f` is a localization map for `M` at `S`."]
+def mul_equiv_map (k : N ≃* P) :


I think the following definitions should come with some compatibility lemmas. E.g., the coe to function of this mul_equiv_map is k ∘ f.1. But also, what happens if I compose this with k.symm: then I recover f. Similar lemmas apply below.

@101damnations What do you think of ⬆️ remark?

added some in this commit and the latest commit but I might be missing some obvious ones, I'm not sure

src/algebra/group/is_unit.lean

kim-em · 2020-03-30T22:59:37Z

@ChrisHughes24, @101damnations, where are we up to on this one? I've lost track, and can't quite tell from the unresolved conversations above which issues are ongoing or not. Does it help to have extra eyes here, or is this almost ready to go?

ChrisHughes24 · 2020-03-30T23:01:58Z

The one comment I have now, is that a lot of the monoid localisation file is quite difficult to read. Some docstribgs would be good so I can understand the statements of the theorems.

101damnations · 2020-04-01T20:05:20Z

I've not added doc strings at the end for now; those lemmas are about functions with unwieldy names but are just kind of unfolding the definitions... Apart from maybe f.mul_equiv_of_mul_equiv k H x = f.map (a proof) k x, but that's true by rfl.

into mon_loc

ChrisHughes24 · 2020-04-02T13:01:50Z

src/group_theory/monoid_localization.lean

+/-- Application of the 'weaker-than-injectivity' property of localization maps `f : M →* N`
+    for a submonoid `S ⊆ M` to the fact that for all `x₁ x₂ : M` and `y₁, y₂ ∈ S`,
+    `f x₁ * (f y₁)⁻¹ * f y₂ = f x₂ → f (x₁ * y₂) = f (x₂ * y₁)`.  -/
+@[to_additive "Application of the 'weaker-than-injectivity' property of localization maps `f : M →+ N` for a submonoid `S ⊆ M` to the fact that for all `x₁ x₂ : M` and `y₁, y₂ ∈ S`, `(f x₁ - f y₁) + f y₂ = f x₂ → f (x₁ + y₂) = f (x₂ + y₁)`."]
+lemma exists_of_sec_mk' (x) (y : S) :
  ∃ c : S, x * (sec S f.1 $ f.mk' x y).2 * c = (sec S f.1 $ f.mk' x y).1 * y * c :=
 (f.4 _ _).1 $ f.mk'_eq_iff_eq.1 $ (mk'_sec _ _).symm


This docstring doesn't seem to match the statement of the theorem.

ChrisHughes24 · 2020-04-02T13:24:07Z

src/group_theory/monoid_localization.lean

+let ⟨c, hc⟩ := (f.4 _ _).1 h in (k.4 _ _).2
+  ⟨⟨g c, hg c⟩, show g _ * g _ = g _ * g _, by rw [←g.map_mul, hc, g.map_mul]⟩
+
+@[to_additive] lemma eq_of_eq (hg : ∀ y : S, is_unit (g y)) {x y} (h : f.1 x = f.1 y) :


I think this needs a docstring.

ChrisHughes24 · 2020-04-02T13:32:33Z

src/group_theory/monoid_localization.lean

+@[simp, to_additive] lemma lift_id (x) : f.lift f.2 x = x :=
+monoid_hom.ext_iff.1 (f.lift_of_comp $ monoid_hom.id N) x
+
+@[simp, to_additive] lemma lift_inv {k : localization_map S P} (z : N) :


I think this needs a docstring

ChrisHughes24 · 2020-04-02T14:08:53Z

src/group_theory/monoid_localization.lean

+    map for `S` and `k : P ≃* M` is an isomorphism of `comm_monoid`s such that `k(T) = S`, `f ∘ k`
+    is a localization map for `T`. -/
+@[to_additive "Given `comm_monoid`s `M, P` and submonoids `S ⊆ M, T ⊆ P`, if `f : M →* N` is a localization map for `S` and `k : P ≃* M` is an isomorphism of `comm_monoid`s such that `k(T) = S`, `f ∘ k` is a localization map for `T`."]
+def mul_equiv_comap {k : P ≃* M} (H : T.map k.to_monoid_hom = S) :


To me the name comap means there's a contravariant functor somewhere. There might be a better name.

ChrisHughes24 · 2020-04-02T22:53:34Z

src/group_theory/monoid_localization.lean

+/-- If `f : M →* N` is a localization map for a submonoid `S` and `k : N ≃* P` is an isomorphism
+    of `comm_monoid`s, `k ∘ f` is a localization map for `M` at `S`. -/
+@[to_additive "If `f : M →+ N` is a localization map for a submonoid `S` and `k : N ≃+ P` is an isomorphism of `add_comm_monoid`s, `k ∘ f` is a localization map for `M` at `S`."]
+def to_mul_equiv (k : N ≃* P) :


to_mul_equiv sounds like it should make a mul_equiv

Also, @jcommelin do you think this might cause problems when in practice there is some canonical map M->P floating around that is eq but not defeq to the map given by this definition.

That will probably be painful, yes... But maybe we should save that for a later refactor, because this is something that we don't have a good solution for anyways...

ChrisHughes24 · 2020-04-03T09:38:26Z

@jcommelin any further comments before I merge this?

jcommelin · 2020-04-03T09:41:51Z

Nope, let's go!

…tions: lift, map (leanprover-community#2118) * should I be changing and committing toml idk * initial monoid loc lemmas * responding to PR comments * removing bad @[simp] * inhabited instances * remove #lint * additive inhabited instance * using is_unit & is_add_unit * doc string * remove simp * submonoid.monoid_loc... -> submonoid.localization * submonoid.monoid_loc... -> submonoid.localization * generalize inhabited instance * remove inhabited instance * 2nd section * docs and linting * removing questionable `@[simp]s` * removing away * adding lemmas, removing 'include' * removing import * responding to PR comments * use eq_of_eq to prove comp_eq_of_eq * name change * trying to update mathlib * make lemma names consistent * Update src/algebra/group/is_unit.lean * Update src/algebra/group/is_unit.lean * fix build * documentation and minor changes * spacing * fix build * applying comments Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com> Co-authored-by: Chris Hughes <chrishughes24@gmail.com> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

101damnations added 22 commits February 13, 2020 18:13

should I be changing and committing toml idk

15a7198

Merge branch 'master' of https://github.com/leanprover-community/mathlib

becaab5

Merge branch 'master' of https://github.com/leanprover-community/mathlib

8596652

initial monoid loc lemmas

56e5978

Merge branch 'master' of https://github.com/leanprover-community/mathlib

ce94ccd

into mon_loc

responding to PR comments

1b0ff70

Merge branch 'master' of https://github.com/leanprover-community/mathlib

d81b6d3

into mon_loc

removing bad @[simp]

c79917c

inhabited instances

573ddcd

remove #lint

d1aeaa0

additive inhabited instance

d5f4e95

using is_unit & is_add_unit

34a5d5e

update mathlib

fa75a6f

doc string

d8815c8

remove simp

858c992

submonoid.monoid_loc... -> submonoid.localization

a8336f6

submonoid.monoid_loc... -> submonoid.localization

1c35c9d

generalize inhabited instance

ffa57d9

remove inhabited instance

5212f1e

2nd section

5a67374

Merge branch 'master' of https://github.com/leanprover-community/mathlib

317197d

into mon_loc

docs and linting

c9f8286

jcommelin reviewed Mar 10, 2020

View reviewed changes

src/group_theory/monoid_localization.lean Outdated Show resolved Hide resolved

101damnations added 2 commits March 10, 2020 08:49

removing questionable @[simp]s

71b7d76

removing away

988613d

jcommelin reviewed Mar 10, 2020

View reviewed changes

101damnations added 2 commits March 11, 2020 13:07

adding lemmas, removing 'include'

9dc2f5b

removing import

581b049

jcommelin assigned ChrisHughes24 Mar 11, 2020

trying to update mathlib

ad87571

robertylewis 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 Mar 28, 2020

make lemma names consistent

7081026

ChrisHughes24 reviewed Mar 30, 2020

View reviewed changes

src/algebra/group/is_unit.lean Outdated Show resolved Hide resolved

src/algebra/group/is_unit.lean Outdated Show resolved Hide resolved

ChrisHughes24 and others added 3 commits March 30, 2020 14:40

Update src/algebra/group/is_unit.lean

e39c9de

Update src/algebra/group/is_unit.lean

b7c2d83

fix build

ac7cb72

101damnations added 2 commits April 1, 2020 20:54

documentation and minor changes

3b6948e

spacing

de49310

101damnations added 2 commits April 1, 2020 23:09

Merge branch 'master' of https://github.com/leanprover-community/mathlib

da04d5a

into mon_loc

fix build

7b273e1

jcommelin requested a review from ChrisHughes24 April 2, 2020 07:05

ChrisHughes24 reviewed Apr 2, 2020

View reviewed changes

applying comments

f00bbee

ChrisHughes24 reviewed Apr 2, 2020

View reviewed changes

ChrisHughes24 approved these changes Apr 3, 2020

View reviewed changes

ChrisHughes24 added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Apr 3, 2020

Merge branch 'master' into mon_loc

4ff2cbf

mergify bot merged commit a590d4b into master Apr 3, 2020

mergify bot deleted the mon_loc branch April 3, 2020 12:34

Conversation

101damnations commented Mar 9, 2020

Uh oh!

101damnations commented Mar 10, 2020 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

jcommelin left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

kim-em commented Mar 30, 2020

Uh oh!

ChrisHughes24 commented Mar 30, 2020

Uh oh!

101damnations commented Apr 1, 2020

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

ChrisHughes24 commented Apr 3, 2020

Uh oh!

jcommelin commented Apr 3, 2020

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

101damnations commented Mar 10, 2020 •

edited

Loading