From 525ff058c5d9b9d43544dd66f3fc9bf4e5ab13be Mon Sep 17 00:00:00 2001 From: Jeremy Tan Jie Rui Date: Sat, 25 Mar 2023 12:28:46 +0000 Subject: [PATCH] feat: port Algebra.MonoidAlgebra.Division (#3068) This is the second part of the forward port of leanprover-community/mathlib#15905. Co-authored-by: Eric Wieser Co-authored-by: Parcly Taxel --- Mathlib.lean | 1 + Mathlib/Algebra/MonoidAlgebra/Division.lean | 208 ++++++++++++++++++++ 2 files changed, 209 insertions(+) create mode 100644 Mathlib/Algebra/MonoidAlgebra/Division.lean diff --git a/Mathlib.lean b/Mathlib.lean index d25d8f07335b1..e142a1f7cae47 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -146,6 +146,7 @@ import Mathlib.Algebra.Module.Submodule.Pointwise import Mathlib.Algebra.Module.ULift import Mathlib.Algebra.MonoidAlgebra.Basic import Mathlib.Algebra.MonoidAlgebra.Degree +import Mathlib.Algebra.MonoidAlgebra.Division import Mathlib.Algebra.MonoidAlgebra.NoZeroDivisors import Mathlib.Algebra.MonoidAlgebra.Support import Mathlib.Algebra.NeZero diff --git a/Mathlib/Algebra/MonoidAlgebra/Division.lean b/Mathlib/Algebra/MonoidAlgebra/Division.lean new file mode 100644 index 0000000000000..db9a32fa36934 --- /dev/null +++ b/Mathlib/Algebra/MonoidAlgebra/Division.lean @@ -0,0 +1,208 @@ +/- +Copyright (c) 2022 Eric Wieser. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Eric Wieser + +! This file was ported from Lean 3 source module algebra.monoid_algebra.division +! leanprover-community/mathlib commit 72c366d0475675f1309d3027d3d7d47ee4423951 +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathlib.Algebra.MonoidAlgebra.Basic +import Mathlib.Data.Finsupp.Order + +/-! +# Division of `AddMonoidAlgebra` by monomials + +This file is most important for when `G = ℕ` (polynomials) or `G = σ →₀ ℕ` (multivariate +polynomials). + +In order to apply in maximal generality (such as for `LaurentPolynomial`s), this uses +`∃ d, g' = g + d` in many places instead of `g ≤ g'`. + +## Main definitions + +* `AddMonoidAlgebra.divOf x g`: divides `x` by the monomial `AddMonoidAlgebra.of k G g` +* `AddMonoidAlgebra.modOf x g`: the remainder upon dividing `x` by the monomial + `AddMonoidAlgebra.of k G g`. + +## Main results + +* `AddMonoidAlgebra.divOf_add_modOf`, `AddMonoidAlgebra.modOf_add_divOf`: `divOf` and + `modOf` are well-behaved as quotient and remainder operators. + +## Implementation notes + +`∃ d, g' = g + d` is used as opposed to some other permutation up to commutativity in order to match +the definition of `semigroupDvd`. The results in this file could be duplicated for +`MonoidAlgebra` by using `g ∣ g'`, but this can't be done automatically, and in any case is not +likely to be very useful. + +-/ + + +variable {k G : Type _} [Semiring k] + +namespace AddMonoidAlgebra + +section + +variable [AddCancelCommMonoid G] + +/-- Divide by `of' k G g`, discarding terms not divisible by this. -/ +noncomputable def divOf (x : AddMonoidAlgebra k G) (g : G) : AddMonoidAlgebra k G := + -- note: comapping by `+ g` has the effect of subtracting `g` from every element in + -- the support, and discarding the elements of the support from which `g` can't be subtracted. + -- If `G` is an additive group, such as `ℤ` when used for `LaurentPolynomial`, + -- then no discarding occurs. + @Finsupp.comapDomain.addMonoidHom _ _ _ _ ((· + ·) g) (add_right_injective g) x +#align add_monoid_algebra.div_of AddMonoidAlgebra.divOf + +local infixl:70 " /ᵒᶠ " => divOf + +@[simp] +theorem divOf_apply (g : G) (x : AddMonoidAlgebra k G) (g' : G) : (x /ᵒᶠ g) g' = x (g + g') := + rfl +#align add_monoid_algebra.div_of_apply AddMonoidAlgebra.divOf_apply + +@[simp] +theorem support_divOf (g : G) (x : AddMonoidAlgebra k G) : + (x /ᵒᶠ g).support = + x.support.preimage ((· + ·) g) (Function.Injective.injOn (add_right_injective g) _) := + rfl +#align add_monoid_algebra.support_div_of AddMonoidAlgebra.support_divOf + +@[simp] +theorem zero_divOf (g : G) : (0 : AddMonoidAlgebra k G) /ᵒᶠ g = 0 := + map_zero _ +#align add_monoid_algebra.zero_div_of AddMonoidAlgebra.zero_divOf + +@[simp] +theorem divOf_zero (x : AddMonoidAlgebra k G) : x /ᵒᶠ 0 = x := by + refine Finsupp.ext fun _ => ?_ -- porting note: `ext` doesn't work + simp only [AddMonoidAlgebra.divOf_apply, zero_add] +#align add_monoid_algebra.div_of_zero AddMonoidAlgebra.divOf_zero + +theorem add_divOf (x y : AddMonoidAlgebra k G) (g : G) : (x + y) /ᵒᶠ g = x /ᵒᶠ g + y /ᵒᶠ g := + map_add _ _ _ +#align add_monoid_algebra.add_div_of AddMonoidAlgebra.add_divOf + +theorem divOf_add (x : AddMonoidAlgebra k G) (a b : G) : x /ᵒᶠ (a + b) = x /ᵒᶠ a /ᵒᶠ b := by + refine Finsupp.ext fun _ => ?_ -- porting note: `ext` doesn't work + simp only [AddMonoidAlgebra.divOf_apply, add_assoc] +#align add_monoid_algebra.div_of_add AddMonoidAlgebra.divOf_add + +/-- A bundled version of `AddMonoidAlgebra.divOf`. -/ +@[simps] +noncomputable def divOfHom : Multiplicative G →* AddMonoid.End (AddMonoidAlgebra k G) where + toFun g := + { toFun := fun x => divOf x (Multiplicative.toAdd g) + map_zero' := zero_divOf _ + map_add' := fun x y => add_divOf x y (Multiplicative.toAdd g) } + map_one' := AddMonoidHom.ext divOf_zero + map_mul' g₁ g₂ := + AddMonoidHom.ext fun _x => + (congr_arg _ (add_comm (Multiplicative.toAdd g₁) (Multiplicative.toAdd g₂))).trans + (divOf_add _ _ _) +#align add_monoid_algebra.div_of_hom AddMonoidAlgebra.divOfHom + +theorem of'_mul_divOf (a : G) (x : AddMonoidAlgebra k G) : of' k G a * x /ᵒᶠ a = x := by + refine Finsupp.ext fun _ => ?_ -- porting note: `ext` doesn't work + rw [AddMonoidAlgebra.divOf_apply, of'_apply, single_mul_apply_aux, one_mul] + intro c + exact add_right_inj _ +#align add_monoid_algebra.of'_mul_div_of AddMonoidAlgebra.of'_mul_divOf + +theorem mul_of'_divOf (x : AddMonoidAlgebra k G) (a : G) : x * of' k G a /ᵒᶠ a = x := by + refine Finsupp.ext fun _ => ?_ -- porting note: `ext` doesn't work + rw [AddMonoidAlgebra.divOf_apply, of'_apply, mul_single_apply_aux, mul_one] + intro c + rw [add_comm] + exact add_right_inj _ +#align add_monoid_algebra.mul_of'_div_of AddMonoidAlgebra.mul_of'_divOf + +theorem of'_divOf (a : G) : of' k G a /ᵒᶠ a = 1 := by + simpa only [one_mul] using mul_of'_divOf (1 : AddMonoidAlgebra k G) a +#align add_monoid_algebra.of'_div_of AddMonoidAlgebra.of'_divOf + +/-- The remainder upon division by `of' k G g`. -/ +noncomputable def modOf (x : AddMonoidAlgebra k G) (g : G) : AddMonoidAlgebra k G := + x.filter fun g₁ => ¬∃ g₂, g₁ = g + g₂ +#align add_monoid_algebra.mod_of AddMonoidAlgebra.modOf + +local infixl:70 " %ᵒᶠ " => modOf + +@[simp] +theorem modOf_apply_of_not_exists_add (x : AddMonoidAlgebra k G) (g : G) (g' : G) + (h : ¬∃ d, g' = g + d) : (x %ᵒᶠ g) g' = x g' := + Finsupp.filter_apply_pos _ _ h +#align add_monoid_algebra.mod_of_apply_of_not_exists_add AddMonoidAlgebra.modOf_apply_of_not_exists_add + +@[simp] +theorem modOf_apply_of_exists_add (x : AddMonoidAlgebra k G) (g : G) (g' : G) + (h : ∃ d, g' = g + d) : (x %ᵒᶠ g) g' = 0 := + Finsupp.filter_apply_neg _ _ <| by rwa [Classical.not_not] +#align add_monoid_algebra.mod_of_apply_of_exists_add AddMonoidAlgebra.modOf_apply_of_exists_add + +@[simp] +theorem modOf_apply_add_self (x : AddMonoidAlgebra k G) (g : G) (d : G) : (x %ᵒᶠ g) (d + g) = 0 := + modOf_apply_of_exists_add _ _ _ ⟨_, add_comm _ _⟩ +#align add_monoid_algebra.mod_of_apply_add_self AddMonoidAlgebra.modOf_apply_add_self + +-- @[simp] -- Porting note: simp can prove this +theorem modOf_apply_self_add (x : AddMonoidAlgebra k G) (g : G) (d : G) : (x %ᵒᶠ g) (g + d) = 0 := + modOf_apply_of_exists_add _ _ _ ⟨_, rfl⟩ +#align add_monoid_algebra.mod_of_apply_self_add AddMonoidAlgebra.modOf_apply_self_add + +theorem of'_mul_modOf (g : G) (x : AddMonoidAlgebra k G) : of' k G g * x %ᵒᶠ g = 0 := by + refine Finsupp.ext fun g' => ?_ -- porting note: `ext g'` doesn't work + rw [Finsupp.zero_apply] + obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d) + · rw [modOf_apply_self_add] + · rw [modOf_apply_of_not_exists_add _ _ _ h, of'_apply, single_mul_apply_of_not_exists_add _ _ h] +#align add_monoid_algebra.of'_mul_mod_of AddMonoidAlgebra.of'_mul_modOf + +theorem mul_of'_modOf (x : AddMonoidAlgebra k G) (g : G) : x * of' k G g %ᵒᶠ g = 0 := by + refine Finsupp.ext fun g' => ?_ -- porting note: `ext g'` doesn't work + rw [Finsupp.zero_apply] + obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d) + · rw [modOf_apply_self_add] + · rw [modOf_apply_of_not_exists_add _ _ _ h, of'_apply, mul_single_apply_of_not_exists_add] + simpa only [add_comm] using h +#align add_monoid_algebra.mul_of'_mod_of AddMonoidAlgebra.mul_of'_modOf + +theorem of'_modOf (g : G) : of' k G g %ᵒᶠ g = 0 := by + simpa only [one_mul] using mul_of'_modOf (1 : AddMonoidAlgebra k G) g +#align add_monoid_algebra.of'_mod_of AddMonoidAlgebra.of'_modOf + +theorem divOf_add_modOf (x : AddMonoidAlgebra k G) (g : G) : + of' k G g * (x /ᵒᶠ g) + x %ᵒᶠ g = x := by + refine Finsupp.ext fun g' => ?_ -- porting note: `ext` doesn't work + rw [Finsupp.add_apply] -- porting note: changed from `simp_rw` which can't see through the type + obtain ⟨d, rfl⟩ | h := em (∃ d, g' = g + d) + swap + · rw [modOf_apply_of_not_exists_add x _ _ h, of'_apply, single_mul_apply_of_not_exists_add _ _ h, + zero_add] + · rw [modOf_apply_self_add, add_zero] + rw [of'_apply, single_mul_apply_aux _ _ _, one_mul, divOf_apply] + intro a + exact add_right_inj _ +#align add_monoid_algebra.div_of_add_mod_of AddMonoidAlgebra.divOf_add_modOf + +theorem modOf_add_divOf (x : AddMonoidAlgebra k G) (g : G) : x %ᵒᶠ g + of' k G g * (x /ᵒᶠ g) = x := + by rw [add_comm, divOf_add_modOf] +#align add_monoid_algebra.mod_of_add_div_of AddMonoidAlgebra.modOf_add_divOf + +theorem of'_dvd_iff_modOf_eq_zero {x : AddMonoidAlgebra k G} {g : G} : + of' k G g ∣ x ↔ x %ᵒᶠ g = 0 := by + constructor + · rintro ⟨x, rfl⟩ + rw [of'_mul_modOf] + · intro h + rw [← divOf_add_modOf x g, h, add_zero] + exact dvd_mul_right _ _ +#align add_monoid_algebra.of'_dvd_iff_mod_of_eq_zero AddMonoidAlgebra.of'_dvd_iff_modOf_eq_zero + +end + +end AddMonoidAlgebra