Free modules

We construct the free module over a ring R generated by a set X. It is assumed that both R and X have decidable equality. This is to obtain decidable equality for the elements of the module, which we do (FreeModule.decEq). We choose our definition to allow both such computations and to prove results.

The definition is as a quotient of Formal Sums (FormalSum), which are simply lists of pairs (a, x) where a is a coefficient in R and x is a term in X. We associate to such a formal sum a coordinate function X → R (FormalSum.coords). We see that having the same coordinate functions gives an equivalence relation on the formal sums. The free module (FreeModule) is then defined as the corresponding quotient of such formal sums.

We also give an alternative description via moves, which is more convenient for universal properties.

Formal sums

@[reducible, inline]

abbrev LeanPool.Polylean.FormalSum (R : Type u_1) (X : Type u_2) [Ring R] : Type (max u_2 u_1)

A formal sum represents an R-linear combination of finitely many elements of X. This is implemented as a list R × X, which associates to each element X of the list a coefficient from R.

Equations

• LeanPool.Polylean.FormalSum R X = List (R × X)

Coordinate functions and Supports

• We define coordinate functions X → R for formal sums.
• We define (weak) support, relate non-zero coordinates.
• We prove decidable equality on a list (easy fact).

Coordinate functions

The definition of coordinate functions is in two steps. We first define the coordinate for a pair (a, x), and then define the coordinate function for a formal sum by summing over such terms.

def LeanPool.Polylean.monomCoeff (R : Type u_1) (X : Type u_2) [Ring R] [DecidableEq X] (x₀ : X) (nx : R × X) : R

Coordinates for a formal sum with one term.

Equations

• LeanPool.Polylean.monomCoeff R X x₀ nx = match nx.snd == x₀ with | true => nx.fst | false => 0

theorem LeanPool.Polylean.monom_coords_hom {R : Type u_1} [Ring R] {X : Type u_2} [DecidableEq X] (x₀ x : X) (a b : R) : monomCoeff R X x₀ (a + b, x) = monomCoeff R X x₀ (a, x) + monomCoeff R X x₀ (b, x)

Homomorphism property for coordinates for a formal sum with one term.

theorem LeanPool.Polylean.monom_coords_mul {R : Type u_1} [Ring R] {X : Type u_2} [DecidableEq X] {x : X} (x₀ : X) (a b : R) : monomCoeff R X x₀ (a * b, x) = a * monomCoeff R X x₀ (b, x)

Associativity of scalar multiplication coordinates for a formal sum with one term.

theorem LeanPool.Polylean.monom_coords_at_zero {R : Type u_1} [Ring R] {X : Type u_2} [DecidableEq X] (x₀ x : X) : monomCoeff R X x₀ (0, x) = 0

Coordinates for a formal sum with one term with scalar 0.

def LeanPool.Polylean.FormalSum.coords {R : Type u_1} [Ring R] {X : Type u_2} [DecidableEq X] : FormalSum R X → X → R

The coordinates for a formal sum.

Equations

• LeanPool.Polylean.FormalSum.coords [] x✝ = 0
• LeanPool.Polylean.FormalSum.coords (h :: t) x✝ = LeanPool.Polylean.monomCoeff R X x✝ h + LeanPool.Polylean.FormalSum.coords t x✝

Support of a formal sum

We next define the support of a formal sum and prove the property that coordinates vanish outside the support.

def LeanPool.Polylean.FormalSum.support {R : Type u_1} [Ring R] {X : Type u_2} (s : FormalSum R X) : List X

Support for a formal sum in a weak sense (coordinates may vanish on this).

Equations

• s.support = List.map (fun (x : R × X) => match x with | (fst, x) => x) s

theorem LeanPool.Polylean.nonzero_coord_in_support {R : Type u_1} [Ring R] {X : Type u_2} [DecidableEq X] (s : FormalSum R X) (x : X) : 0 ≠ s.coords x → x ∈ s.support

