Denominator-cleared dependence over an integral domain

These algebraic helpers contain no Carlson functions or analytic assumptions.

def DirichletTransform.denominatorClosure {A : Type u_1} {M : Type u_2} [CommRing A] [IsDomain A] [AddCommGroup M] [Module A M] (P : Submodule A M) : Submodule A M

Clearing a nonzero scalar denominator in a submodule.

Equations

• DirichletTransform.denominatorClosure P = { carrier := {v : M | ∃ (d : A), d ≠ 0 ∧ d • v ∈ P}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

theorem DirichletTransform.mem_denominatorClosure {A : Type u_1} {M : Type u_2} [CommRing A] [IsDomain A] [AddCommGroup M] [Module A M] (P : Submodule A M) {v : M} (hv : v ∈ P) : v ∈ denominatorClosure P

theorem DirichletTransform.denominatorClosure_cancel {A : Type u_1} {M : Type u_2} [CommRing A] [IsDomain A] [AddCommGroup M] [Module A M] (P : Submodule A M) {c : A} {v : M} (hc : c ≠ 0) (hv : c • v ∈ denominatorClosure P) : v ∈ denominatorClosure P

theorem DirichletTransform.exists_relation_of_mem_denominatorClosure {A : Type u_1} {M : Type u_2} {J : Type u_3} {K : Type u_4} [CommRing A] [IsDomain A] [AddCommGroup M] [Module A M] [Fintype J] [Fintype K] (v : K → M) (w : J → M) (hcard : Fintype.card K < Fintype.card J) (hw : ∀ (j : J), w j ∈ denominatorClosure (Submodule.span A (Set.range v))) : ∃ (a : J → A), (∃ (j : J), a j ≠ 0) ∧ ∑ j : J, a j • w j = 0

Clearing denominators reduces dependence in a saturated finite span to dependence of coefficient vectors over the original integral domain.