Documentation

Mathlib.Algebra.Module.LocalizedModuleIntegers

Integer elements of a localized module #

This is a mirror of the corresponding notion for localizations of rings.

Main definitions #

Implementation details #

After IsLocalizedModule and IsLocalization are unified, the two IsInteger predicates can be unified.

def IsLocalizedModule.IsInteger {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {M' : Type u_3} [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') (x : M') :

Given x : M', M' a localization of M via f, IsInteger f x iff x is in the image of the localization map f.

Equations
theorem IsLocalizedModule.isInteger_zero {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {M' : Type u_3} [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') :
theorem IsLocalizedModule.isInteger_add {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {M' : Type u_3} [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') {x : M'} {y : M'} (hx : IsLocalizedModule.IsInteger f x) (hy : IsLocalizedModule.IsInteger f y) :
theorem IsLocalizedModule.isInteger_smul {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {M' : Type u_3} [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') {a : R} {x : M'} (hx : IsLocalizedModule.IsInteger f x) :
theorem IsLocalizedModule.exists_integer_multiple {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} [AddCommMonoid M] [Module R M] {M' : Type u_3} [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (x : M') :
∃ (a : S), IsLocalizedModule.IsInteger f (a x)

Each element x : M' has an S-multiple which is an integer.

theorem IsLocalizedModule.exist_integer_multiples {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} [AddCommMonoid M] [Module R M] {M' : Type u_3} [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] {ι : Type u_4} (s : Finset ι) (g : ιM') :
∃ (b : S), is, IsLocalizedModule.IsInteger f (b g i)

We can clear the denominators of a Finset-indexed family of fractions.

theorem IsLocalizedModule.exist_integer_multiples_of_finite {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} [AddCommMonoid M] [Module R M] {M' : Type u_3} [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] {ι : Type u_4} [Finite ι] (g : ιM') :
∃ (b : S), ∀ (i : ι), IsLocalizedModule.IsInteger f (b g i)

We can clear the denominators of a finite indexed family of fractions.

theorem IsLocalizedModule.exist_integer_multiples_of_finset {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} [AddCommMonoid M] [Module R M] {M' : Type u_3} [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (s : Finset M') :
∃ (b : S), as, IsLocalizedModule.IsInteger f (b a)

We can clear the denominators of a finite set of fractions.

noncomputable def IsLocalizedModule.commonDenom {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} [AddCommMonoid M] [Module R M] {M' : Type u_3} [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] {ι : Type u_4} (s : Finset ι) (g : ιM') :
S

A choice of a common multiple of the denominators of a Finset-indexed family of fractions.

Equations
noncomputable def IsLocalizedModule.integerMultiple {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} [AddCommMonoid M] [Module R M] {M' : Type u_3} [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] {ι : Type u_4} (s : Finset ι) (g : ιM') (i : { x : ι // x s }) :
M

The numerator of a fraction after clearing the denominators of a Finset-indexed family of fractions.

Equations
@[simp]
theorem IsLocalizedModule.map_integerMultiple {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} [AddCommMonoid M] [Module R M] {M' : Type u_3} [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] {ι : Type u_4} (s : Finset ι) (g : ιM') (i : { x : ι // x s }) :
noncomputable def IsLocalizedModule.commonDenomOfFinset {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} [AddCommMonoid M] [Module R M] {M' : Type u_3} [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] (s : Finset M') :
S

A choice of a common multiple of the denominators of a finite set of fractions.

Equations
noncomputable def IsLocalizedModule.finsetIntegerMultiple {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} [AddCommMonoid M] [Module R M] {M' : Type u_3} [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] [DecidableEq M] (s : Finset M') :

The finset of numerators after clearing the denominators of a finite set of fractions.

Equations
theorem IsLocalizedModule.smul_mem_finsetIntegerMultiple_span {R : Type u_1} [CommSemiring R] (S : Submonoid R) {M : Type u_2} [AddCommMonoid M] [Module R M] {M' : Type u_3} [AddCommMonoid M'] [Module R M'] (f : M →ₗ[R] M') [IsLocalizedModule S f] [DecidableEq M] (x : M) (s : Finset M') (hx : f x Submodule.span R s) :