Support contains elements x : X where the coordinate is not 0.

Equality of coordinates on a list

We define equality of coordinates on a list and prove that it is decidable and implied by equality of formal sums.

def LeanPool.Polylean.equalOnList {R : Type u_1} {X : Type u_2} (l : List X) (f g : X → R) : Prop

The condition of being equal on all elements is a given list

Equations

• LeanPool.Polylean.equalOnList [] f g = (true = true)
• LeanPool.Polylean.equalOnList (h :: t) f g = (f h = g h ∧ LeanPool.Polylean.equalOnList t f g)

theorem LeanPool.Polylean.equalOnList_of_equal {R : Type u_2} {X : Type u_1} (l : List X) (f g : X → R) : f = g → equalOnList l f g

Equal functions are equal on arbitrary supports.

theorem LeanPool.Polylean.eq_mem_of_equalOnList {R : Type u_2} {X : Type u_1} (l : List X) (f g : X → R) (x : X) (mhyp : x ∈ l) : equalOnList l f g → f x = g x

Functions equal on support l are equal on each x ∈ l.

@[reducible]

instance LeanPool.Polylean.decidableEqualOnList {R : Type u_1} [DecidableEq R] {X : Type u_2} (l : List X) (f g : X → R) : Decidable (equalOnList l f g)

Decidability of equality on list.

Equations

• One or more equations did not get rendered due to their size.
• LeanPool.Polylean.decidableEqualOnList [] f g = isTrue LeanPool.Polylean.decidableEqualOnList._proof_1

Quotient Free Module

• We define relation by having equal coordinates
• We show this is an equivalence relation and define the quotient

def LeanPool.Polylean.eqlCoords (R X : Type) [Ring R] [DecidableEq X] (s₁ s₂ : FormalSum R X) : Prop

Relation by equal coordinates.

Equations

• LeanPool.Polylean.eqlCoords R X s₁ s₂ = (s₁.coords = s₂.coords)

theorem LeanPool.Polylean.eqlCoords.refl {R : Type} [Ring R] {X : Type} [DecidableEq X] (s : FormalSum R X) : eqlCoords R X s s

Relation by equal coordinates is reflexive.

theorem LeanPool.Polylean.eqlCoords.symm {R : Type} [Ring R] {X : Type} [DecidableEq X] {s₁ s₂ : FormalSum R X} : eqlCoords R X s₁ s₂ → eqlCoords R X s₂ s₁

Relation by equal coordinates is symmetric.

theorem LeanPool.Polylean.eqlCoords.trans {R : Type} [Ring R] {X : Type} [DecidableEq X] {s₁ s₂ s₃ : FormalSum R X} : eqlCoords R X s₁ s₂ → eqlCoords R X s₂ s₃ → eqlCoords R X s₁ s₃

Relation by equal coordinates is transitive.

theorem LeanPool.Polylean.eqlCoords.is_equivalence {R : Type} [Ring R] {X : Type} [DecidableEq X] : Equivalence (eqlCoords R X)

Relation by equal coordinates is an equivalence relation.

@[implicit_reducible]

instance LeanPool.Polylean.formalSumSetoid (R X : Type) [Ring R] [DecidableEq X] [DecidableEq R] : Setoid (FormalSum R X)

Setoid based on equal coordinates.

Equations

• LeanPool.Polylean.formalSumSetoid R X = { r := LeanPool.Polylean.eqlCoords R X, iseqv := ⋯ }

@[reducible, inline]

abbrev LeanPool.Polylean.FreeModule (R X : Type) [Ring R] [DecidableEq X] [DecidableEq R] : Type

Quotient free module.

Equations

• R[X] = Quotient (LeanPool.Polylean.formalSumSetoid R X)

def LeanPool.Polylean.«term_[_]» : Lean.TrailingParserDescr

Notation for the quotient free module over R generated by G.

Equations

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

Decidable equality on quotient free modules

We show that the free module F[X] has decidable equality. This has two steps:

