feat(Algebra/MonoidAlgebra/NoZeroDivisors): `NoZeroDivisors` instance on `AddMonoidAlgebra`s #6627

adomani · 2023-08-17T08:05:51Z

Porting the first part of mathlib3 #16157.

This contains the NoZeroDivisor instance on AddMonoidAlgebras that will trickle down to (Mv)Polynomials.

alreadydone · 2023-08-17T15:43:13Z

Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean

+variable [NoZeroDivisors R] [Add A] [LinearOrder A] [CovariantClass A A (· + ·) (· < ·)]
+  [CovariantClass A A (Function.swap (· + ·)) (· < ·)]


Currently, Covariants.to_uniqueSums uses the stronger set of conditions

[CovariantClass A A (· * ·) (· ≤ ·)] [CovariantClass A A (Function.swap (· * ·)) (· < ·)] [ContravariantClass A A (· * ·) (· ≤ ·)]

In fact the last condition is equivalent to [CovariantClass A A (· + ·) (· < ·)] in a linear order because a + c ≤ a + b → c ≤ b is simply the contrapositive of b < c → a + b < a + c.

I think the way to go is to change Covariants.to_uniqueSums (and eq_and_eq_of_le_of_le_of_add_le) to use the same conditions as here, prove NoZeroDivisors.uniqueSums here instead, and derive NoZeroDivisors.biOrdered from it. And I think we can make the proof of NoZeroDivisors.of_left_ordered etc. a single line.

Maybe we could make UniqueSums a typeclass and then NoZeroDivisors.biOrdered would be inferInstance.

Also, it should be trivial to add the MonoidAlgebra version, but I think to_additive doesn't work here.

Yes, you are right: the plan was indeed to use UniqueSums! I simply got stuck a few PRs before the port started... I'll fix it, but now is time to sleep for me!

Thanks and no worries! It's my bad that I already realized the PR is outdated but still mentioned it. No rush to update PR because I find that stuff around Covariant/ContravariantClasses should benefit from some refactoring utilizing Lean 4's loopy instances: there are lots of results of the shape A ↔ B, or A → B and B ∧ C → A. It would be nice to unify the assumptions of Left.add_eq_add_iff_eq_and_eq, Right.add_eq_add_iff_eq_and_eq, and your eq_and_eq_of_le_of_le_of_add_le, for example. I'll keep you updated!

