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

ink

@[inline]

abbrev FormalSum (R : Type u_1) (X : Type u_2) [inst : Ring R] : Type (maxu_2u_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

• 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.

ink

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

Coordinates for a formal sum with one term.

Equations

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

ink

theorem monom_coords_hom {R : Type u_1} [inst : Ring R] {X : Type u_2} [inst : DecidableEq X] (x₀ : X) (x : X) (a : R) (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.

ink

theorem monom_coords_mul {R : Type u_1} [inst : Ring R] {X : Type u_2} [inst : DecidableEq X] {x : X} (x₀ : X) (a : R) (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.

ink

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

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

ink

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

The coordinates for a formal sum.

Equations

• FormalSum.coords [] x = 0
• FormalSum.coords (h :: t) x = monomCoeff R X x h + 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.

ink

def FormalSum.support {R : Type u_1} [inst : 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

• FormalSum.support s = List.map (fun x => match x with | (fst, x) => x) s

ink

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

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.

ink

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

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

Equations

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

ink

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

Equal functions are equal on arbitrary supports.

ink

theorem eq_mem_of_equalOnList {R : Type u_2} {X : Type u_1} (l : List X) (f : X → R) (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.

ink

instance decidableEqualOnList {R : Type u_1} [inst : DecidableEq R] {X : Type u_2} (l : List X) (f : X → R) (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.
• decidableEqualOnList [] f g = isTrue (_ : true = true)

Quotient Free Module

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

ink

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

Relation by equal coordinates.

Equations

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

ink

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

Relation by equal coordinates is reflexive.

ink

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

Relation by equal coordinates is symmetric.

ink

theorem eqlCoords.trans {R : Type} [inst : Ring R] {X : Type} [inst : DecidableEq X] {s₁ : FormalSum R X} {s₂ : FormalSum R X} {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.

ink

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

Relation by equal coordinates is an equivalence relation.

ink

instance formalSumSetoid (R : Type) (X : Type) [inst : Ring R] [inst : DecidableEq X] : Setoid (FormalSum R X)

Setoid based on equal coordinates.

Equations

• formalSumSetoid R X = { r := eqlCoords R X, iseqv := (_ : Equivalence (eqlCoords R X)) }

ink

@[inline]

abbrev FreeModule (R : Type) (X : Type) [inst : Ring R] [inst : DecidableEq X] : Type

Quotient free module.

Equations

• R[X] = Quotient (formalSumSetoid R X)

ink

def «term_[_]» : Lean.TrailingParserDescr

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.

ink

instance FreeModule.decideEqualQuotient {R : Type} [inst : Ring R] [inst : DecidableEq R] {X : Type} [inst : DecidableEq X] (s₁ : FormalSum R X) (s₂ : FormalSum R X) : Decidable (Quotient.mk (formalSumSetoid R X) s₁ = Quotient.mk (formalSumSetoid R X) 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

ink

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

Boolean equality on support.

Equations

• FreeModule.beqOnSupport l f g = List.all l fun x => decide (f x = g x)

ink

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

Equality on support from boolean equality.

ink

theorem FreeModule.eqlquot_of_beq_support {R : Type} [inst : Ring R] [inst : DecidableEq R] {X : Type} [inst : DecidableEq X] (s₁ : FormalSum R X) (s₂ : FormalSum R X) (c₁ : FreeModule.beqOnSupport (FormalSum.support s₁) (FormalSum.coords s₁) (FormalSum.coords s₂) = true) (c₂ : FreeModule.beqOnSupport (FormalSum.support s₂) (FormalSum.coords s₁) (FormalSum.coords s₂) = true) : Quotient.mk (formalSumSetoid R X) s₁ = Quotient.mk (formalSumSetoid R X) s₂

Boolean equality on support gives equal quotients.

ink

def FreeModule.beq_quot {R : Type} [inst : Ring R] [inst : DecidableEq R] {X : Type} [inst : DecidableEq X] (x₁ : R[X]) (x₂ : R[X]) : Bool

Boolean equality for the quotient via lifting

Equations

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

ink

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

Boolean equality for the quotient is equality.

ink

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

Boolean inequality for the quotient is inequality.

ink

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

Decidable equality for the free module.

Equations

• FreeModule.decEq x₁ x₂ = match p : FreeModule.beq_quot x₁ x₂ with | true => isTrue (_ : x₁ = x₂) | false => isFalse (_ : ¬x₁ = x₂)

Induced coordinates on the quotient.

ink

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

Coordinates are well defined on the quotient.

ink

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

coordinates for the quotient

Equations

• FreeModule.coordinates x₀ = Quotient.lift (fun s => FormalSum.coords s x₀) (_ : ∀ (a b : FormalSum R X), a ≈ b → FormalSum.coords a x₀ = FormalSum.coords b 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.

ink

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

Scalar multiplication on formal sums.

Equations

• FormalSum.scmul x [] = []
• FormalSum.scmul x (h :: t) = match h with | (a₀, x₀) => (x * a₀, x₀) :: FormalSum.scmul x t

ink

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

Coordinates after scalar multiplication.

ink

def FormalSum.FreeModule.scmul {R : Type} [inst : Ring R] {X : Type} [inst : DecidableEq X] : R → R[X] → R[X]

Scalar multiplication on the Free Module.

Equations

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

Addition: on formal sums and on the quotient.

ink

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

Coordinates add when appending.

ink

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

Coordinates well-defined up to equivalence.

ink

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

Addition of elements in the free module.

Equations

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

ink

instance instAddFreeModule {R : Type} [inst : Ring R] {X : Type} [inst : DecidableEq X] : Add (R[X])

Equations

• instAddFreeModule = { add := FreeModule.add }

ink

instance instHSMulFreeModule {R : Type} [inst : Ring R] {X : Type} [inst : DecidableEq X] : HSMul R (R[X]) (R[X])

Equations

• instHSMulFreeModule = { hSMul := FormalSum.FreeModule.scmul }

Properties of operations on formal sums.

ink

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

Associativity for scalar multiplication for formal sums.

ink

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

Distributivity for the module operations.

Module properties for the free module.

ink

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

Associativity for scalar and ring products.

ink

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

Commutativity of addition.

ink

theorem FreeModule.add_assoc_aux {R : Type} [inst : Ring R] {X : Type} [inst : DecidableEq X] (s₁ : FormalSum R X) (x₂ : R[X]) (x₃ : R[X]) : Quotient.mk (formalSumSetoid R X) s₁ + x₂ + x₃ = Quotient.mk (formalSumSetoid R X) s₁ + (x₂ + x₃)

ink

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

Associativity of addition.

ink

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

The zero element of the free module.

Equations

• FreeModule.zero = Quotient.mk (formalSumSetoid R X) []

ink

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

adding zero

ink

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

adding zero

ink

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

Distributivity for addition of module elements.

ink

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

Distributivity with respect to scalars.

ink

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

Multiplication by 1 : R.

ink

theorem FreeModule.zero_coeffs {R : Type} [inst : Ring R] {X : Type} [inst : DecidableEq X] (x : R[X]) : 0 • x = Quotient.mk (formalSumSetoid R X) []

Multiplication by 0 : R.

ink

instance FreeModule.instAddCommGroupFreeModule {R : Type} [inst : Ring R] {X : Type} [inst : DecidableEq X] : AddCommGroup (R[X])

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

Equations

• FreeModule.instAddCommGroupFreeModule = AddCommGroup.mk (_ : ∀ (x₁ x₂ : R[X]), x₁ + x₂ = x₂ + x₁)

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

ink

inductive ElementaryMove (R : Type) (X : Type) [inst : Ring R] [inst : DecidableEq R] [inst : DecidableEq X] : FormalSum R X → FormalSum R X → Prop

• zeroCoeff: ∀ {R X : Type} [inst : Ring R] [inst_1 : DecidableEq R] [inst_2 : DecidableEq X] (tail : FormalSum R X) (x : X) (a : R), a = 0 → ElementaryMove R X ((a, x) :: tail) tail
• addCoeffs: ∀ {R X : Type} [inst : Ring R] [inst_1 : DecidableEq R] [inst_2 : 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} [inst : Ring R] [inst_1 : DecidableEq R] [inst_2 : 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} [inst : Ring R] [inst_1 : DecidableEq R] [inst_2 : 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)

Elementary moves for formal sums.

ink

def FreeModuleAux (R : Type) (X : Type) [inst : Ring R] [inst : DecidableEq R] [inst : DecidableEq X] : Type

Equations

• FreeModuleAux R X = Quot (ElementaryMove R X)

ink

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

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

Equations

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

ink

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

Equivalence by having the same image.

Equations

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

ink

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

Equations

• FormalSum.«term_≃_» = Lean.ParserDescr.trailingNode `FormalSum.term_≃_ 65 66 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃ ") (Lean.ParserDescr.cat `term 66))

Invariance of coordinates under elementary moves

ink

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

Coordinates are invariant under moves.

ink

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

Coordinates on the quotients.

Equations

• FreeModuleAux.coeff x₀ = Quot.lift (fun s => FormalSum.coords s x₀) (_ : ∀ (s₁ s₂ : FormalSum R X), ElementaryMove R X s₁ s₂ → FormalSum.coords s₁ x₀ = FormalSum.coords s₂ x₀)

ink

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

Commutative diagram for coordinates.

ink

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

Coordinates well-defined under the equivalence generated by moves.

Equal coordinates implies related by elementary moves.

ink

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

Cons respects equivalence.

ink

theorem FormalSum.nonzero_coeff_has_complement {R : Type} [inst : Ring R] [inst : DecidableEq R] {X : Type} [inst : DecidableEq X] (x₀ : X) (s : FormalSum R X) : 0 ≠ FormalSum.coords s x₀ → ∃ ys, (FormalSum.coords s 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.

ink

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

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

ink

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

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

Functions invariant under moves pass to the quotient.

ink

theorem FormalSum.func_eql_of_move_equiv {R : Type} [inst : Ring R] [inst : DecidableEq R] {X : Type} [inst : 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.

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

ink

theorem fst_le_max (a : ℕ) (b : ℕ) : a ≤ max a b

ink

theorem snd_le_max (a : ℕ) (b : ℕ) : b ≤ max a b

ink

theorem eq_fst_or_snd_of_max (a : ℕ) (b : ℕ) : max a b = a ∨ max a b = b

ink

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

Equations

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

ink

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

ink

theorem supp_below_max {R : Type u_2} [inst : Ring R] [inst : 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

ink

theorem supp_zero_of_max_zero {R : Type u_2} [inst : Ring R] [inst : 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

ink

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

Equations

• FormalSum.normSucc norm s = maxNormSuccOnSupp norm (FormalSum.coords s) (FormalSum.support s)

ink

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

ink

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

ink

class NormCube (α : Type) : Type

• norm : α → ℕ
• cube : ℕ → List α

ink

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

Equations

• normCube α k = NormCube.cube k

ink

instance natCube : NormCube ℕ

Equations

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

ink

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

Equations

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

ink

instance intCube : NormCube ℤ

Equations

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

ink

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

Equations

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

ink

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

Equations

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

ink

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

Equations

• FreeModule.coeffList x = List.filterMap (fun x₀ => let a := FreeModule.coordinates x₀ x; if a = 0 then none else some (a, x₀)) (NormCube.cube (FreeModule.normBound x))

ink

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

Equations

• basicRepr = { reprPrec := fun x x_1 => Std.Format.text (reprStr (FreeModule.coeffList x)) }