[Merged by Bors] - feat(algebra/ring/basic): define non-unital, non-associative rings #6786

ocfnash · 2021-03-20T17:08:30Z

This introduces the following typeclasses beneath semiring:

non_unital_non_assoc_semiring
non_unital_semiring
non_assoc_semiring

The goal is to use these to support a non-unital, non-associative
algebras.

The typeclass requirements of subring, subsemiring, and ring_hom are relaxed from semiring to non_assoc_semiring.

Instances of these new typeclasses are added for:

alias types:
- opposite
- ulift
convolutive types:
- (add_)monoid_algebra
- direct_sum
- set_semiring
- hahn_series
elementwise types:
- locally_constant
- pi
- prod
- finsupp

The changes here aim to be the uncontroversial part of #6591

depends on [Merged by Bors] - refactor(algebra/*): add new mul_one_class and add_zero_class for non-associative monoids #6865
depends on [Merged by Bors] - chore(algebra/opposite): add missing monoid_with_zero instance #7339
depends on [Merged by Bors] - feat(algebra/group_with_zero): add semigroup_with_zero #7346 (semigroup_with_zero)
depends on [Merged by Bors] - chore(ring_theory/hahn_series): emb_domain_add needs only add_monoid, not semiring #7802

They key changes here are the introduction of the following: * `non_unital_non_assoc_semiring` * `non_unital_semiring` * `non_assoc_semiring` The goal is to use these to support a non-unital, non-associative algebras.

src/analysis/special_functions/trigonometric.lean

src/data/mv_polynomial/variables.lean

src/algebra/group_with_zero/defs.lean

src/algebra/group/defs.lean

src/algebra/ring/basic.lean

I decided to make one last attempt at this. Let's see if it builds.

I _pray_ that this doesn't send me down another rabbit hole of failed builds.

src/algebra/group/defs.lean

src/algebra/pointwise.lean

src/data/mv_polynomial/variables.lean

src/algebra/group/defs.lean

semorrison · 2021-03-22T22:30:26Z

bors merge

eric-wieser · 2021-06-01T22:27:23Z

CI looks happy now - I'll look over this once more tomorrow, but i think it's ready to go

This isn't a complete generalization of all lemmas, but at least puts the instances in place

# Conflicts: # src/data/finsupp/pointwise.lean

eric-wieser · 2021-06-02T13:30:27Z

src/ring_theory/hahn_series.lean

+section domain
+variables {Γ' : Type*} [partial_order Γ']
+
+lemma emb_domain_add (f : Γ ↪o Γ') (x y : hahn_series Γ R) :
+  emb_domain f (x + y) = emb_domain f x + emb_domain f y :=
+begin
+  ext g,
+  by_cases hg : g ∈ set.range f,
+  { obtain ⟨a, rfl⟩ := hg,
+    simp },
+  { simp [emb_domain_notin_range, hg] }
+end
+
+end domain
+


This change is #7802, which is probably worth merging first just to keep the history manageable

eric-wieser

CI needs to run again, but I think I cleaned up all the distrib instances that can now be non_unital_non_assoc_semiring instances.

… non_unital_assoc_rings

eric-wieser · 2021-06-05T16:18:42Z

src/data/multiset/antidiagonal.lean

@@ -77,7 +77,9 @@ begin
  refine s.induction_on _ _,
  { simp },
  { assume a s ih,
-    simp [ih, add_mul, mul_comm, mul_left_comm, mul_assoc, sum_map_mul_left.symm],
+    have := @sum_map_mul_left α β _,


Suggested change

have := @sum_map_mul_left α β _,

jcommelin · 2021-06-07T12:37:28Z

Great accomplishment!

Thanks 🎉

bors merge

…6786) This introduces the following typeclasses beneath `semiring`: * `non_unital_non_assoc_semiring` * `non_unital_semiring` * `non_assoc_semiring` The goal is to use these to support a non-unital, non-associative algebras. The typeclass requirements of `subring`, `subsemiring`, and `ring_hom` are relaxed from `semiring` to `non_assoc_semiring`. Instances of these new typeclasses are added for: * alias types: * `opposite` * `ulift` * convolutive types: * `(add_)monoid_algebra` * `direct_sum` * `set_semiring` * `hahn_series` * elementwise types: * `locally_constant` * `pi` * `prod` * `finsupp` Co-authored-by: Gabriel Ebner <gebner@gebner.org> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

bors · 2021-06-07T15:39:54Z

Build failed (retrying...):

Build mathlib

…6786) This introduces the following typeclasses beneath `semiring`: * `non_unital_non_assoc_semiring` * `non_unital_semiring` * `non_assoc_semiring` The goal is to use these to support a non-unital, non-associative algebras. The typeclass requirements of `subring`, `subsemiring`, and `ring_hom` are relaxed from `semiring` to `non_assoc_semiring`. Instances of these new typeclasses are added for: * alias types: * `opposite` * `ulift` * convolutive types: * `(add_)monoid_algebra` * `direct_sum` * `set_semiring` * `hahn_series` * elementwise types: * `locally_constant` * `pi` * `prod` * `finsupp` Co-authored-by: Gabriel Ebner <gebner@gebner.org> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

eric-wieser · 2021-06-07T17:23:54Z

If this fails again it will probably do so in half an hour - we should punt this off the queue at that point, since the likelihood of it being the cause is high.

bors · 2021-06-07T20:55:01Z

Pull request successfully merged into master.

Build succeeded:

feat(algebra/ring/basic): define non-unital, non-associative rings

9037c1d

They key changes here are the introduction of the following: * `non_unital_non_assoc_semiring` * `non_unital_semiring` * `non_assoc_semiring` The goal is to use these to support a non-unital, non-associative algebras.

ocfnash commented Mar 20, 2021

View reviewed changes

src/analysis/special_functions/trigonometric.lean Show resolved Hide resolved

ocfnash commented Mar 20, 2021

View reviewed changes

src/data/mv_polynomial/variables.lean Show resolved Hide resolved

bryangingechen added the awaiting-review The author would like community review of the PR label Mar 20, 2021

jcommelin reviewed Mar 20, 2021

View reviewed changes

src/algebra/group_with_zero/defs.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Mar 20, 2021

View reviewed changes

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

eric-wieser reviewed Mar 20, 2021

View reviewed changes

src/algebra/ring/basic.lean Outdated Show resolved Hide resolved

semorrison 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 Mar 20, 2021

bryangingechen mentioned this pull request Mar 21, 2021

feat(algebra/algebra/non_unital): define non-unital, non-associative algebras #6591

Closed

1 task

ocfnash added 3 commits March 21, 2021 13:11

Change monoid / add_monoid ancestors

f867c47

I decided to make one last attempt at this. Let's see if it builds.

Fix timeout caused by change to monoid / add_monoid ancestors

a1b38de

Add monoid_with_zero.to_semigroup_with_zero

34790d4

I _pray_ that this doesn't send me down another rabbit hole of failed builds.

ocfnash 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 21, 2021

Remove redundant ancestors from monoid / add_monoid.

a365f64

eric-wieser reviewed Mar 22, 2021

View reviewed changes

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

eric-wieser reviewed Mar 22, 2021

View reviewed changes

src/algebra/pointwise.lean Outdated Show resolved Hide resolved

Weaken typeclass hypotheses for mul_one and one_mul.

dd80907

Vierkantor approved these changes Mar 22, 2021

View reviewed changes

src/data/mv_polynomial/variables.lean Show resolved Hide resolved

eric-wieser reviewed Mar 22, 2021

View reviewed changes

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

gebner and others added 6 commits March 22, 2021 15:03

Fix type tags.

7a913e2

Move misplaced attribute statement

13a1454

add comment

46ab1f4

a better fix

b4cce9d

another similar fix

2a8830e

a bit more

8f297ad

github-actions bot 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 Mar 22, 2021

semorrison 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 2, 2021

eric-wieser added 2 commits June 2, 2021 09:52

fix(deprecated/group): generalize some lemmas

1124c5c

fix(algebra/big_operators/ring): generalize some lemmas

36c1270

github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Jun 2, 2021

eric-wieser added 2 commits June 2, 2021 14:20

feat(ring_theory/hahn_series): generalize semiring typeclasses

9bc4b28

This isn't a complete generalization of all lemmas, but at least puts the instances in place

Merge remote-tracking branch 'origin/master' into non_unital_assoc_rings

929c632

# Conflicts: # src/data/finsupp/pointwise.lean

github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Jun 2, 2021

eric-wieser reviewed Jun 2, 2021

View reviewed changes

eric-wieser approved these changes Jun 2, 2021

View reviewed changes

eric-wieser added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Jun 2, 2021

github-actions bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Jun 2, 2021

eric-wieser added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Jun 3, 2021

eric-wieser mentioned this pull request Jun 3, 2021

[Merged by Bors] - chore(ring_theory/hahn_series): emb_domain_add needs only add_monoid, not semiring #7802

Closed

github-actions bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Jun 3, 2021

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

97e5e20

… non_unital_assoc_rings

bryangingechen requested a review from Vierkantor June 4, 2021 17:09

eric-wieser reviewed Jun 5, 2021

View reviewed changes

github-actions bot 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 Jun 7, 2021

bors bot changed the title ~~feat(algebra/ring/basic): define non-unital, non-associative rings~~ [Merged by Bors] - feat(algebra/ring/basic): define non-unital, non-associative rings Jun 7, 2021

bors bot closed this Jun 7, 2021

bors bot deleted the non_unital_assoc_rings branch June 7, 2021 20:55

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(algebra/ring/basic): define non-unital, non-associative rings #6786

[Merged by Bors] - feat(algebra/ring/basic): define non-unital, non-associative rings #6786

ocfnash commented Mar 20, 2021 •

edited by github-actions bot

semorrison commented Mar 22, 2021

eric-wieser commented Jun 1, 2021

eric-wieser Jun 2, 2021 •

edited

eric-wieser left a comment

eric-wieser Jun 5, 2021

jcommelin commented Jun 7, 2021

bors bot commented Jun 7, 2021

eric-wieser commented Jun 7, 2021

bors bot commented Jun 7, 2021

[Merged by Bors] - feat(algebra/ring/basic): define non-unital, non-associative rings #6786

[Merged by Bors] - feat(algebra/ring/basic): define non-unital, non-associative rings #6786

Conversation

ocfnash commented Mar 20, 2021 • edited by github-actions bot

semorrison commented Mar 22, 2021

eric-wieser commented Jun 1, 2021

eric-wieser Jun 2, 2021 • edited

Choose a reason for hiding this comment

eric-wieser left a comment

Choose a reason for hiding this comment

eric-wieser Jun 5, 2021

Choose a reason for hiding this comment

jcommelin commented Jun 7, 2021

bors bot commented Jun 7, 2021

eric-wieser commented Jun 7, 2021

bors bot commented Jun 7, 2021

ocfnash commented Mar 20, 2021 •

edited by github-actions bot

eric-wieser Jun 2, 2021 •

edited