(And I just realized UniqueProds and UniqueSums are indeed already instances; I confused them with UniqueMul and UniqueMul.

Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean

Ruben-VandeVelde · 2023-08-18T11:20:55Z

Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean

+###  Remarks
+To prove `NoZeroDivisors.biOrdered`,
+we use `CovariantClass` assumptions on `A`.  In combination with `LinearOrder A`, these
+assumptions actually imply that `A` is cancellative.  However, cancellativity alone in not enough.


Suggested change

assumptions actually imply that `A` is cancellative. However, cancellativity alone in not enough.

assumptions actually imply that `A` is cancellative. However, cancellativity alone is not enough.

Ruben-VandeVelde · 2023-08-18T11:21:40Z

Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean

+open Finsupp AddMonoidAlgebra
+
+example {R} [Ring R] [Nontrivial R] :
+  ∃ x y : AddMonoidAlgebra R (ZMod 2), x * y = 0 ∧ x ≠ 0 ∧ y ≠ 0 := by


Does this belong in Counterexamples/?

Ruben-VandeVelde · 2023-08-18T11:22:12Z

Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean

+The corresponding statement for a general product `f * g` is `AddMonoidAlgebra.mul_apply_of_le`.
+It is proved with a further `CovariantClass` assumption. -/
+theorem single_mul_apply_of_le (r : R) (ft : ∀ a ∈ f.support, a ≤ t) :
+  ((AddMonoidAlgebra.single a r) * f) (a + t) = r * f t := by


Suggested change

((AddMonoidAlgebra.single a r) * f) (a + t) = r * f t := by

(AddMonoidAlgebra.single a r * f) (a + t) = r * f t := by

Ruben-VandeVelde · 2023-08-18T11:22:47Z

Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean

+  ((AddMonoidAlgebra.single a r) * f) (a + b) = r * f b :=
+single_mul_apply_of_le (A := Aᵒᵈ) _ fb


Suggested change

((AddMonoidAlgebra.single a r) * f) (a + b) = r * f b :=

single_mul_apply_of_le (A := Aᵒᵈ) _ fb

(AddMonoidAlgebra.single a r * f) (a + b) = r * f b :=

single_mul_apply_of_le (A := Aᵒᵈ) _ fb

Ruben-VandeVelde · 2023-08-18T11:23:01Z

Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean

+Here, "top" is simply an upper bound for the elements of the support of the corresponding
+polynomial (e.g. the product is `0` if "top" is not a maximum). -/
+theorem mul_apply_of_le (fa : ∀ i ∈ f.support, i ≤ a) (gt : ∀ i ∈ g.support, i ≤ t) :
+  (f * g) (a + t) = f a * g t := by


Suggested change

(f * g) (a + t) = f a * g t := by

(f * g) (a + t) = f a * g t := by

Ruben-VandeVelde · 2023-08-18T11:23:51Z

Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean

+  (f * g) (a + b) = f a * g b :=
+mul_apply_of_le (A := Aᵒᵈ) fa gb


Suggested change

(f * g) (a + b) = f a * g b :=

mul_apply_of_le (A := Aᵒᵈ) fa gb

(f * g) (a + b) = f a * g b :=

mul_apply_of_le (A := Aᵒᵈ) fa gb

Ruben-VandeVelde · 2023-08-18T11:24:16Z

Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean

+mul_apply_of_le (A := Aᵒᵈ) fa gb
+
+theorem mul_apply_eq_zero_of_lt (fa : ∀ i ∈ f.support, a ≤ i) (gb : ∀ i ∈ g.support, b < i) :
+  (f * g) (a + b) = 0 := by


Suggested change

(f * g) (a + b) = 0 := by

(f * g) (a + b) = 0 := by

Ruben-VandeVelde · 2023-08-18T11:31:50Z

Mathlib/Algebra/MonoidAlgebra/NoZeroDivisors.lean

+  simp only [Finsupp.coe_zero, Pi.zero_apply]
+  rw [mul_apply_of_le] <;>
+    try exact Finset.le_max' _
+  refine mul_ne_zero_iff.mpr ⟨?_, ?_⟩ <;>


Suggested change

refine mul_ne_zero_iff.mpr ⟨?_, ?_⟩ <;>

refine mul_ne_zero ?_ ?_ <;>

adomani added 3 commits August 17, 2023 09:47

NoZeroDivisors

4e3902b

Docs

1673aa8

Fixes

43532b8

adomani changed the title ~~feat():~~ feat(Algebra/MonoidAlgebra/NoZeroDivisors): NoZeroDivisors instance on AddMonoidAlgebras Aug 17, 2023

adomani added 2 commits August 17, 2023 10:07

Isolated bys

a87dfdc

Docs

6ecdaef

adomani added awaiting-review The author would like community review of the PR t-algebra Algebra (groups, rings, fields etc) labels Aug 17, 2023

adomani mentioned this pull request Aug 17, 2023

feat(..Polynomial..): MvPolynomials have no zero divisors #6633

Open

1 task

alreadydone reviewed Aug 17, 2023

View reviewed changes

Use targeted implicits, as per Junyan's suggestion

b05da78

Ruben-VandeVelde reviewed Aug 18, 2023

View reviewed changes

negiizhao mentioned this pull request Aug 22, 2023

feat: Lindemann-Weierstrass Theorem #6718

Open

5 tasks

YaelDillies 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 Sep 6, 2023

leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Sep 14, 2023

bors bot changed the base branch from master to ScottCarnahan/BinomialRing2 September 17, 2023 03:26

semorrison changed the base branch from ScottCarnahan/BinomialRing2 to master September 17, 2023 12:12

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(Algebra/MonoidAlgebra/NoZeroDivisors): `NoZeroDivisors` instance on `AddMonoidAlgebra`s #6627

feat(Algebra/MonoidAlgebra/NoZeroDivisors): `NoZeroDivisors` instance on `AddMonoidAlgebra`s #6627

adomani commented Aug 17, 2023

alreadydone Aug 17, 2023

alreadydone Aug 17, 2023 •

edited

adomani Aug 17, 2023

alreadydone Aug 17, 2023 •

edited

Ruben-VandeVelde Aug 18, 2023

Ruben-VandeVelde Aug 18, 2023

Ruben-VandeVelde Aug 18, 2023

Ruben-VandeVelde Aug 18, 2023

Ruben-VandeVelde Aug 18, 2023

Ruben-VandeVelde Aug 18, 2023

Ruben-VandeVelde Aug 18, 2023

Ruben-VandeVelde Aug 18, 2023

		variable [NoZeroDivisors R] [Add A] [LinearOrder A] [CovariantClass A A (· + ·) (· < ·)]
		[CovariantClass A A (Function.swap (· + ·)) (· < ·)]

	assumptions actually imply that `A` is cancellative. However, cancellativity alone in not enough.
	assumptions actually imply that `A` is cancellative. However, cancellativity alone is not enough.

	((AddMonoidAlgebra.single a r) * f) (a + t) = r * f t := by
	(AddMonoidAlgebra.single a r * f) (a + t) = r * f t := by

		((AddMonoidAlgebra.single a r) * f) (a + b) = r * f b :=
		single_mul_apply_of_le (A := Aᵒᵈ) _ fb

	(f * g) (a + t) = f a * g t := by
	(f * g) (a + t) = f a * g t := by

		(f * g) (a + b) = f a * g b :=
		mul_apply_of_le (A := Aᵒᵈ) fa gb

	refine mul_ne_zero_iff.mpr ⟨?_, ?_⟩ <;>
	refine mul_ne_zero ?_ ?_ <;>

feat(Algebra/MonoidAlgebra/NoZeroDivisors): NoZeroDivisors instance on AddMonoidAlgebras #6627

Are you sure you want to change the base?

feat(Algebra/MonoidAlgebra/NoZeroDivisors): NoZeroDivisors instance on AddMonoidAlgebras #6627

Conversation

adomani commented Aug 17, 2023

Choose a reason for hiding this comment

alreadydone Aug 17, 2023 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

alreadydone Aug 17, 2023 • 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

feat(Algebra/MonoidAlgebra/NoZeroDivisors): `NoZeroDivisors` instance on `AddMonoidAlgebra`s #6627

feat(Algebra/MonoidAlgebra/NoZeroDivisors): `NoZeroDivisors` instance on `AddMonoidAlgebra`s #6627

alreadydone Aug 17, 2023 •

edited

alreadydone Aug 17, 2023 •

edited