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 LaurentPolynomials), 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.

noncomputable def AddMonoidAlgebra.divOf {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (x : AddMonoidAlgebra k G) (g : G) : AddMonoidAlgebra k G

Divide by of' k G g, discarding terms not divisible by this.

Equations

• AddMonoidAlgebra.divOf x g = ↑(Finsupp.comapDomain.addMonoidHom (_ : Function.Injective ((fun x x_1 => x + x_1) g))) x

@[simp]

theorem AddMonoidAlgebra.divOf_apply {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (g : G) (x : AddMonoidAlgebra k G) (g' : G) : ↑(AddMonoidAlgebra.divOf x g) g' = ↑x (g + g')

@[simp]

theorem AddMonoidAlgebra.support_divOf {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (g : G) (x : AddMonoidAlgebra k G) : (AddMonoidAlgebra.divOf x g).support = Finset.preimage x.support ((fun x x_1 => x + x_1) g) (_ : Set.InjOn ((fun x x_1 => x + x_1) g) ((fun x x_1 => x + x_1) g ⁻¹' ↑x.support))

@[simp]

theorem AddMonoidAlgebra.zero_divOf {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (g : G) : AddMonoidAlgebra.divOf 0 g = 0

@[simp]

theorem AddMonoidAlgebra.divOf_zero {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (x : AddMonoidAlgebra k G) : AddMonoidAlgebra.divOf x 0 = x

theorem AddMonoidAlgebra.add_divOf {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (x : AddMonoidAlgebra k G) (y : AddMonoidAlgebra k G) (g : G) : AddMonoidAlgebra.divOf (x + y) g = AddMonoidAlgebra.divOf x g + AddMonoidAlgebra.divOf y g

theorem AddMonoidAlgebra.divOf_add {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (x : AddMonoidAlgebra k G) (a : G) (b : G) : AddMonoidAlgebra.divOf x (a + b) = AddMonoidAlgebra.divOf (AddMonoidAlgebra.divOf x a) b

@[simp]

theorem AddMonoidAlgebra.divOfHom_apply_apply {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (g : Multiplicative G) (x : AddMonoidAlgebra k G) : ↑(↑AddMonoidAlgebra.divOfHom g) x = AddMonoidAlgebra.divOf x (↑Multiplicative.toAdd g)

noncomputable def AddMonoidAlgebra.divOfHom {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] : Multiplicative G →* AddMonoid.End (AddMonoidAlgebra k G)

A bundled version of AddMonoidAlgebra.divOf.

Equations

• One or more equations did not get rendered due to their size.

theorem AddMonoidAlgebra.of'_mul_divOf {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (a : G) (x : AddMonoidAlgebra k G) : AddMonoidAlgebra.divOf (AddMonoidAlgebra.of' k G a * x) a = x

theorem AddMonoidAlgebra.mul_of'_divOf {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (x : AddMonoidAlgebra k G) (a : G) : AddMonoidAlgebra.divOf (x * AddMonoidAlgebra.of' k G a) a = x

theorem AddMonoidAlgebra.of'_divOf {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (a : G) : AddMonoidAlgebra.divOf (AddMonoidAlgebra.of' k G a) a = 1

noncomputable def AddMonoidAlgebra.modOf {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (x : AddMonoidAlgebra k G) (g : G) : AddMonoidAlgebra k G

The remainder upon division by of' k G g.

Equations

• AddMonoidAlgebra.modOf x g = Finsupp.filter (fun g₁ => ¬∃ g₂, g₁ = g + g₂) x

@[simp]

theorem AddMonoidAlgebra.modOf_apply_of_not_exists_add {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (x : AddMonoidAlgebra k G) (g : G) (g' : G) (h : ¬∃ d, g' = g + d) : ↑(AddMonoidAlgebra.modOf x g) g' = ↑x g'

@[simp]

theorem AddMonoidAlgebra.modOf_apply_of_exists_add {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (x : AddMonoidAlgebra k G) (g : G) (g' : G) (h : ∃ d, g' = g + d) : ↑(AddMonoidAlgebra.modOf x g) g' = 0

@[simp]

theorem AddMonoidAlgebra.modOf_apply_add_self {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (x : AddMonoidAlgebra k G) (g : G) (d : G) : ↑(AddMonoidAlgebra.modOf x g) (d + g) = 0

theorem AddMonoidAlgebra.modOf_apply_self_add {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (x : AddMonoidAlgebra k G) (g : G) (d : G) : ↑(AddMonoidAlgebra.modOf x g) (g + d) = 0

theorem AddMonoidAlgebra.of'_mul_modOf {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (g : G) (x : AddMonoidAlgebra k G) : AddMonoidAlgebra.modOf (AddMonoidAlgebra.of' k G g * x) g = 0

theorem AddMonoidAlgebra.mul_of'_modOf {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (x : AddMonoidAlgebra k G) (g : G) : AddMonoidAlgebra.modOf (x * AddMonoidAlgebra.of' k G g) g = 0

theorem AddMonoidAlgebra.of'_modOf {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (g : G) : AddMonoidAlgebra.modOf (AddMonoidAlgebra.of' k G g) g = 0

theorem AddMonoidAlgebra.divOf_add_modOf {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (x : AddMonoidAlgebra k G) (g : G) : AddMonoidAlgebra.of' k G g * AddMonoidAlgebra.divOf x g + AddMonoidAlgebra.modOf x g = x

theorem AddMonoidAlgebra.modOf_add_divOf {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] (x : AddMonoidAlgebra k G) (g : G) : AddMonoidAlgebra.modOf x g + AddMonoidAlgebra.of' k G g * AddMonoidAlgebra.divOf x g = x

theorem AddMonoidAlgebra.of'_dvd_iff_modOf_eq_zero {k : Type u_1} {G : Type u_2} [Semiring k] [AddCancelCommMonoid G] {x : AddMonoidAlgebra k G} {g : G} : AddMonoidAlgebra.of' k G g ∣ x ↔ AddMonoidAlgebra.modOf x g = 0