• show decidable equality for images of formal sums.
• lift to quotient (by relating to formal sums).

We also show that the coordinate functions are defined on the quotient.

theorem LeanPool.Polylean.FreeModule.eqlquot_of_equalOnList {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (s₁ s₂ : FormalSum R X) (ch₁ : equalOnList s₁.support s₁.coords s₂.coords) (ch₂ : equalOnList s₂.support s₁.coords s₂.coords) : ⟦s₁⟧ = ⟦s₂⟧

Equality on both supports gives equal quotients.

@[reducible]

instance LeanPool.Polylean.FreeModule.decideEqualQuotient {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (s₁ s₂ : FormalSum R X) : Decidable (⟦s₁⟧ = ⟦s₂⟧)

Decidable equality for quotient elements in the free module

Equations

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

Lift to quotient

def LeanPool.Polylean.FreeModule.beqOnSupport {R : Type u_1} [DecidableEq R] {X : Type u_2} (l : List X) (f g : X → R) : Bool

Boolean equality on support.

Equations

• LeanPool.Polylean.FreeModule.beqOnSupport l f g = l.all fun (x : X) => decide (f x = g x)

theorem LeanPool.Polylean.FreeModule.eql_on_support_of_true {R : Type u_2} [DecidableEq R] {X : Type u_1} {l : List X} {f g : X → R} : beqOnSupport l f g = true → equalOnList l f g

Equality on support from boolean equality.

theorem LeanPool.Polylean.FreeModule.eqlquot_of_beq_support {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (s₁ s₂ : FormalSum R X) (c₁ : beqOnSupport s₁.support s₁.coords s₂.coords = true) (c₂ : beqOnSupport s₂.support s₁.coords s₂.coords = true) : ⟦s₁⟧ = ⟦s₂⟧

Boolean equality on support gives equal quotients.

def LeanPool.Polylean.FreeModule.beqQuot {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (x₁ x₂ : R[X]) : Bool

Boolean equality for the quotient via lifting

Equations

• LeanPool.Polylean.FreeModule.beqQuot = Quotient.lift₂ (fun (s₁ s₂ : LeanPool.Polylean.FormalSum R X) => decide (⟦s₁⟧ = ⟦s₂⟧)) ⋯

theorem LeanPool.Polylean.FreeModule.eq_of_beq_true {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (x₁ x₂ : R[X]) : x₁.beqQuot x₂ = true → x₁ = x₂

Boolean equality for the quotient is equality.

theorem LeanPool.Polylean.FreeModule.neq_of_beq_false {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (x₁ x₂ : R[X]) : x₁.beqQuot x₂ = false → ¬x₁ = x₂

Boolean inequality for the quotient is inequality.

@[reducible]

instance LeanPool.Polylean.FreeModule.decEq {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (x₁ x₂ : R[X]) : Decidable (x₁ = x₂)

Decidable equality for the free module.

Equations

• x₁.decEq x₂ = match p : x₁.beqQuot x₂ with | true => isTrue ⋯ | false => isFalse ⋯

Induced coordinates on the quotient.

theorem LeanPool.Polylean.FreeModule.equal_coords_of_approx {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (s₁ s₂ : FormalSum R X) : s₁ ≈ s₂ → s₁.coords = s₂.coords

Coordinates are well defined on the quotient.

def LeanPool.Polylean.FreeModule.coordinates {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (x₀ : X) : R[X] → R

coordinates for the quotient

Equations

• LeanPool.Polylean.FreeModule.coordinates x₀ = Quotient.lift (fun (s : LeanPool.Polylean.FormalSum R X) => s.coords x₀) ⋯

Module structure

We define the module structure on the quotient of the free module by the equivalence relation.

• We define scalar multiplication and addition on formal sums.
• We show that we have induced operations on the quotient.
• We show that the induced operations give a module structure on the quotient.

Scalar multiplication: on formal sums and on the quotient.

def LeanPool.Polylean.FormalSum.scmul {R : Type u_1} [Ring R] {X : Type u_2} : R → FormalSum R X → FormalSum R X

Scalar multiplication on formal sums.

Equations

• LeanPool.Polylean.FormalSum.scmul x✝ [] = []
• LeanPool.Polylean.FormalSum.scmul x✝ ((fst, x_3) :: t) = (x✝ * fst, x_3) :: LeanPool.Polylean.FormalSum.scmul x✝ t

theorem LeanPool.Polylean.FormalSum.scmul_coords {R : Type u_1} [Ring R] {X : Type u_2} [DecidableEq X] (r : R) (s : FormalSum R X) (x₀ : X) : r * s.coords x₀ = (scmul r s).coords x₀

Coordinates after scalar multiplication.

def LeanPool.Polylean.FreeModule.scmul {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] : R → R[X] → R[X]

Scalar multiplication on the Free Module.

Equations

• LeanPool.Polylean.FreeModule.scmul r = Quotient.lift (fun (s : LeanPool.Polylean.FormalSum R X) => ⟦LeanPool.Polylean.FormalSum.scmul r s⟧) ⋯

Addition: on formal sums and on the quotient.

theorem LeanPool.Polylean.FormalSum.append_coords {R : Type u_1} [Ring R] {X : Type u_2} [DecidableEq X] (s₁ s₂ : FormalSum R X) (x₀ : X) : s₁.coords x₀ + s₂.coords x₀ = (s₁ ++ s₂).coords x₀

Coordinates add when appending.

theorem LeanPool.Polylean.FormalSum.append_equiv {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (s₁ s₂ t₁ t₂ : FormalSum R X) : s₁ ≈ s₂ → t₁ ≈ t₂ → s₁ ++ t₁ ≈ s₂ ++ t₂

Coordinates well-defined up to equivalence.

def LeanPool.Polylean.FreeModule.add {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] : R[X] → R[X] → R[X]

Addition of elements in the free module.

Equations

• LeanPool.Polylean.FreeModule.add = Quotient.lift₂ (fun (s₁ s₂ : LeanPool.Polylean.FormalSum R X) => ⟦s₁ ++ s₂⟧) ⋯

@[implicit_reducible]

instance LeanPool.Polylean.instAddFreeModule {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] : Add (R[X])

Equations

• LeanPool.Polylean.instAddFreeModule = { add := LeanPool.Polylean.FreeModule.add }

@[implicit_reducible]

instance LeanPool.Polylean.instHSMulFreeModule {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] : HSMul R (R[X]) (R[X])

Equations

• LeanPool.Polylean.instHSMulFreeModule = { hSMul := LeanPool.Polylean.FreeModule.scmul }

Properties of operations on formal sums.

theorem LeanPool.Polylean.FormalSum.action {R : Type u_1} [Ring R] {X : Type u_2} (a b : R) (s : FormalSum R X) : scmul a (scmul b s) = scmul (a * b) s

Associativity for scalar multiplication for formal sums.

theorem LeanPool.Polylean.FormalSum.act_sum {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (a b : R) (s : FormalSum R X) : scmul a s ++ scmul b s ≈ scmul (a + b) s

Distributivity for the module operations.

Module properties for the free module.

theorem LeanPool.Polylean.FreeModule.module_action {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (a b : R) (x : R[X]) : a • b • x = (a * b) • x

Associativity for scalar and ring products.

theorem LeanPool.Polylean.FreeModule.addn_comm {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (x₁ x₂ : R[X]) : x₁ + x₂ = x₂ + x₁

Commutativity of addition.

theorem LeanPool.Polylean.FreeModule.add_assoc_aux {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (s₁ : FormalSum R X) (x₂ x₃ : R[X]) : ⟦s₁⟧ + x₂ + x₃ = ⟦s₁⟧ + (x₂ + x₃)

theorem LeanPool.Polylean.FreeModule.addn_assoc {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (x₁ x₂ x₃ : R[X]) : x₁ + x₂ + x₃ = x₁ + (x₂ + x₃)

Associativity of addition.

def LeanPool.Polylean.FreeModule.zero {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] : R[X]

The zero element of the free module.

Equations

• LeanPool.Polylean.FreeModule.zero = ⟦[]⟧

theorem LeanPool.Polylean.FreeModule.addn_zero {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (x : R[X]) : x + zero = x

adding zero

theorem LeanPool.Polylean.FreeModule.zero_addn {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (x : R[X]) : zero + x = x

adding zero

theorem LeanPool.Polylean.FreeModule.elem_distrib {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (a : R) (x₁ x₂ : R[X]) : a • (x₁ + x₂) = a • x₁ + a • x₂

Distributivity for addition of module elements.

theorem LeanPool.Polylean.FreeModule.coeffs_distrib {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (a b : R) (x : R[X]) : a • x + b • x = (a + b) • x

Distributivity with respect to scalars.

theorem LeanPool.Polylean.FreeModule.unit_coeffs {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (x : R[X]) : 1 • x = x

Multiplication by 1 : R.

theorem LeanPool.Polylean.FreeModule.zero_coeffs {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (x : R[X]) : 0 • x = ⟦[]⟧

Multiplication by 0 : R.

@[implicit_reducible]

instance LeanPool.Polylean.FreeModule.instZero {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] : Zero (R[X])

Equations

• LeanPool.Polylean.FreeModule.instZero = { zero := LeanPool.Polylean.FreeModule.zero }

@[implicit_reducible]

instance LeanPool.Polylean.FreeModule.instNeg {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] : Neg (R[X])

Equations

• LeanPool.Polylean.FreeModule.instNeg = { neg := fun (x : R[X]) => -1 • x }

@[implicit_reducible]

instance LeanPool.Polylean.FreeModule.instAddCommGroup {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] : AddCommGroup (R[X])

The module is an additive commutative group, mainly proved as a check

Equations

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

Equivalent definition of the relation via moves

For conceptual results such as the universal property (needed for the group ring structure) it is useful to define the relation on the free module in terms of moves. We do this, and show that this is the same as the relation defined by equality of coordinates.

• We define elementary moves on formal sums
• We show coordinates equal if and only if related by elementary moves
• Hence can define map on Free Module when invariant under elementary moves

inductive LeanPool.Polylean.ElementaryMove (R X : Type) [Ring R] [DecidableEq R] [DecidableEq X] : FormalSum R X → FormalSum R X → Prop

Elementary moves for formal sums.

• zeroCoeff {R X : Type} [Ring R] [DecidableEq R] [DecidableEq X] (tail : FormalSum R X) (x : X) (a : R) (h : a = 0) : ElementaryMove R X ((a, x) :: tail) tail
• addCoeffs {R X : Type} [Ring R] [DecidableEq R] [DecidableEq X] (a b : R) (x : X) (tail : FormalSum R X) : ElementaryMove R X ((a, x) :: (b, x) :: tail) ((a + b, x) :: tail)
• cons {R X : Type} [Ring R] [DecidableEq R] [DecidableEq X] (a : R) (x : X) (s₁ s₂ : FormalSum R X) : ElementaryMove R X s₁ s₂ → ElementaryMove R X ((a, x) :: s₁) ((a, x) :: s₂)
• swap {R X : Type} [Ring R] [DecidableEq R] [DecidableEq X] (a₁ a₂ : R) (x₁ x₂ : X) (tail : FormalSum R X) : ElementaryMove R X ((a₁, x₁) :: (a₂, x₂) :: tail) ((a₂, x₂) :: (a₁, x₁) :: tail)

def LeanPool.Polylean.FreeModuleAux (R X : Type) [Ring R] [DecidableEq R] [DecidableEq X] : Type

Free module quotient using elementary moves on formal sums.

Equations

• LeanPool.Polylean.FreeModuleAux R X = Quot (LeanPool.Polylean.ElementaryMove R X)

def LeanPool.Polylean.FormalSum.sum {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (s : FormalSum R X) : FreeModuleAux R X

Image in the quotient (i.e., actual, not formal, sum).

Equations

• s.sum = Quot.mk (LeanPool.Polylean.ElementaryMove R X) s

def LeanPool.Polylean.FormalSum.equiv {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (s₁ s₂ : FormalSum R X) : Prop

Equivalence by having the same image.

Equations

• s₁ ≃ s₂ = (s₁.sum = s₂.sum)

def LeanPool.Polylean.FormalSum.«term_≃_» : Lean.TrailingParserDescr

Infix notation for equivalence by elementary moves.

Equations

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

Invariance of coordinates under elementary moves

theorem LeanPool.Polylean.FormalSum.coords_move_invariant {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (x₀ : X) (s₁ s₂ : FormalSum R X) (h : ElementaryMove R X s₁ s₂) : s₁.coords x₀ = s₂.coords x₀

Coordinates are invariant under moves.

def LeanPool.Polylean.FreeModuleAux.coeff {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (x₀ : X) : FreeModuleAux R X → R

Coordinates on the quotients.

Equations

• LeanPool.Polylean.FreeModuleAux.coeff x₀ = Quot.lift (fun (s : LeanPool.Polylean.FormalSum R X) => s.coords x₀) ⋯

theorem LeanPool.Polylean.FormalSum.coeff_factors {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (x : X) (s : FormalSum R X) : FreeModuleAux.coeff x s.sum = s.coords x

Commutative diagram for coordinates.

theorem LeanPool.Polylean.FormalSum.coords_well_defined {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (x : X) (s₁ s₂ : FormalSum R X) : s₁ ≃ s₂ → s₁.coords x = s₂.coords x

Coordinates well-defined under the equivalence generated by moves.

Equal coordinates implies related by elementary moves.

theorem LeanPool.Polylean.FormalSum.cons_equiv_of_equiv {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (s₁ s₂ : FormalSum R X) (a : R) (x : X) : s₁ ≃ s₂ → (a, x) :: s₁ ≃ (a, x) :: s₂

Cons respects equivalence.

theorem LeanPool.Polylean.FormalSum.nonzero_coeff_has_complement {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (x₀ : X) (s : FormalSum R X) : 0 ≠ s.coords x₀ → ∃ (ys : FormalSum R X), (s.coords x₀, x₀) :: ys ≃ s ∧ List.length ys < List.length s

If a coordinate x for a formal sum s is non-zero, s is related by moves to a formal sum with first term x with coefficient its coordinates, and the rest shorter than s.

theorem LeanPool.Polylean.FormalSum.equiv_e_of_zero_coeffs {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (s : FormalSum R X) (hyp : ∀ (x : X), s.coords x = 0) : s ≃ []

If all coordinates are zero, then moves relate to the empty sum.

theorem LeanPool.Polylean.FormalSum.equiv_of_equal_coeffs {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (s₁ s₂ : FormalSum R X) (hyp : ∀ (x : X), s₁.coords x = s₂.coords x) : s₁ ≃ s₂

If coordinates are equal, the sums are related by moves.

Functions invariant under moves pass to the quotient.

theorem LeanPool.Polylean.FormalSum.func_eql_of_move_equiv {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] {β : Sort u} (f : FormalSum R X → β) : (∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → f s₁ = f s₂) → ∀ (s₁ s₂ : FormalSum R X), s₁ ≈ s₂ → f s₁ = f s₂

Lifting functions to the move induced quotient.

Injectivity of inclusions

We show that, under appropriate hypotheses, two inclusions into Free Modules are injective.

• If a : R is nonzero, then x : X ↦ ⟦[(a, x)]⟧ is injective.
• If x: X, then a : R ↦ ⟦[(a, x)]⟧ is injective.

These are used in proving injectivity results for related functions on group rings, which act as a check on the correctness of the definitions.

theorem LeanPool.Polylean.monom_elem_eq_of_coord_eq_nonzero {R : Type u_1} [Ring R] {X : Type u_2} [DecidableEq X] (a : R) (non_zero : a ≠ 0) (x₀ x₁ : X) : FormalSum.coords [(a, x₀)] = FormalSum.coords [(a, x₁)] → x₀ = x₁

For a : R and a ≠ 0, injectivity of the function x : X ↦ [(a, x)] up to equivalence.

theorem LeanPool.Polylean.monom_coeff_eq_of_coord_eq {R : Type u_1} [Ring R] {X : Type u_2} [DecidableEq X] (x : X) (a₀ a₁ : R) : FormalSum.coords [(a₀, x)] = FormalSum.coords [(a₁, x)] → a₀ = a₁

For x : X, injectivity of the function a : R ↦ [(a, x)] up to equivalence.

def LeanPool.Polylean.coeffInclusion {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (x₀ : X) : R → R[X]

For x: X, the functions a : R ↦ ⟦[(a, x)]⟧

Equations

• LeanPool.Polylean.coeffInclusion x₀ a₀ = ⟦[(a₀, x₀)]⟧

theorem LeanPool.Polylean.coeffInclusion_injective {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (x₀ : X) (a₀ a₁ : R) : coeffInclusion x₀ a₀ = coeffInclusion x₀ a₁ → a₀ = a₁

Injectivity of coeffInclusion

def LeanPool.Polylean.baseInclusion {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (a₀ : R) : X → R[X]

For a: A, the function x: X ↦ ⟦[(a, x)]⟧

Equations

• LeanPool.Polylean.baseInclusion a₀ x₀ = ⟦[(a₀, x₀)]⟧

theorem LeanPool.Polylean.baseInclusion_injective {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (a₀ : R) (non_zero : a₀ ≠ 0) (x₀ x₁ : X) : baseInclusion a₀ x₀ = baseInclusion a₀ x₁ → x₀ = x₁

Injectivity of baseInclusion a give a ≠0

Basic Repr

An instance of Repr on Free Modules, mainly for debugging (fairly crude). This is implemented by constructing a norm ball containing all the non-zero coordinates, and then making a list of non-zero coordinates.

theorem LeanPool.Polylean.fst_le_max (a b : ℕ) : a ≤ max a b

theorem LeanPool.Polylean.snd_le_max (a b : ℕ) : b ≤ max a b

theorem LeanPool.Polylean.eq_fst_or_snd_of_max (a b : ℕ) : max a b = a ∨ max a b = b

def LeanPool.Polylean.maxNormSuccOnSupp {R : Type u_1} [Ring R] [DecidableEq R] {X : Type u_2} (norm : X → ℕ) (crds : X → R) (s : List X) : ℕ

The successor of the largest norm with nonzero coordinate on a support list.

Equations

• LeanPool.Polylean.maxNormSuccOnSupp norm crds [] = 0
• LeanPool.Polylean.maxNormSuccOnSupp norm crds (h :: t) = if crds h ≠ 0 then max (norm h + 1) (LeanPool.Polylean.maxNormSuccOnSupp norm crds t) else LeanPool.Polylean.maxNormSuccOnSupp norm crds t

theorem LeanPool.Polylean.max_in_support {R : Type u_2} [Ring R] [DecidableEq R] {X : Type u_1} (norm : X → ℕ) (crds : X → R) (s : List X) : maxNormSuccOnSupp norm crds s > 0 → ∃ (x : X), crds x ≠ 0 ∧ maxNormSuccOnSupp norm crds s = norm x + 1

theorem LeanPool.Polylean.supp_below_max {R : Type u_2} [Ring R] [DecidableEq R] {X : Type u_1} (norm : X → ℕ) (crds : X → R) (s : List X) (x : X) : x ∈ s → crds x ≠ 0 → norm x + 1 ≤ maxNormSuccOnSupp norm crds s

theorem LeanPool.Polylean.supp_zero_of_max_zero {R : Type u_2} [Ring R] [DecidableEq R] {X : Type u_1} (norm : X → ℕ) (crds : X → R) (s : List X) : maxNormSuccOnSupp norm crds s = 0 → ∀ (x : X), x ∈ s → crds x = 0

def LeanPool.Polylean.FormalSum.normSucc {R : Type u_1} [Ring R] [DecidableEq R] {X : Type u_2} [DecidableEq X] (norm : X → ℕ) (s : FormalSum R X) : ℕ

The successor of the largest norm with nonzero coefficient in a formal sum.

Equations

• LeanPool.Polylean.FormalSum.normSucc norm s = LeanPool.Polylean.maxNormSuccOnSupp norm s.coords s.support

theorem LeanPool.Polylean.normsucc_le {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (norm : X → ℕ) (s₁ s₂ : FormalSum R X) (eql : s₁ ≈ s₂) : FormalSum.normSucc norm s₁ ≤ FormalSum.normSucc norm s₂

theorem LeanPool.Polylean.norm_succ_eq {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (norm : X → ℕ) (s₁ s₂ : FormalSum R X) (eql : s₁ ≈ s₂) : FormalSum.normSucc norm s₁ = FormalSum.normSucc norm s₂

class LeanPool.Polylean.NormCube (α : Type) : Type

Finite exhaustive approximations to a type, organized by a norm.

• norm : α → ℕ

  A size function on elements.

• cube : ℕ → List α

  Elements whose norm is bounded by a given natural number.

def LeanPool.Polylean.normCube (α : Type) [nc : NormCube α] (k : ℕ) : List α

The finite cube at radius k.

Equations

• LeanPool.Polylean.normCube α k = LeanPool.Polylean.NormCube.cube k

@[implicit_reducible]

instance LeanPool.Polylean.natCube : NormCube ℕ

Equations

• LeanPool.Polylean.natCube = { norm := id, cube := fun (n : ℕ) => (List.range n).reverse }

@[implicit_reducible]

instance LeanPool.Polylean.finCube {k : ℕ} : NormCube (Fin k.succ)

Equations

• LeanPool.Polylean.finCube = { norm := fun (j : Fin k.succ) => ↑j, cube := fun (n : ℕ) => List.map (fun (n : ℕ) => ⟨n % k.succ, ⋯⟩) (List.range (min (k + 1) n)).reverse }

@[implicit_reducible]

instance LeanPool.Polylean.intCube : NormCube ℤ

Equations

• LeanPool.Polylean.intCube = { norm := Int.natAbs, cube := fun (n : ℕ) => List.map Int.ofNat (List.range n).reverse ++ List.map Int.negSucc (List.range (n - 1)) }

@[implicit_reducible]

instance LeanPool.Polylean.prodCube {α β : Type} [na : NormCube α] [nb : NormCube β] : NormCube (α × β)

Equations

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

def LeanPool.Polylean.FreeModule.normBound {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (x : R[X]) [nx : NormCube X] : ℕ

A norm bound for the support of a quotient free-module element.

Equations

• x.normBound = Quotient.lift (fun (s : LeanPool.Polylean.FormalSum R X) => LeanPool.Polylean.FormalSum.normSucc LeanPool.Polylean.NormCube.norm s) ⋯ x

def LeanPool.Polylean.FreeModule.coeffList {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] (x : R[X]) [nx : NormCube X] : List (R × X)

The nonzero coefficients of a quotient free-module element in a bounded cube.

Equations

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

@[implicit_reducible]

instance LeanPool.Polylean.basicRepr {R : Type} [Ring R] [DecidableEq R] {X : Type} [DecidableEq X] [NormCube X] [Repr X] [Repr R] : Repr (R[X])

Equations

• LeanPool.Polylean.basicRepr = { reprPrec := fun (x : R[X]) (x_1 : ℕ) => Std.Format.text (reprStr x.coeffList) }