Integer elements of a localized module

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

Main definitions

• IsLocalizedModule.IsInteger is a predicate stating that m : M' is in the image of M

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') : Prop

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

• IsLocalizedModule.IsInteger f x = (x ∈ LinearMap.range f)

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') : IsInteger f 0

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 y : M'} (hx : IsInteger f x) (hy : IsInteger f y) : IsInteger f (x + 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 : IsInteger f x) : IsInteger f (a • 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), 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), ∀ i ∈ s, 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 : ι), 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), ∀ a ∈ s, 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

• IsLocalizedModule.commonDenom S f s g = ⋯.choose

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

• IsLocalizedModule.integerMultiple S f s g i = Exists.choose ⋯

@[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 }) : f (integerMultiple S f s g i) = commonDenom S f s g • g ↑i

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

• IsLocalizedModule.commonDenomOfFinset S f s = IsLocalizedModule.commonDenom S f s id

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') : Finset M

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

Equations

• IsLocalizedModule.finsetIntegerMultiple S f s = Finset.image (fun (t : { x : M' // x ∈ s }) => IsLocalizedModule.integerMultiple S f s id t) s.attach

theorem IsLocalizedModule.finsetIntegerMultiple_image {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') : ⇑f '' ↑(finsetIntegerMultiple S f s) = commonDenomOfFinset S f s • ↑s

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) : ∃ (m : ↥S), m • x ∈ Submodule.span R ↑(finsetIntegerMultiple S f s)