Submonoid of inverses #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Main definitions #

is_localization.inv_submonoid M S is the submonoid of S = M⁻¹R consisting of inverses of each element x ∈ M

Implementation notes #

See src/ring_theory/localization/basic.lean for a design overview.

Tags #

localization, ring localization, commutative ring localization, characteristic predicate, commutative ring, field of fractions

source

def is_localization.inv_submonoid {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] :

submonoid S

The submonoid of S = M⁻¹R consisting of { 1 / x | x ∈ M }.

Equations

is_localization.inv_submonoid M S = (submonoid.map (algebra_map R S) M).left_inv

source

theorem is_localization.submonoid_map_le_is_unit {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] :

submonoid.map (algebra_map R S) M ≤ is_unit.submonoid S

source

@[reducible]

noncomputable def is_localization.equiv_inv_submonoid {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] :

↥(submonoid.map (algebra_map R S) M) ≃* ↥(is_localization.inv_submonoid M S)

There is an equivalence of monoids between the image of M and inv_submonoid.

source

noncomputable def is_localization.to_inv_submonoid {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] :

↥M →* ↥(is_localization.inv_submonoid M S)

There is a canonical map from M to inv_submonoid sending x to 1 / x.

Equations

is_localization.to_inv_submonoid M S = (is_localization.equiv_inv_submonoid M S).to_monoid_hom.comp (↑(algebra_map R S).submonoid_map M)

source

theorem is_localization.to_inv_submonoid_surjective {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] :

function.surjective ⇑(is_localization.to_inv_submonoid M S)

source

@[simp]

theorem is_localization.to_inv_submonoid_mul {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] (m : ↥M) :

↑(⇑(is_localization.to_inv_submonoid M S) m) * ⇑(algebra_map R S) ↑m = 1

source

@[simp]

theorem is_localization.mul_to_inv_submonoid {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] (m : ↥M) :

⇑(algebra_map R S) ↑m * ↑(⇑(is_localization.to_inv_submonoid M S) m) = 1

source

@[simp]

theorem is_localization.smul_to_inv_submonoid {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] (m : ↥M) :

m • ↑(⇑(is_localization.to_inv_submonoid M S) m) = 1

source

theorem is_localization.surj' {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (z : S) :

∃ (r : R) (m : ↥M), z = r • ↑(⇑(is_localization.to_inv_submonoid M S) m)

source

theorem is_localization.to_inv_submonoid_eq_mk' {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (x : ↥M) :

↑(⇑(is_localization.to_inv_submonoid M S) x) = is_localization.mk' S 1 x

source

theorem is_localization.mem_inv_submonoid_iff_exists_mk' {R : Type u_1} [comm_ring R] (M : submonoid R) {S : Type u_2} [comm_ring S] [algebra R S] [is_localization M S] (x : S) :

x ∈ is_localization.inv_submonoid M S ↔ ∃ (m : ↥M), is_localization.mk' S 1 m = x

source

theorem is_localization.span_inv_submonoid {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] :

submodule.span R ↑(is_localization.inv_submonoid M S) = ⊤

source

theorem is_localization.finite_type_of_monoid_fg {R : Type u_1} [comm_ring R] (M : submonoid R) (S : Type u_2) [comm_ring S] [algebra R S] [is_localization M S] [monoid.fg ↥M] :

algebra.finite_type R S