group_theory.monoid_localization

@[nolint]

structure add_submonoid.localization_map {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) (N : Type u_2) [add_comm_monoid N] :

Type (max u_1 u_2)

to_add_monoid_hom : M →+ N
map_add_units' : ∀ (y : ↥S), is_add_unit (self.to_add_monoid_hom.to_fun ↑y)
surj' : ∀ (z : N), ∃ (x : M × ↥S), z + self.to_add_monoid_hom.to_fun ↑(x.snd) = self.to_add_monoid_hom.to_fun x.fst
eq_iff_exists' : ∀ (x y : M), self.to_add_monoid_hom.to_fun x = self.to_add_monoid_hom.to_fun y ↔ ∃ (c : ↥S), ↑c + x = ↑c + y

The type of add_monoid homomorphisms satisfying the characteristic predicate: if f : M →+ N satisfies this predicate, then N is isomorphic to the localization of M at S.

Instances for add_submonoid.localization_map

add_submonoid.localization_map.has_sizeof_inst

source

@[nolint]

structure submonoid.localization_map {M : Type u_1} [comm_monoid M] (S : submonoid M) (N : Type u_2) [comm_monoid N] :

Type (max u_1 u_2)

to_monoid_hom : M →* N
map_units' : ∀ (y : ↥S), is_unit (self.to_monoid_hom.to_fun ↑y)
surj' : ∀ (z : N), ∃ (x : M × ↥S), z * self.to_monoid_hom.to_fun ↑(x.snd) = self.to_monoid_hom.to_fun x.fst
eq_iff_exists' : ∀ (x y : M), self.to_monoid_hom.to_fun x = self.to_monoid_hom.to_fun y ↔ ∃ (c : ↥S), ↑c * x = ↑c * y

The type of monoid homomorphisms satisfying the characteristic predicate: if f : M →* N satisfies this predicate, then N is isomorphic to the localization of M at S.

Instances for submonoid.localization_map

submonoid.localization_map.has_sizeof_inst

source

def add_localization.r {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) :

add_con (M × ↥S)

The congruence relation on M × S, M an add_comm_monoid and S an add_submonoid of M, whose quotient is the localization of M at S, defined as the unique congruence relation on M × S such that for any other congruence relation s on M × S where for all y ∈ S, (0, 0) ∼ (y, y) under s, we have that (x₁, y₁) ∼ (x₂, y₂) by r implies (x₁, y₁) ∼ (x₂, y₂) by s.

Equations

add_localization.r S = has_Inf.Inf {c : add_con (M × ↥S) | ∀ (y : ↥S), ⇑c 0 (↑y, y)}

source

def localization.r {M : Type u_1} [comm_monoid M] (S : submonoid M) :

con (M × ↥S)

The congruence relation on M × S, M a comm_monoid and S a submonoid of M, whose quotient is the localization of M at S, defined as the unique congruence relation on M × S such that for any other congruence relation s on M × S where for all y ∈ S, (1, 1) ∼ (y, y) under s, we have that (x₁, y₁) ∼ (x₂, y₂) by r implies (x₁, y₁) ∼ (x₂, y₂) by s.

Equations

localization.r S = has_Inf.Inf {c : con (M × ↥S) | ∀ (y : ↥S), ⇑c 1 (↑y, y)}

source

def add_localization.r' {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) :

add_con (M × ↥S)

An alternate form of the congruence relation on M × S, M a comm_monoid and S a submonoid of M, whose quotient is the localization of M at S.

Equations

add_localization.r' S = {to_setoid := {r := λ (a b : M × ↥S), ∃ (c : ↥S), ↑c + (↑(b.snd) + a.fst) = ↑c + (↑(a.snd) + b.fst), iseqv := _}, add' := _}

source

def localization.r' {M : Type u_1} [comm_monoid M] (S : submonoid M) :

con (M × ↥S)

An alternate form of the congruence relation on M × S, M a comm_monoid and S a submonoid of M, whose quotient is the localization of M at S.

Equations

localization.r' S = {to_setoid := {r := λ (a b : M × ↥S), ∃ (c : ↥S), ↑c * (↑(b.snd) * a.fst) = ↑c * (↑(a.snd) * b.fst), iseqv := _}, mul' := _}

source

theorem localization.r_eq_r' {M : Type u_1} [comm_monoid M] (S : submonoid M) :

localization.r S = localization.r' S

The congruence relation used to localize a comm_monoid at a submonoid can be expressed equivalently as an infimum (see localization.r) or explicitly (see localization.r').

source

theorem add_localization.r_eq_r' {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) :

add_localization.r S = add_localization.r' S

The additive congruence relation used to localize an add_comm_monoid at a submonoid can be expressed equivalently as an infimum (see add_localization.r) or explicitly (see add_localization.r').

source

theorem add_localization.r_iff_exists {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {x y : M × ↥S} :

⇑(add_localization.r S) x y ↔ ∃ (c : ↥S), ↑c + (↑(y.snd) + x.fst) = ↑c + (↑(x.snd) + y.fst)

source

theorem localization.r_iff_exists {M : Type u_1} [comm_monoid M] {S : submonoid M} {x y : M × ↥S} :

⇑(localization.r S) x y ↔ ∃ (c : ↥S), ↑c * (↑(y.snd) * x.fst) = ↑c * (↑(x.snd) * y.fst)

source

@[irreducible]

def localization {M : Type u_1} [comm_monoid M] (S : submonoid M) :

Type u_1

The localization of a comm_monoid at one of its submonoids (as a quotient type).

Equations

localization S = (localization.r S).quotient

Instances for localization

source

def add_localization {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) :

Type u_1

The localization of an add_comm_monoid at one of its submonoids (as a quotient type).

Equations

add_localization S = (add_localization.r S).quotient

Instances for add_localization

source

@[protected, instance]

def localization.inhabited {M : Type u_1} [comm_monoid M] (S : submonoid M) :

inhabited (localization S)

Equations

localization.inhabited S = con.quotient.inhabited

source

@[protected, instance]

def add_localization.inhabited {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) :

inhabited (add_localization S)

Equations

add_localization.inhabited S = add_con.quotient.inhabited

source

@[protected, irreducible]

def localization.mul {M : Type u_1} [comm_monoid M] (S : submonoid M) :

localization S → localization S → localization S

Multiplication in a localization is defined as ⟨a, b⟩ * ⟨c, d⟩ = ⟨a * c, b * d⟩.

Equations

localization.mul S = comm_monoid.mul

source

@[protected]

def add_localization.add {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) :

add_localization S → add_localization S → add_localization S

Addition in an add_localization is defined as ⟨a, b⟩ + ⟨c, d⟩ = ⟨a + c, b + d⟩.

Should not be confused with the ring localization counterpart localization.add, which maps ⟨a, b⟩ + ⟨c, d⟩ to ⟨d * a + b * c, b * d⟩.

Equations

add_localization.add S = add_comm_monoid.add

source

@[protected, instance]

def localization.has_mul {M : Type u_1} [comm_monoid M] (S : submonoid M) :

has_mul (localization S)

Equations

localization.has_mul S = {mul := localization.mul S}

source

@[protected, instance]

def add_localization.has_add {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) :

has_add (add_localization S)

Equations

add_localization.has_add S = {add := add_localization.add S}

source

@[protected, irreducible]

def localization.one {M : Type u_1} [comm_monoid M] (S : submonoid M) :

localization S

The identity element of a localization is defined as ⟨1, 1⟩.

Equations

localization.one S = comm_monoid.one

source

@[protected]

def add_localization.zero {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) :

add_localization S

The identity element of an add_localization is defined as ⟨0, 0⟩.

Should not be confused with the ring localization counterpart localization.zero, which is defined as ⟨0, 1⟩.

Equations

add_localization.zero S = add_comm_monoid.zero

source

@[protected, instance]

def add_localization.has_zero {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) :

has_zero (add_localization S)

Equations

add_localization.has_zero S = {zero := add_localization.zero S}

source

@[protected, instance]

def localization.has_one {M : Type u_1} [comm_monoid M] (S : submonoid M) :

has_one (localization S)

Equations

localization.has_one S = {one := localization.one S}

source

@[protected, irreducible]

def localization.npow {M : Type u_1} [comm_monoid M] (S : submonoid M) :

ℕ → localization S → localization S

Exponentiation in a localization is defined as ⟨a, b⟩ ^ n = ⟨a ^ n, b ^ n⟩.

This is a separate irreducible def to ensure the elaborator doesn't waste its time trying to unify some huge recursive definition with itself, but unfolded one step less.

Equations

localization.npow S = comm_monoid.npow

source

@[protected]

def add_localization.nsmul {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) :

ℕ → add_localization S → add_localization S

Multiplication with a natural in an add_localization is defined as n • ⟨a, b⟩ = ⟨n • a, n • b⟩.

This is a separate irreducible def to ensure the elaborator doesn't waste its time trying to unify some huge recursive definition with itself, but unfolded one step less.

Equations

add_localization.nsmul S = add_comm_monoid.nsmul

source

@[protected, instance]

def add_localization.add_comm_monoid {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) :

add_comm_monoid (add_localization S)

Equations

add_localization.add_comm_monoid S = {add := has_add.add (add_localization.has_add S), add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_localization.nsmul S, nsmul_zero' := _, nsmul_succ' := _, add_comm := _}

source

@[protected, instance]

def localization.comm_monoid {M : Type u_1} [comm_monoid M] (S : submonoid M) :

comm_monoid (localization S)

Equations

localization.comm_monoid S = {mul := has_mul.mul (localization.has_mul S), mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := localization.npow S, npow_zero' := _, npow_succ' := _, mul_comm := _}

source

def localization.mk {M : Type u_1} [comm_monoid M] {S : submonoid M} (x : M) (y : ↥S) :

localization S

Given a comm_monoid M and submonoid S, mk sends x : M, y ∈ S to the equivalence class of (x, y) in the localization of M at S.

Equations

localization.mk x y = ⇑((localization.r S).mk') (x, y)

source

def add_localization.mk {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} (x : M) (y : ↥S) :

add_localization S

Given an add_comm_monoid M and submonoid S, mk sends x : M, y ∈ S to the equivalence class of (x, y) in the localization of M at S.

Equations

add_localization.mk x y = ⇑((add_localization.r S).mk') (x, y)

source

theorem add_localization.mk_eq_mk_iff {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {a c : M} {b d : ↥S} :

add_localization.mk a b = add_localization.mk c d ↔ ⇑(add_localization.r S) (a, b) (c, d)

source

theorem localization.mk_eq_mk_iff {M : Type u_1} [comm_monoid M] {S : submonoid M} {a c : M} {b d : ↥S} :

localization.mk a b = localization.mk c d ↔ ⇑(localization.r S) (a, b) (c, d)

source

def localization.rec {M : Type u_1} [comm_monoid M] {S : submonoid M} {p : localization S → Sort u} (f : Π (a : M) (b : ↥S), p (localization.mk a b)) (H : ∀ {a c : M} {b d : ↥S} (h : ⇑(localization.r S) (a, b) (c, d)), eq.rec (f a b) _ = f c d) (x : localization S) :

p x

Dependent recursion principle for localizations: given elements f a b : p (mk a b) for all a b, such that r S (a, b) (c, d) implies f a b = f c d (with the correct coercions), then f is defined on the whole localization S.

Equations

localization.rec f H x = quot.rec (λ (y : M × ↥S), eq.rec (f y.fst y.snd) _) _ x

source

def add_localization.rec {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {p : add_localization S → Sort u} (f : Π (a : M) (b : ↥S), p (add_localization.mk a b)) (H : ∀ {a c : M} {b d : ↥S} (h : ⇑(add_localization.r S) (a, b) (c, d)), eq.rec (f a b) _ = f c d) (x : add_localization S) :

p x

Dependent recursion principle for add_localizations: given elements f a b : p (mk a b) for all a b, such that r S (a, b) (c, d) implies f a b = f c d (with the correct coercions), then f is defined on the whole add_localization S.

Equations

add_localization.rec f H x = quot.rec (λ (y : M × ↥S), eq.rec (f y.fst y.snd) _) _ x

source

def localization.rec_on_subsingleton₂ {M : Type u_1} [comm_monoid M] {S : submonoid M} {r : localization S → localization S → Sort u} [h : ∀ (a c : M) (b d : ↥S), subsingleton (r (localization.mk a b) (localization.mk c d))] (x y : localization S) (f : Π (a c : M) (b d : ↥S), r (localization.mk a b) (localization.mk c d)) :

r x y

Copy of quotient.rec_on_subsingleton₂ for localization

Equations

x.rec_on_subsingleton₂ y f = quotient.rec_on_subsingleton₂' x y (prod.rec (λ (_x : M) (_x_1 : ↥S), prod.rec (λ (_x_2 : M) (_x_3 : ↥S), f _x _x_2 _x_1 _x_3)))

source

def add_localization.rec_on_subsingleton₂ {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {r : add_localization S → add_localization S → Sort u} [h : ∀ (a c : M) (b d : ↥S), subsingleton (r (add_localization.mk a b) (add_localization.mk c d))] (x y : add_localization S) (f : Π (a c : M) (b d : ↥S), r (add_localization.mk a b) (add_localization.mk c d)) :

r x y

Copy of quotient.rec_on_subsingleton₂ for add_localization

Equations

x.rec_on_subsingleton₂ y f = quotient.rec_on_subsingleton₂' x y (prod.rec (λ (_x : M) (_x_1 : ↥S), prod.rec (λ (_x_2 : M) (_x_3 : ↥S), f _x _x_2 _x_1 _x_3)))

source

theorem add_localization.mk_add {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} (a c : M) (b d : ↥S) :

add_localization.mk a b + add_localization.mk c d = add_localization.mk (a + c) (b + d)

source

theorem localization.mk_mul {M : Type u_1} [comm_monoid M] {S : submonoid M} (a c : M) (b d : ↥S) :

localization.mk a b * localization.mk c d = localization.mk (a * c) (b * d)

source

theorem localization.mk_one {M : Type u_1} [comm_monoid M] {S : submonoid M} :

localization.mk 1 1 = 1

source

theorem add_localization.mk_zero {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} :

add_localization.mk 0 0 = 0

source

theorem localization.mk_pow {M : Type u_1} [comm_monoid M] {S : submonoid M} (n : ℕ) (a : M) (b : ↥S) :

localization.mk a b ^ n = localization.mk (a ^ n) (b ^ n)

source

theorem add_localization.mk_nsmul {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} (n : ℕ) (a : M) (b : ↥S) :

n • add_localization.mk a b = add_localization.mk (n • a) (n • b)

source

@[simp]

theorem add_localization.rec_mk {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {p : add_localization S → Sort u} (f : Π (a : M) (b : ↥S), p (add_localization.mk a b)) (H : ∀ {a c : M} {b d : ↥S} (h : ⇑(add_localization.r S) (a, b) (c, d)), eq.rec (f a b) _ = f c d) (a : M) (b : ↥S) :

add_localization.rec f H (add_localization.mk a b) = f a b

source

@[simp]

theorem localization.rec_mk {M : Type u_1} [comm_monoid M] {S : submonoid M} {p : localization S → Sort u} (f : Π (a : M) (b : ↥S), p (localization.mk a b)) (H : ∀ {a c : M} {b d : ↥S} (h : ⇑(localization.r S) (a, b) (c, d)), eq.rec (f a b) _ = f c d) (a : M) (b : ↥S) :

localization.rec f H (localization.mk a b) = f a b

source

def add_localization.lift_on {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {p : Sort u} (x : add_localization S) (f : M → ↥S → p) (H : ∀ {a c : M} {b d : ↥S}, ⇑(add_localization.r S) (a, b) (c, d) → f a b = f c d) :

p

Non-dependent recursion principle for add_localizations: given elements f a b : p for all a b, such that r S (a, b) (c, d) implies f a b = f c d, then f is defined on the whole localization S.

Equations

x.lift_on f H = add_localization.rec f _ x

source

def localization.lift_on {M : Type u_1} [comm_monoid M] {S : submonoid M} {p : Sort u} (x : localization S) (f : M → ↥S → p) (H : ∀ {a c : M} {b d : ↥S}, ⇑(localization.r S) (a, b) (c, d) → f a b = f c d) :

p

Non-dependent recursion principle for localizations: given elements f a b : p for all a b, such that r S (a, b) (c, d) implies f a b = f c d, then f is defined on the whole localization S.

Equations

x.lift_on f H = localization.rec f _ x

source

theorem localization.lift_on_mk {M : Type u_1} [comm_monoid M] {S : submonoid M} {p : Sort u} (f : M → ↥S → p) (H : ∀ {a c : M} {b d : ↥S}, ⇑(localization.r S) (a, b) (c, d) → f a b = f c d) (a : M) (b : ↥S) :

(localization.mk a b).lift_on f H = f a b

source

theorem add_localization.lift_on_mk {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {p : Sort u} (f : M → ↥S → p) (H : ∀ {a c : M} {b d : ↥S}, ⇑(add_localization.r S) (a, b) (c, d) → f a b = f c d) (a : M) (b : ↥S) :

(add_localization.mk a b).lift_on f H = f a b

source

theorem add_localization.ind {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {p : add_localization S → Prop} (H : ∀ (y : M × ↥S), p (add_localization.mk y.fst y.snd)) (x : add_localization S) :

p x

source

theorem localization.ind {M : Type u_1} [comm_monoid M] {S : submonoid M} {p : localization S → Prop} (H : ∀ (y : M × ↥S), p (localization.mk y.fst y.snd)) (x : localization S) :

p x

source

theorem localization.induction_on {M : Type u_1} [comm_monoid M] {S : submonoid M} {p : localization S → Prop} (x : localization S) (H : ∀ (y : M × ↥S), p (localization.mk y.fst y.snd)) :

p x

source

theorem add_localization.induction_on {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {p : add_localization S → Prop} (x : add_localization S) (H : ∀ (y : M × ↥S), p (add_localization.mk y.fst y.snd)) :

p x

source

def add_localization.lift_on₂ {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {p : Sort u} (x y : add_localization S) (f : M → ↥S → M → ↥S → p) (H : ∀ {a a' : M} {b b' : ↥S} {c c' : M} {d d' : ↥S}, ⇑(add_localization.r S) (a, b) (a', b') → ⇑(add_localization.r S) (c, d) (c', d') → f a b c d = f a' b' c' d') :

p

Non-dependent recursion principle for localizations: given elements f x y : p for all x and y, such that r S x x' and r S y y' implies f x y = f x' y', then f is defined on the whole localization S.

Equations

x.lift_on₂ y f H = x.lift_on (λ (a : M) (b : ↥S), y.lift_on (f a b) _) _

source

def localization.lift_on₂ {M : Type u_1} [comm_monoid M] {S : submonoid M} {p : Sort u} (x y : localization S) (f : M → ↥S → M → ↥S → p) (H : ∀ {a a' : M} {b b' : ↥S} {c c' : M} {d d' : ↥S}, ⇑(localization.r S) (a, b) (a', b') → ⇑(localization.r S) (c, d) (c', d') → f a b c d = f a' b' c' d') :

p

Non-dependent recursion principle for localizations: given elements f x y : p for all x and y, such that r S x x' and r S y y' implies f x y = f x' y', then f is defined on the whole localization S.

Equations

x.lift_on₂ y f H = x.lift_on (λ (a : M) (b : ↥S), y.lift_on (f a b) _) _

source

theorem localization.lift_on₂_mk {M : Type u_1} [comm_monoid M] {S : submonoid M} {p : Sort u_2} (f : M → ↥S → M → ↥S → p) (H : ∀ {a a' : M} {b b' : ↥S} {c c' : M} {d d' : ↥S}, ⇑(localization.r S) (a, b) (a', b') → ⇑(localization.r S) (c, d) (c', d') → f a b c d = f a' b' c' d') (a c : M) (b d : ↥S) :

(localization.mk a b).lift_on₂ (localization.mk c d) f H = f a b c d

source

theorem add_localization.lift_on₂_mk {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {p : Sort u_2} (f : M → ↥S → M → ↥S → p) (H : ∀ {a a' : M} {b b' : ↥S} {c c' : M} {d d' : ↥S}, ⇑(add_localization.r S) (a, b) (a', b') → ⇑(add_localization.r S) (c, d) (c', d') → f a b c d = f a' b' c' d') (a c : M) (b d : ↥S) :

(add_localization.mk a b).lift_on₂ (add_localization.mk c d) f H = f a b c d

source

theorem localization.induction_on₂ {M : Type u_1} [comm_monoid M] {S : submonoid M} {p : localization S → localization S → Prop} (x y : localization S) (H : ∀ (x y : M × ↥S), p (localization.mk x.fst x.snd) (localization.mk y.fst y.snd)) :

p x y

source

theorem add_localization.induction_on₂ {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {p : add_localization S → add_localization S → Prop} (x y : add_localization S) (H : ∀ (x y : M × ↥S), p (add_localization.mk x.fst x.snd) (add_localization.mk y.fst y.snd)) :

p x y

source

theorem add_localization.induction_on₃ {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {p : add_localization S → add_localization S → add_localization S → Prop} (x y z : add_localization S) (H : ∀ (x y z : M × ↥S), p (add_localization.mk x.fst x.snd) (add_localization.mk y.fst y.snd) (add_localization.mk z.fst z.snd)) :

p x y z

source

theorem localization.induction_on₃ {M : Type u_1} [comm_monoid M] {S : submonoid M} {p : localization S → localization S → localization S → Prop} (x y z : localization S) (H : ∀ (x y z : M × ↥S), p (localization.mk x.fst x.snd) (localization.mk y.fst y.snd) (localization.mk z.fst z.snd)) :

p x y z

source

theorem localization.one_rel {M : Type u_1} [comm_monoid M] {S : submonoid M} (y : ↥S) :

⇑(localization.r S) 1 (↑y, y)

source

theorem add_localization.zero_rel {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} (y : ↥S) :

⇑(add_localization.r S) 0 (↑y, y)

source

theorem localization.r_of_eq {M : Type u_1} [comm_monoid M] {S : submonoid M} {x y : M × ↥S} (h : ↑(y.snd) * x.fst = ↑(x.snd) * y.fst) :

⇑(localization.r S) x y

source

theorem add_localization.r_of_eq {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {x y : M × ↥S} (h : ↑(y.snd) + x.fst = ↑(x.snd) + y.fst) :

⇑(add_localization.r S) x y

source

theorem add_localization.mk_self {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} (a : ↥S) :

add_localization.mk ↑a a = 0

source

theorem localization.mk_self {M : Type u_1} [comm_monoid M] {S : submonoid M} (a : ↥S) :

localization.mk ↑a a = 1

source

@[protected, irreducible]

def localization.smul {M : Type u_1} [comm_monoid M] {S : submonoid M} {R : Type u_4} [has_smul R M] [is_scalar_tower R M M] (c : R) (z : localization S) :

localization S

Scalar multiplication in a monoid localization is defined as c • ⟨a, b⟩ = ⟨c • a, b⟩.

Equations

localization.smul c z = z.lift_on (λ (a : M) (b : ↥S), localization.mk (c • a) b) _

source

@[protected, instance]

def localization.has_smul {M : Type u_1} [comm_monoid M] {S : submonoid M} {R : Type u_4} [has_smul R M] [is_scalar_tower R M M] :

has_smul R (localization S)

Equations

localization.has_smul = {smul := localization.smul _inst_5}

source

theorem localization.smul_mk {M : Type u_1} [comm_monoid M] {S : submonoid M} {R : Type u_4} [has_smul R M] [is_scalar_tower R M M] (c : R) (a : M) (b : ↥S) :

c • localization.mk a b = localization.mk (c • a) b

source

@[protected, instance]

def localization.smul_comm_class {M : Type u_1} [comm_monoid M] {S : submonoid M} {R₁ : Type u_5} {R₂ : Type u_6} [has_smul R₁ M] [has_smul R₂ M] [is_scalar_tower R₁ M M] [is_scalar_tower R₂ M M] [smul_comm_class R₁ R₂ M] :

smul_comm_class R₁ R₂ (localization S)

source

@[protected, instance]

def localization.is_scalar_tower {M : Type u_1} [comm_monoid M] {S : submonoid M} {R₁ : Type u_5} {R₂ : Type u_6} [has_smul R₁ M] [has_smul R₂ M] [is_scalar_tower R₁ M M] [is_scalar_tower R₂ M M] [has_smul R₁ R₂] [is_scalar_tower R₁ R₂ M] :

is_scalar_tower R₁ R₂ (localization S)

source

@[protected, instance]

def localization.smul_comm_class_right {M : Type u_1} [comm_monoid M] {S : submonoid M} {R : Type u_2} [has_smul R M] [is_scalar_tower R M M] :

smul_comm_class R (localization S) (localization S)

source

@[protected, instance]

def localization.is_scalar_tower_right {M : Type u_1} [comm_monoid M] {S : submonoid M} {R : Type u_2} [has_smul R M] [is_scalar_tower R M M] :

is_scalar_tower R (localization S) (localization S)

source

@[protected, instance]

def localization.is_central_scalar {M : Type u_1} [comm_monoid M] {S : submonoid M} {R : Type u_4} [has_smul R M] [has_smul Rᵐᵒᵖ M] [is_scalar_tower R M M] [is_scalar_tower Rᵐᵒᵖ M M] [is_central_scalar R M] :

is_central_scalar R (localization S)

source

@[protected, instance]

def localization.mul_action {M : Type u_1} [comm_monoid M] {S : submonoid M} {R : Type u_4} [monoid R] [mul_action R M] [is_scalar_tower R M M] :

mul_action R (localization S)

Equations

localization.mul_action = {to_has_smul := localization.has_smul _inst_6, one_smul := _, mul_smul := _}

source

@[protected, instance]

def localization.mul_distrib_mul_action {M : Type u_1} [comm_monoid M] {S : submonoid M} {R : Type u_4} [monoid R] [mul_distrib_mul_action R M] [is_scalar_tower R M M] :

mul_distrib_mul_action R (localization S)

Equations

localization.mul_distrib_mul_action = {to_mul_action := localization.mul_action _inst_6, smul_mul := _, smul_one := _}

source

def add_monoid_hom.to_localization_map {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : M →+ N) (H1 : ∀ (y : ↥S), is_add_unit (⇑f ↑y)) (H2 : ∀ (z : N), ∃ (x : M × ↥S), z + ⇑f ↑(x.snd) = ⇑f x.fst) (H3 : ∀ (x y : M), ⇑f x = ⇑f y ↔ ∃ (c : ↥S), ↑c + x = ↑c + y) :

S.localization_map N

Makes a localization map from an add_comm_monoid hom satisfying the characteristic predicate.

Equations

f.to_localization_map H1 H2 H3 = {to_add_monoid_hom := {to_fun := f.to_fun, map_zero' := _, map_add' := _}, map_add_units' := H1, surj' := H2, eq_iff_exists' := H3}

source

def monoid_hom.to_localization_map {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : M →* N) (H1 : ∀ (y : ↥S), is_unit (⇑f ↑y)) (H2 : ∀ (z : N), ∃ (x : M × ↥S), z * ⇑f ↑(x.snd) = ⇑f x.fst) (H3 : ∀ (x y : M), ⇑f x = ⇑f y ↔ ∃ (c : ↥S), ↑c * x = ↑c * y) :

S.localization_map N

Makes a localization map from a comm_monoid hom satisfying the characteristic predicate.

Equations

f.to_localization_map H1 H2 H3 = {to_monoid_hom := {to_fun := f.to_fun, map_one' := _, map_mul' := _}, map_units' := H1, surj' := H2, eq_iff_exists' := H3}

source

@[reducible]

def add_submonoid.localization_map.to_map {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) :

M →+ N

Short for to_add_monoid_hom; used to apply a localization map as a function.

source

@[reducible]

def submonoid.localization_map.to_map {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) :

M →* N

Short for to_monoid_hom; used to apply a localization map as a function.

source

@[ext]

theorem add_submonoid.localization_map.ext {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {f g : S.localization_map N} (h : ∀ (x : M), ⇑(f.to_map) x = ⇑(g.to_map) x) :

f = g

source

@[ext]

theorem submonoid.localization_map.ext {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {f g : S.localization_map N} (h : ∀ (x : M), ⇑(f.to_map) x = ⇑(g.to_map) x) :

f = g

source

theorem submonoid.localization_map.ext_iff {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {f g : S.localization_map N} :

f = g ↔ ∀ (x : M), ⇑(f.to_map) x = ⇑(g.to_map) x

source

theorem add_submonoid.localization_map.ext_iff {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {f g : S.localization_map N} :

f = g ↔ ∀ (x : M), ⇑(f.to_map) x = ⇑(g.to_map) x

source

theorem add_submonoid.localization_map.to_map_injective {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] :

function.injective add_submonoid.localization_map.to_map

source

theorem submonoid.localization_map.to_map_injective {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] :

function.injective submonoid.localization_map.to_map

source

theorem submonoid.localization_map.map_units {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (y : ↥S) :

is_unit (⇑(f.to_map) ↑y)

source

theorem add_submonoid.localization_map.map_add_units {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) (y : ↥S) :

is_add_unit (⇑(f.to_map) ↑y)

source

theorem submonoid.localization_map.surj {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (z : N) :

∃ (x : M × ↥S), z * ⇑(f.to_map) ↑(x.snd) = ⇑(f.to_map) x.fst

source

theorem add_submonoid.localization_map.surj {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) (z : N) :

∃ (x : M × ↥S), z + ⇑(f.to_map) ↑(x.snd) = ⇑(f.to_map) x.fst

source

theorem submonoid.localization_map.eq_iff_exists {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) {x y : M} :

⇑(f.to_map) x = ⇑(f.to_map) y ↔ ∃ (c : ↥S), ↑c * x = ↑c * y

source

theorem add_submonoid.localization_map.eq_iff_exists {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) {x y : M} :

⇑(f.to_map) x = ⇑(f.to_map) y ↔ ∃ (c : ↥S), ↑c + x = ↑c + y

source

noncomputable def submonoid.localization_map.sec {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (z : N) :

M × ↥S

Given a localization map f : M →* N, a section function sending z : N to some (x, y) : M × S such that f x * (f y)⁻¹ = z.

Equations

f.sec z = classical.some _

source

noncomputable def add_submonoid.localization_map.sec {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) (z : N) :

M × ↥S

Given a localization map f : M →+ N, a section function sending z : N to some (x, y) : M × S such that f x - f y = z.

Equations

f.sec z = classical.some _

source

theorem submonoid.localization_map.sec_spec {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {f : S.localization_map N} (z : N) :

z * ⇑(f.to_map) ↑((f.sec z).snd) = ⇑(f.to_map) (f.sec z).fst

source

theorem add_submonoid.localization_map.sec_spec {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {f : S.localization_map N} (z : N) :

z + ⇑(f.to_map) ↑((f.sec z).snd) = ⇑(f.to_map) (f.sec z).fst

source

theorem submonoid.localization_map.sec_spec' {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {f : S.localization_map N} (z : N) :

⇑(f.to_map) (f.sec z).fst = ⇑(f.to_map) ↑((f.sec z).snd) * z

source

theorem add_submonoid.localization_map.sec_spec' {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {f : S.localization_map N} (z : N) :

⇑(f.to_map) (f.sec z).fst = ⇑(f.to_map) ↑((f.sec z).snd) + z

source

theorem add_submonoid.localization_map.add_neg_left {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {f : M →+ N} (h : ∀ (y : ↥S), is_add_unit (⇑f ↑y)) (y : ↥S) (w z : N) :

w + ↑-⇑(is_add_unit.lift_right (f.restrict S) h) y = z ↔ w = ⇑f ↑y + z

Given an add_monoid hom f : M →+ N and submonoid S ⊆ M such that f(S) ⊆ add_units N, for all w : M, z : N and y ∈ S, we have w - f y = z ↔ w = f y + z.

source

theorem submonoid.localization_map.mul_inv_left {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {f : M →* N} (h : ∀ (y : ↥S), is_unit (⇑f ↑y)) (y : ↥S) (w z : N) :

w * ↑(⇑(is_unit.lift_right (f.restrict S) h) y)⁻¹ = z ↔ w = ⇑f ↑y * z

Given a monoid hom f : M →* N and submonoid S ⊆ M such that f(S) ⊆ Nˣ, for all w : M, z : N and y ∈ S, we have w * (f y)⁻¹ = z ↔ w = f y * z.

source

theorem submonoid.localization_map.mul_inv_right {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {f : M →* N} (h : ∀ (y : ↥S), is_unit (⇑f ↑y)) (y : ↥S) (w z : N) :

z = w * ↑(⇑(is_unit.lift_right (f.restrict S) h) y)⁻¹ ↔ z * ⇑f ↑y = w

Given a monoid hom f : M →* N and submonoid S ⊆ M such that f(S) ⊆ Nˣ, for all w : M, z : N and y ∈ S, we have z = w * (f y)⁻¹ ↔ z * f y = w.

source

theorem add_submonoid.localization_map.add_neg_right {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {f : M →+ N} (h : ∀ (y : ↥S), is_add_unit (⇑f ↑y)) (y : ↥S) (w z : N) :

z = w + ↑-⇑(is_add_unit.lift_right (f.restrict S) h) y ↔ z + ⇑f ↑y = w

Given an add_monoid hom f : M →+ N and submonoid S ⊆ M such that f(S) ⊆ add_units N, for all w : M, z : N and y ∈ S, we have z = w - f y ↔ z + f y = w.

source

@[simp]

theorem add_submonoid.localization_map.add_neg {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {f : M →+ N} (h : ∀ (y : ↥S), is_add_unit (⇑f ↑y)) {x₁ x₂ : M} {y₁ y₂ : ↥S} :

⇑f x₁ + ↑-⇑(is_add_unit.lift_right (f.restrict S) h) y₁ = ⇑f x₂ + ↑-⇑(is_add_unit.lift_right (f.restrict S) h) y₂ ↔ ⇑f (x₁ + ↑y₂) = ⇑f (x₂ + ↑y₁)

Given an add_monoid hom f : M →+ N and submonoid S ⊆ M such that f(S) ⊆ add_units N, for all x₁ x₂ : M and y₁, y₂ ∈ S, we have f x₁ - f y₁ = f x₂ - f y₂ ↔ f (x₁ + y₂) = f (x₂ + y₁).

source

@[simp]

theorem submonoid.localization_map.mul_inv {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {f : M →* N} (h : ∀ (y : ↥S), is_unit (⇑f ↑y)) {x₁ x₂ : M} {y₁ y₂ : ↥S} :

⇑f x₁ * ↑(⇑(is_unit.lift_right (f.restrict S) h) y₁)⁻¹ = ⇑f x₂ * ↑(⇑(is_unit.lift_right (f.restrict S) h) y₂)⁻¹ ↔ ⇑f (x₁ * ↑y₂) = ⇑f (x₂ * ↑y₁)

Given a monoid hom f : M →* N and submonoid S ⊆ M such that f(S) ⊆ Nˣ, for all x₁ x₂ : M and y₁, y₂ ∈ S, we have f x₁ * (f y₁)⁻¹ = f x₂ * (f y₂)⁻¹ ↔ f (x₁ * y₂) = f (x₂ * y₁).

source

theorem add_submonoid.localization_map.neg_inj {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {f : M →+ N} (hf : ∀ (y : ↥S), is_add_unit (⇑f ↑y)) {y z : ↥S} (h : -⇑(is_add_unit.lift_right (f.restrict S) hf) y = -⇑(is_add_unit.lift_right (f.restrict S) hf) z) :

⇑f ↑y = ⇑f ↑z

Given an add_monoid hom f : M →+ N and submonoid S ⊆ M such that f(S) ⊆ add_units N, for all y, z ∈ S, we have - (f y) = - (f z) → f y = f z.

source

theorem submonoid.localization_map.inv_inj {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {f : M →* N} (hf : ∀ (y : ↥S), is_unit (⇑f ↑y)) {y z : ↥S} (h : (⇑(is_unit.lift_right (f.restrict S) hf) y)⁻¹ = (⇑(is_unit.lift_right (f.restrict S) hf) z)⁻¹) :

⇑f ↑y = ⇑f ↑z

Given a monoid hom f : M →* N and submonoid S ⊆ M such that f(S) ⊆ Nˣ, for all y, z ∈ S, we have (f y)⁻¹ = (f z)⁻¹ → f y = f z.

source

theorem add_submonoid.localization_map.neg_unique {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {f : M →+ N} (h : ∀ (y : ↥S), is_add_unit (⇑f ↑y)) {y : ↥S} {z : N} (H : ⇑f ↑y + z = 0) :

↑-⇑(is_add_unit.lift_right (f.restrict S) h) y = z

Given an add_monoid hom f : M →+ N and submonoid S ⊆ M such that f(S) ⊆ add_units N, for all y ∈ S, - (f y) is unique.

source

theorem submonoid.localization_map.inv_unique {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {f : M →* N} (h : ∀ (y : ↥S), is_unit (⇑f ↑y)) {y : ↥S} {z : N} (H : ⇑f ↑y * z = 1) :

↑(⇑(is_unit.lift_right (f.restrict S) h) y)⁻¹ = z

Given a monoid hom f : M →* N and submonoid S ⊆ M such that f(S) ⊆ Nˣ, for all y ∈ S, (f y)⁻¹ is unique.

source

theorem submonoid.localization_map.map_right_cancel {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) {x y : M} {c : ↥S} (h : ⇑(f.to_map) (↑c * x) = ⇑(f.to_map) (↑c * y)) :

⇑(f.to_map) x = ⇑(f.to_map) y

source

theorem add_submonoid.localization_map.map_right_cancel {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) {x y : M} {c : ↥S} (h : ⇑(f.to_map) (↑c + x) = ⇑(f.to_map) (↑c + y)) :

⇑(f.to_map) x = ⇑(f.to_map) y

source

theorem submonoid.localization_map.map_left_cancel {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) {x y : M} {c : ↥S} (h : ⇑(f.to_map) (x * ↑c) = ⇑(f.to_map) (y * ↑c)) :

⇑(f.to_map) x = ⇑(f.to_map) y

source

theorem add_submonoid.localization_map.map_left_cancel {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) {x y : M} {c : ↥S} (h : ⇑(f.to_map) (x + ↑c) = ⇑(f.to_map) (y + ↑c)) :

⇑(f.to_map) x = ⇑(f.to_map) y

source

noncomputable def add_submonoid.localization_map.mk' {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) (x : M) (y : ↥S) :

N

Given a localization map f : M →+ N, the surjection sending (x, y) : M × S to f x - f y.

Equations

f.mk' x y = ⇑(f.to_map) x + ↑-⇑(is_add_unit.lift_right (f.to_map.restrict S) _) y

source

noncomputable def submonoid.localization_map.mk' {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (x : M) (y : ↥S) :

N

Given a localization map f : M →* N, the surjection sending (x, y) : M × S to f x * (f y)⁻¹.

Equations

f.mk' x y = ⇑(f.to_map) x * ↑(⇑(is_unit.lift_right (f.to_map.restrict S) _) y)⁻¹

source

theorem submonoid.localization_map.mk'_mul {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (x₁ x₂ : M) (y₁ y₂ : ↥S) :

f.mk' (x₁ * x₂) (y₁ * y₂) = f.mk' x₁ y₁ * f.mk' x₂ y₂

source

theorem add_submonoid.localization_map.mk'_add {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) (x₁ x₂ : M) (y₁ y₂ : ↥S) :

f.mk' (x₁ + x₂) (y₁ + y₂) = f.mk' x₁ y₁ + f.mk' x₂ y₂

source

theorem add_submonoid.localization_map.mk'_zero {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) (x : M) :

f.mk' x 0 = ⇑(f.to_map) x

source

theorem submonoid.localization_map.mk'_one {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (x : M) :

f.mk' x 1 = ⇑(f.to_map) x

source

@[simp]

theorem add_submonoid.localization_map.mk'_sec {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) (z : N) :

f.mk' (f.sec z).fst (f.sec z).snd = z

Given a localization map f : M →+ N for a submonoid S ⊆ M, for all z : N we have that if x : M, y ∈ S are such that z + f y = f x, then f x - f y = z.

source

@[simp]

theorem submonoid.localization_map.mk'_sec {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (z : N) :

f.mk' (f.sec z).fst (f.sec z).snd = z

Given a localization map f : M →* N for a submonoid S ⊆ M, for all z : N we have that if x : M, y ∈ S are such that z * f y = f x, then f x * (f y)⁻¹ = z.

source

theorem submonoid.localization_map.mk'_surjective {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (z : N) :

∃ (x : M) (y : ↥S), f.mk' x y = z

source

theorem add_submonoid.localization_map.mk'_surjective {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) (z : N) :

∃ (x : M) (y : ↥S), f.mk' x y = z

source

theorem add_submonoid.localization_map.mk'_spec {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) (x : M) (y : ↥S) :

f.mk' x y + ⇑(f.to_map) ↑y = ⇑(f.to_map) x

source

theorem submonoid.localization_map.mk'_spec {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (x : M) (y : ↥S) :

f.mk' x y * ⇑(f.to_map) ↑y = ⇑(f.to_map) x

source

theorem submonoid.localization_map.mk'_spec' {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (x : M) (y : ↥S) :

⇑(f.to_map) ↑y * f.mk' x y = ⇑(f.to_map) x

source

theorem add_submonoid.localization_map.mk'_spec' {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) (x : M) (y : ↥S) :

⇑(f.to_map) ↑y + f.mk' x y = ⇑(f.to_map) x

source

theorem add_submonoid.localization_map.eq_mk'_iff_add_eq {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) {x : M} {y : ↥S} {z : N} :

z = f.mk' x y ↔ z + ⇑(f.to_map) ↑y = ⇑(f.to_map) x

source

theorem submonoid.localization_map.eq_mk'_iff_mul_eq {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) {x : M} {y : ↥S} {z : N} :

z = f.mk' x y ↔ z * ⇑(f.to_map) ↑y = ⇑(f.to_map) x

source

theorem add_submonoid.localization_map.mk'_eq_iff_eq_add {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) {x : M} {y : ↥S} {z : N} :

f.mk' x y = z ↔ ⇑(f.to_map) x = z + ⇑(f.to_map) ↑y

source

theorem submonoid.localization_map.mk'_eq_iff_eq_mul {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) {x : M} {y : ↥S} {z : N} :

f.mk' x y = z ↔ ⇑(f.to_map) x = z * ⇑(f.to_map) ↑y

source

theorem submonoid.localization_map.mk'_eq_iff_eq {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) {x₁ x₂ : M} {y₁ y₂ : ↥S} :

f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ ⇑(f.to_map) (↑y₂ * x₁) = ⇑(f.to_map) (↑y₁ * x₂)

source

theorem add_submonoid.localization_map.mk'_eq_iff_eq {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) {x₁ x₂ : M} {y₁ y₂ : ↥S} :

f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ ⇑(f.to_map) (↑y₂ + x₁) = ⇑(f.to_map) (↑y₁ + x₂)

source

theorem submonoid.localization_map.mk'_eq_iff_eq' {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) {x₁ x₂ : M} {y₁ y₂ : ↥S} :

f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ ⇑(f.to_map) (x₁ * ↑y₂) = ⇑(f.to_map) (x₂ * ↑y₁)

source

theorem add_submonoid.localization_map.mk'_eq_iff_eq' {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) {x₁ x₂ : M} {y₁ y₂ : ↥S} :

f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ ⇑(f.to_map) (x₁ + ↑y₂) = ⇑(f.to_map) (x₂ + ↑y₁)

source

@[protected]

theorem submonoid.localization_map.eq {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) {a₁ b₁ : M} {a₂ b₂ : ↥S} :

f.mk' a₁ a₂ = f.mk' b₁ b₂ ↔ ∃ (c : ↥S), ↑c * (↑b₂ * a₁) = ↑c * (↑a₂ * b₁)

source

@[protected]

theorem add_submonoid.localization_map.eq {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) {a₁ b₁ : M} {a₂ b₂ : ↥S} :

f.mk' a₁ a₂ = f.mk' b₁ b₂ ↔ ∃ (c : ↥S), ↑c + (↑b₂ + a₁) = ↑c + (↑a₂ + b₁)

source

@[protected]

theorem add_submonoid.localization_map.eq' {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) {a₁ b₁ : M} {a₂ b₂ : ↥S} :

f.mk' a₁ a₂ = f.mk' b₁ b₂ ↔ ⇑(add_localization.r S) (a₁, a₂) (b₁, b₂)

source

@[protected]

theorem submonoid.localization_map.eq' {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) {a₁ b₁ : M} {a₂ b₂ : ↥S} :

f.mk' a₁ a₂ = f.mk' b₁ b₂ ↔ ⇑(localization.r S) (a₁, a₂) (b₁, b₂)

source

theorem submonoid.localization_map.eq_iff_eq {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) (g : S.localization_map P) {x y : M} :

⇑(f.to_map) x = ⇑(f.to_map) y ↔ ⇑(g.to_map) x = ⇑(g.to_map) y

source

theorem add_submonoid.localization_map.eq_iff_eq {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) (g : S.localization_map P) {x y : M} :

⇑(f.to_map) x = ⇑(f.to_map) y ↔ ⇑(g.to_map) x = ⇑(g.to_map) y

source

theorem submonoid.localization_map.mk'_eq_iff_mk'_eq {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) (g : S.localization_map P) {x₁ x₂ : M} {y₁ y₂ : ↥S} :

f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ g.mk' x₁ y₁ = g.mk' x₂ y₂

source

theorem add_submonoid.localization_map.mk'_eq_iff_mk'_eq {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) (g : S.localization_map P) {x₁ x₂ : M} {y₁ y₂ : ↥S} :

f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ g.mk' x₁ y₁ = g.mk' x₂ y₂

source

theorem add_submonoid.localization_map.exists_of_sec_mk' {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) (x : M) (y : ↥S) :

∃ (c : ↥S), ↑c + (↑((f.sec (f.mk' x y)).snd) + x) = ↑c + (↑y + (f.sec (f.mk' x y)).fst)

Given a localization map f : M →+ N for a submonoid S ⊆ M, for all x₁ : M and y₁ ∈ S, if x₂ : M, y₂ ∈ S are such that (f x₁ - f y₁) + f y₂ = f x₂, then there exists c ∈ S such that x₁ + y₂ + c = x₂ + y₁ + c.

source

theorem submonoid.localization_map.exists_of_sec_mk' {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (x : M) (y : ↥S) :

∃ (c : ↥S), ↑c * (↑((f.sec (f.mk' x y)).snd) * x) = ↑c * (↑y * (f.sec (f.mk' x y)).fst)

Given a localization map f : M →* N for a submonoid S ⊆ M, for all x₁ : M and y₁ ∈ S, if x₂ : M, y₂ ∈ S are such that f x₁ * (f y₁)⁻¹ * f y₂ = f x₂, then there exists c ∈ S such that x₁ * y₂ * c = x₂ * y₁ * c.

source

theorem add_submonoid.localization_map.mk'_eq_of_eq {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) {a₁ b₁ : M} {a₂ b₂ : ↥S} (H : ↑a₂ + b₁ = ↑b₂ + a₁) :

f.mk' a₁ a₂ = f.mk' b₁ b₂

source

theorem submonoid.localization_map.mk'_eq_of_eq {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) {a₁ b₁ : M} {a₂ b₂ : ↥S} (H : ↑a₂ * b₁ = ↑b₂ * a₁) :

f.mk' a₁ a₂ = f.mk' b₁ b₂

source

theorem submonoid.localization_map.mk'_eq_of_eq' {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) {a₁ b₁ : M} {a₂ b₂ : ↥S} (H : b₁ * ↑a₂ = a₁ * ↑b₂) :

f.mk' a₁ a₂ = f.mk' b₁ b₂

source

theorem add_submonoid.localization_map.mk'_eq_of_eq' {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) {a₁ b₁ : M} {a₂ b₂ : ↥S} (H : b₁ + ↑a₂ = a₁ + ↑b₂) :

f.mk' a₁ a₂ = f.mk' b₁ b₂

source

@[simp]

theorem add_submonoid.localization_map.mk'_self' {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) (y : ↥S) :

f.mk' ↑y y = 0

source

@[simp]

theorem submonoid.localization_map.mk'_self' {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (y : ↥S) :

f.mk' ↑y y = 1

source

@[simp]

theorem add_submonoid.localization_map.mk'_self {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) (x : M) (H : x ∈ S) :

f.mk' x ⟨x, H⟩ = 0

source

@[simp]

theorem submonoid.localization_map.mk'_self {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (x : M) (H : x ∈ S) :

f.mk' x ⟨x, H⟩ = 1

source

theorem submonoid.localization_map.mul_mk'_eq_mk'_of_mul {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (x₁ x₂ : M) (y : ↥S) :

⇑(f.to_map) x₁ * f.mk' x₂ y = f.mk' (x₁ * x₂) y

source

theorem add_submonoid.localization_map.add_mk'_eq_mk'_of_add {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) (x₁ x₂ : M) (y : ↥S) :

⇑(f.to_map) x₁ + f.mk' x₂ y = f.mk' (x₁ + x₂) y

source

theorem add_submonoid.localization_map.mk'_add_eq_mk'_of_add {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) (x₁ x₂ : M) (y : ↥S) :

f.mk' x₂ y + ⇑(f.to_map) x₁ = f.mk' (x₁ + x₂) y

source

theorem submonoid.localization_map.mk'_mul_eq_mk'_of_mul {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (x₁ x₂ : M) (y : ↥S) :

f.mk' x₂ y * ⇑(f.to_map) x₁ = f.mk' (x₁ * x₂) y

source

theorem add_submonoid.localization_map.add_mk'_zero_eq_mk' {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) (x : M) (y : ↥S) :

⇑(f.to_map) x + f.mk' 0 y = f.mk' x y

source

theorem submonoid.localization_map.mul_mk'_one_eq_mk' {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (x : M) (y : ↥S) :

⇑(f.to_map) x * f.mk' 1 y = f.mk' x y

source

@[simp]

theorem submonoid.localization_map.mk'_mul_cancel_right {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (x : M) (y : ↥S) :

f.mk' (x * ↑y) y = ⇑(f.to_map) x

source

@[simp]

theorem add_submonoid.localization_map.mk'_add_cancel_right {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) (x : M) (y : ↥S) :

f.mk' (x + ↑y) y = ⇑(f.to_map) x

source

theorem add_submonoid.localization_map.mk'_add_cancel_left {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) (x : M) (y : ↥S) :

f.mk' (↑y + x) y = ⇑(f.to_map) x

source

theorem submonoid.localization_map.mk'_mul_cancel_left {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (x : M) (y : ↥S) :

f.mk' (↑y * x) y = ⇑(f.to_map) x

source

theorem submonoid.localization_map.is_unit_comp {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) (j : N →* P) (y : ↥S) :

is_unit (⇑(j.comp f.to_map) ↑y)

source

theorem add_submonoid.localization_map.is_add_unit_comp {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) (j : N →+ P) (y : ↥S) :

is_add_unit (⇑(j.comp f.to_map) ↑y)

source

theorem submonoid.localization_map.eq_of_eq {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} (hg : ∀ (y : ↥S), is_unit (⇑g ↑y)) {x y : M} (h : ⇑(f.to_map) x = ⇑(f.to_map) y) :

⇑g x = ⇑g y

Given a localization map f : M →* N for a submonoid S ⊆ M and a map of comm_monoids g : M →* P such that g(S) ⊆ units P, f x = f y → g x = g y for all x y : M.

source

theorem add_submonoid.localization_map.eq_of_eq {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {g : M →+ P} (hg : ∀ (y : ↥S), is_add_unit (⇑g ↑y)) {x y : M} (h : ⇑(f.to_map) x = ⇑(f.to_map) y) :

⇑g x = ⇑g y

Given a localization map f : M →+ N for a submonoid S ⊆ M and a map of add_comm_monoids g : M →+ P such that g(S) ⊆ add_units P, f x = f y → g x = g y for all x y : M.

source

theorem submonoid.localization_map.comp_eq_of_eq {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} {T : submonoid P} {Q : Type u_4} [comm_monoid Q] (hg : ∀ (y : ↥S), ⇑g ↑y ∈ T) (k : T.localization_map Q) {x y : M} (h : ⇑(f.to_map) x = ⇑(f.to_map) y) :

⇑(k.to_map) (⇑g x) = ⇑(k.to_map) (⇑g y)

Given comm_monoids M, P, localization maps f : M →* N, k : P →* Q for submonoids S, T respectively, and g : M →* P such that g(S) ⊆ T, f x = f y implies k (g x) = k (g y).

source

theorem add_submonoid.localization_map.comp_eq_of_eq {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {g : M →+ P} {T : add_submonoid P} {Q : Type u_4} [add_comm_monoid Q] (hg : ∀ (y : ↥S), ⇑g ↑y ∈ T) (k : T.localization_map Q) {x y : M} (h : ⇑(f.to_map) x = ⇑(f.to_map) y) :

⇑(k.to_map) (⇑g x) = ⇑(k.to_map) (⇑g y)

Given add_comm_monoids M, P, localization maps f : M →+ N, k : P →+ Q for submonoids S, T respectively, and g : M →+ P such that g(S) ⊆ T, f x = f y implies k (g x) = k (g y).

source

noncomputable def submonoid.localization_map.lift {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} (hg : ∀ (y : ↥S), is_unit (⇑g ↑y)) :

N →* P

Given a localization map f : M →* N for a submonoid S ⊆ M and a map of comm_monoids g : M →* P such that g y is invertible for all y : S, the homomorphism induced from N to P sending z : N to g x * (g y)⁻¹, where (x, y) : M × S are such that z = f x * (f y)⁻¹.

Equations

f.lift hg = {to_fun := λ (z : N), ⇑g (f.sec z).fst * ↑(⇑(is_unit.lift_right (g.restrict S) hg) (f.sec z).snd)⁻¹, map_one' := _, map_mul' := _}

source

noncomputable def add_submonoid.localization_map.lift {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {g : M →+ P} (hg : ∀ (y : ↥S), is_add_unit (⇑g ↑y)) :

N →+ P

Given a localization map f : M →+ N for a submonoid S ⊆ M and a map of add_comm_monoids g : M →+ P such that g y is invertible for all y : S, the homomorphism induced from N to P sending z : N to g x - g y, where (x, y) : M × S are such that z = f x - f y.

Equations

f.lift hg = {to_fun := λ (z : N), ⇑g (f.sec z).fst + ↑-⇑(is_add_unit.lift_right (g.restrict S) hg) (f.sec z).snd, map_zero' := _, map_add' := _}

source

theorem submonoid.localization_map.lift_mk' {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} (hg : ∀ (y : ↥S), is_unit (⇑g ↑y)) (x : M) (y : ↥S) :

⇑(f.lift hg) (f.mk' x y) = ⇑g x * ↑(⇑(is_unit.lift_right (g.restrict S) hg) y)⁻¹

Given a localization map f : M →* N for a submonoid S ⊆ M and a map of comm_monoids g : M →* P such that g y is invertible for all y : S, the homomorphism induced from N to P maps f x * (f y)⁻¹ to g x * (g y)⁻¹ for all x : M, y ∈ S.

source

theorem add_submonoid.localization_map.lift_mk' {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {g : M →+ P} (hg : ∀ (y : ↥S), is_add_unit (⇑g ↑y)) (x : M) (y : ↥S) :

⇑(f.lift hg) (f.mk' x y) = ⇑g x + ↑-⇑(is_add_unit.lift_right (g.restrict S) hg) y

Given a localization map f : M →+ N for a submonoid S ⊆ M and a map of add_comm_monoids g : M →+ P such that g y is invertible for all y : S, the homomorphism induced from N to P maps f x - f y to g x - g y for all x : M, y ∈ S.

source

theorem submonoid.localization_map.lift_spec {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} (hg : ∀ (y : ↥S), is_unit (⇑g ↑y)) (z : N) (v : P) :

⇑(f.lift hg) z = v ↔ ⇑g (f.sec z).fst = ⇑g ↑((f.sec z).snd) * v

Given a localization map f : M →* N for a submonoid S ⊆ M, if a comm_monoid map g : M →* P induces a map f.lift hg : N →* P then for all z : N, v : P, we have f.lift hg z = v ↔ g x = g y * v, where x : M, y ∈ S are such that z * f y = f x.

source

theorem add_submonoid.localization_map.lift_spec {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {g : M →+ P} (hg : ∀ (y : ↥S), is_add_unit (⇑g ↑y)) (z : N) (v : P) :

⇑(f.lift hg) z = v ↔ ⇑g (f.sec z).fst = ⇑g ↑((f.sec z).snd) + v

Given a localization map f : M →+ N for a submonoid S ⊆ M, if an add_comm_monoid map g : M →+ P induces a map f.lift hg : N →+ P then for all z : N, v : P, we have f.lift hg z = v ↔ g x = g y + v, where x : M, y ∈ S are such that z + f y = f x.

source

theorem submonoid.localization_map.lift_spec_mul {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} (hg : ∀ (y : ↥S), is_unit (⇑g ↑y)) (z : N) (w v : P) :

⇑(f.lift hg) z * w = v ↔ ⇑g (f.sec z).fst * w = ⇑g ↑((f.sec z).snd) * v

Given a localization map f : M →* N for a submonoid S ⊆ M, if a comm_monoid map g : M →* P induces a map f.lift hg : N →* P then for all z : N, v w : P, we have f.lift hg z * w = v ↔ g x * w = g y * v, where x : M, y ∈ S are such that z * f y = f x.

source

theorem add_submonoid.localization_map.lift_spec_add {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {g : M →+ P} (hg : ∀ (y : ↥S), is_add_unit (⇑g ↑y)) (z : N) (w v : P) :

⇑(f.lift hg) z + w = v ↔ ⇑g (f.sec z).fst + w = ⇑g ↑((f.sec z).snd) + v

Given a localization map f : M →+ N for a submonoid S ⊆ M, if an add_comm_monoid map g : M →+ P induces a map f.lift hg : N →+ P then for all z : N, v w : P, we have f.lift hg z + w = v ↔ g x + w = g y + v, where x : M, y ∈ S are such that z + f y = f x.

source

theorem add_submonoid.localization_map.lift_mk'_spec {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {g : M →+ P} (hg : ∀ (y : ↥S), is_add_unit (⇑g ↑y)) (x : M) (v : P) (y : ↥S) :

⇑(f.lift hg) (f.mk' x y) = v ↔ ⇑g x = ⇑g ↑y + v

source

theorem submonoid.localization_map.lift_mk'_spec {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} (hg : ∀ (y : ↥S), is_unit (⇑g ↑y)) (x : M) (v : P) (y : ↥S) :

⇑(f.lift hg) (f.mk' x y) = v ↔ ⇑g x = ⇑g ↑y * v

source

theorem submonoid.localization_map.lift_mul_right {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} (hg : ∀ (y : ↥S), is_unit (⇑g ↑y)) (z : N) :

⇑(f.lift hg) z * ⇑g ↑((f.sec z).snd) = ⇑g (f.sec z).fst

Given a localization map f : M →* N for a submonoid S ⊆ M, if a comm_monoid map g : M →* P induces a map f.lift hg : N →* P then for all z : N, we have f.lift hg z * g y = g x, where x : M, y ∈ S are such that z * f y = f x.

source

theorem add_submonoid.localization_map.lift_add_right {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {g : M →+ P} (hg : ∀ (y : ↥S), is_add_unit (⇑g ↑y)) (z : N) :

⇑(f.lift hg) z + ⇑g ↑((f.sec z).snd) = ⇑g (f.sec z).fst

Given a localization map f : M →+ N for a submonoid S ⊆ M, if an add_comm_monoid map g : M →+ P induces a map f.lift hg : N →+ P then for all z : N, we have f.lift hg z + g y = g x, where x : M, y ∈ S are such that z + f y = f x.

source

theorem add_submonoid.localization_map.lift_add_left {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {g : M →+ P} (hg : ∀ (y : ↥S), is_add_unit (⇑g ↑y)) (z : N) :

⇑g ↑((f.sec z).snd) + ⇑(f.lift hg) z = ⇑g (f.sec z).fst

Given a localization map f : M →+ N for a submonoid S ⊆ M, if an add_comm_monoid map g : M →+ P induces a map f.lift hg : N →+ P then for all z : N, we have g y + f.lift hg z = g x, where x : M, y ∈ S are such that z + f y = f x.

source

theorem submonoid.localization_map.lift_mul_left {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} (hg : ∀ (y : ↥S), is_unit (⇑g ↑y)) (z : N) :

⇑g ↑((f.sec z).snd) * ⇑(f.lift hg) z = ⇑g (f.sec z).fst

Given a localization map f : M →* N for a submonoid S ⊆ M, if a comm_monoid map g : M →* P induces a map f.lift hg : N →* P then for all z : N, we have g y * f.lift hg z = g x, where x : M, y ∈ S are such that z * f y = f x.

source

@[simp]

theorem submonoid.localization_map.lift_eq {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} (hg : ∀ (y : ↥S), is_unit (⇑g ↑y)) (x : M) :

⇑(f.lift hg) (⇑(f.to_map) x) = ⇑g x

source

@[simp]

theorem add_submonoid.localization_map.lift_eq {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {g : M →+ P} (hg : ∀ (y : ↥S), is_add_unit (⇑g ↑y)) (x : M) :

⇑(f.lift hg) (⇑(f.to_map) x) = ⇑g x

source

theorem submonoid.localization_map.lift_eq_iff {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} (hg : ∀ (y : ↥S), is_unit (⇑g ↑y)) {x y : M × ↥S} :

⇑(f.lift hg) (f.mk' x.fst x.snd) = ⇑(f.lift hg) (f.mk' y.fst y.snd) ↔ ⇑g (x.fst * ↑(y.snd)) = ⇑g (y.fst * ↑(x.snd))

source

theorem add_submonoid.localization_map.lift_eq_iff {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {g : M →+ P} (hg : ∀ (y : ↥S), is_add_unit (⇑g ↑y)) {x y : M × ↥S} :

⇑(f.lift hg) (f.mk' x.fst x.snd) = ⇑(f.lift hg) (f.mk' y.fst y.snd) ↔ ⇑g (x.fst + ↑(y.snd)) = ⇑g (y.fst + ↑(x.snd))

source

@[simp]

theorem add_submonoid.localization_map.lift_comp {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {g : M →+ P} (hg : ∀ (y : ↥S), is_add_unit (⇑g ↑y)) :

(f.lift hg).comp f.to_map = g

source

@[simp]

theorem submonoid.localization_map.lift_comp {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} (hg : ∀ (y : ↥S), is_unit (⇑g ↑y)) :

(f.lift hg).comp f.to_map = g

source

@[simp]

theorem add_submonoid.localization_map.lift_of_comp {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) (j : N →+ P) :

f.lift _ = j

source

@[simp]

theorem submonoid.localization_map.lift_of_comp {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) (j : N →* P) :

f.lift _ = j

source

theorem submonoid.localization_map.epic_of_localization_map {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {j k : N →* P} (h : ∀ (a : M), ⇑(j.comp f.to_map) a = ⇑(k.comp f.to_map) a) :

j = k

source

theorem add_submonoid.localization_map.epic_of_localization_map {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {j k : N →+ P} (h : ∀ (a : M), ⇑(j.comp f.to_map) a = ⇑(k.comp f.to_map) a) :

j = k

source

theorem add_submonoid.localization_map.lift_unique {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {g : M →+ P} (hg : ∀ (y : ↥S), is_add_unit (⇑g ↑y)) {j : N →+ P} (hj : ∀ (x : M), ⇑j (⇑(f.to_map) x) = ⇑g x) :

f.lift hg = j

source

theorem submonoid.localization_map.lift_unique {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} (hg : ∀ (y : ↥S), is_unit (⇑g ↑y)) {j : N →* P} (hj : ∀ (x : M), ⇑j (⇑(f.to_map) x) = ⇑g x) :

f.lift hg = j

source

@[simp]

theorem add_submonoid.localization_map.lift_id {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) (x : N) :

⇑(f.lift _) x = x

source

@[simp]

theorem submonoid.localization_map.lift_id {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (x : N) :

⇑(f.lift _) x = x

source

@[simp]

theorem add_submonoid.localization_map.lift_left_inverse {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {k : S.localization_map P} (z : N) :

⇑(k.lift _) (⇑(f.lift _) z) = z

Given two localization maps f : M →+ N, k : M →+ P for a submonoid S ⊆ M, the hom from P to N induced by f is left inverse to the hom from N to P induced by k.

source

@[simp]

theorem submonoid.localization_map.lift_left_inverse {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {k : S.localization_map P} (z : N) :

⇑(k.lift _) (⇑(f.lift _) z) = z

Given two localization maps f : M →* N, k : M →* P for a submonoid S ⊆ M, the hom from P to N induced by f is left inverse to the hom from N to P induced by k.

source

theorem add_submonoid.localization_map.lift_surjective_iff {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {g : M →+ P} (hg : ∀ (y : ↥S), is_add_unit (⇑g ↑y)) :

function.surjective ⇑(f.lift hg) ↔ ∀ (v : P), ∃ (x : M × ↥S), v + ⇑g ↑(x.snd) = ⇑g x.fst

source

theorem submonoid.localization_map.lift_surjective_iff {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} (hg : ∀ (y : ↥S), is_unit (⇑g ↑y)) :

function.surjective ⇑(f.lift hg) ↔ ∀ (v : P), ∃ (x : M × ↥S), v * ⇑g ↑(x.snd) = ⇑g x.fst

source

theorem submonoid.localization_map.lift_injective_iff {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} (hg : ∀ (y : ↥S), is_unit (⇑g ↑y)) :

function.injective ⇑(f.lift hg) ↔ ∀ (x y : M), ⇑(f.to_map) x = ⇑(f.to_map) y ↔ ⇑g x = ⇑g y

source

theorem add_submonoid.localization_map.lift_injective_iff {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {g : M →+ P} (hg : ∀ (y : ↥S), is_add_unit (⇑g ↑y)) :

function.injective ⇑(f.lift hg) ↔ ∀ (x y : M), ⇑(f.to_map) x = ⇑(f.to_map) y ↔ ⇑g x = ⇑g y

source

noncomputable def add_submonoid.localization_map.map {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {g : M →+ P} {T : add_submonoid P} (hy : ∀ (y : ↥S), ⇑g ↑y ∈ T) {Q : Type u_4} [add_comm_monoid Q] (k : T.localization_map Q) :

N →+ Q

Given a add_comm_monoid homomorphism g : M →+ P where for submonoids S ⊆ M, T ⊆ P we have g(S) ⊆ T, the induced add_monoid homomorphism from the localization of M at S to the localization of P at T: if f : M →+ N and k : P →+ Q are localization maps for S and T respectively, we send z : N to k (g x) - k (g y), where (x, y) : M × S are such that z = f x - f y.

Equations

f.map hy k = f.lift _

source

noncomputable def submonoid.localization_map.map {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} {T : submonoid P} (hy : ∀ (y : ↥S), ⇑g ↑y ∈ T) {Q : Type u_4} [comm_monoid Q] (k : T.localization_map Q) :

N →* Q

Given a comm_monoid homomorphism g : M →* P where for submonoids S ⊆ M, T ⊆ P we have g(S) ⊆ T, the induced monoid homomorphism from the localization of M at S to the localization of P at T: if f : M →* N and k : P →* Q are localization maps for S and T respectively, we send z : N to k (g x) * (k (g y))⁻¹, where (x, y) : M × S are such that z = f x * (f y)⁻¹.

Equations

f.map hy k = f.lift _

source

theorem submonoid.localization_map.map_eq {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} {T : submonoid P} (hy : ∀ (y : ↥S), ⇑g ↑y ∈ T) {Q : Type u_4} [comm_monoid Q] {k : T.localization_map Q} (x : M) :

⇑(f.map hy k) (⇑(f.to_map) x) = ⇑(k.to_map) (⇑g x)

source

theorem add_submonoid.localization_map.map_eq {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {g : M →+ P} {T : add_submonoid P} (hy : ∀ (y : ↥S), ⇑g ↑y ∈ T) {Q : Type u_4} [add_comm_monoid Q] {k : T.localization_map Q} (x : M) :

⇑(f.map hy k) (⇑(f.to_map) x) = ⇑(k.to_map) (⇑g x)

source

@[simp]

theorem add_submonoid.localization_map.map_comp {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {g : M →+ P} {T : add_submonoid P} (hy : ∀ (y : ↥S), ⇑g ↑y ∈ T) {Q : Type u_4} [add_comm_monoid Q] {k : T.localization_map Q} :

(f.map hy k).comp f.to_map = k.to_map.comp g

source

@[simp]

theorem submonoid.localization_map.map_comp {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} {T : submonoid P} (hy : ∀ (y : ↥S), ⇑g ↑y ∈ T) {Q : Type u_4} [comm_monoid Q] {k : T.localization_map Q} :

(f.map hy k).comp f.to_map = k.to_map.comp g

source

theorem add_submonoid.localization_map.map_mk' {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {g : M →+ P} {T : add_submonoid P} (hy : ∀ (y : ↥S), ⇑g ↑y ∈ T) {Q : Type u_4} [add_comm_monoid Q] {k : T.localization_map Q} (x : M) (y : ↥S) :

⇑(f.map hy k) (f.mk' x y) = k.mk' (⇑g x) ⟨⇑g ↑y, _⟩

source

theorem submonoid.localization_map.map_mk' {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} {T : submonoid P} (hy : ∀ (y : ↥S), ⇑g ↑y ∈ T) {Q : Type u_4} [comm_monoid Q] {k : T.localization_map Q} (x : M) (y : ↥S) :

⇑(f.map hy k) (f.mk' x y) = k.mk' (⇑g x) ⟨⇑g ↑y, _⟩

source

theorem add_submonoid.localization_map.map_spec {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {g : M →+ P} {T : add_submonoid P} (hy : ∀ (y : ↥S), ⇑g ↑y ∈ T) {Q : Type u_4} [add_comm_monoid Q] {k : T.localization_map Q} (z : N) (u : Q) :

⇑(f.map hy k) z = u ↔ ⇑(k.to_map) (⇑g (f.sec z).fst) = ⇑(k.to_map) (⇑g ↑((f.sec z).snd)) + u

Given localization maps f : M →+ N, k : P →+ Q for submonoids S, T respectively, if an add_comm_monoid homomorphism g : M →+ P induces a f.map hy k : N →+ Q, then for all z : N, u : Q, we have f.map hy k z = u ↔ k (g x) = k (g y) + u where x : M, y ∈ S are such that z + f y = f x.

source

theorem submonoid.localization_map.map_spec {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} {T : submonoid P} (hy : ∀ (y : ↥S), ⇑g ↑y ∈ T) {Q : Type u_4} [comm_monoid Q] {k : T.localization_map Q} (z : N) (u : Q) :

⇑(f.map hy k) z = u ↔ ⇑(k.to_map) (⇑g (f.sec z).fst) = ⇑(k.to_map) (⇑g ↑((f.sec z).snd)) * u

Given localization maps f : M →* N, k : P →* Q for submonoids S, T respectively, if a comm_monoid homomorphism g : M →* P induces a f.map hy k : N →* Q, then for all z : N, u : Q, we have f.map hy k z = u ↔ k (g x) = k (g y) * u where x : M, y ∈ S are such that z * f y = f x.

source

theorem submonoid.localization_map.map_mul_right {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} {T : submonoid P} (hy : ∀ (y : ↥S), ⇑g ↑y ∈ T) {Q : Type u_4} [comm_monoid Q] {k : T.localization_map Q} (z : N) :

⇑(f.map hy k) z * ⇑(k.to_map) (⇑g ↑((f.sec z).snd)) = ⇑(k.to_map) (⇑g (f.sec z).fst)

Given localization maps f : M →* N, k : P →* Q for submonoids S, T respectively, if a comm_monoid homomorphism g : M →* P induces a f.map hy k : N →* Q, then for all z : N, we have f.map hy k z * k (g y) = k (g x) where x : M, y ∈ S are such that z * f y = f x.

source

theorem add_submonoid.localization_map.map_add_right {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {g : M →+ P} {T : add_submonoid P} (hy : ∀ (y : ↥S), ⇑g ↑y ∈ T) {Q : Type u_4} [add_comm_monoid Q] {k : T.localization_map Q} (z : N) :

⇑(f.map hy k) z + ⇑(k.to_map) (⇑g ↑((f.sec z).snd)) = ⇑(k.to_map) (⇑g (f.sec z).fst)

Given localization maps f : M →+ N, k : P →+ Q for submonoids S, T respectively, if an add_comm_monoid homomorphism g : M →+ P induces a f.map hy k : N →+ Q, then for all z : N, we have f.map hy k z + k (g y) = k (g x) where x : M, y ∈ S are such that z + f y = f x.

source

theorem add_submonoid.localization_map.map_add_left {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {g : M →+ P} {T : add_submonoid P} (hy : ∀ (y : ↥S), ⇑g ↑y ∈ T) {Q : Type u_4} [add_comm_monoid Q] {k : T.localization_map Q} (z : N) :

⇑(k.to_map) (⇑g ↑((f.sec z).snd)) + ⇑(f.map hy k) z = ⇑(k.to_map) (⇑g (f.sec z).fst)

Given localization maps f : M →+ N, k : P →+ Q for submonoids S, T respectively, if an add_comm_monoid homomorphism g : M →+ P induces a f.map hy k : N →+ Q, then for all z : N, we have k (g y) + f.map hy k z = k (g x) where x : M, y ∈ S are such that z + f y = f x.

source

theorem submonoid.localization_map.map_mul_left {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} {T : submonoid P} (hy : ∀ (y : ↥S), ⇑g ↑y ∈ T) {Q : Type u_4} [comm_monoid Q] {k : T.localization_map Q} (z : N) :

⇑(k.to_map) (⇑g ↑((f.sec z).snd)) * ⇑(f.map hy k) z = ⇑(k.to_map) (⇑g (f.sec z).fst)

Given localization maps f : M →* N, k : P →* Q for submonoids S, T respectively, if a comm_monoid homomorphism g : M →* P induces a f.map hy k : N →* Q, then for all z : N, we have k (g y) * f.map hy k z = k (g x) where x : M, y ∈ S are such that z * f y = f x.

source

@[simp]

theorem add_submonoid.localization_map.map_id {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) (z : N) :

⇑(f.map _ f) z = z

source

@[simp]

theorem submonoid.localization_map.map_id {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) (z : N) :

⇑(f.map _ f) z = z

source

theorem add_submonoid.localization_map.map_comp_map {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {g : M →+ P} {T : add_submonoid P} (hy : ∀ (y : ↥S), ⇑g ↑y ∈ T) {Q : Type u_4} [add_comm_monoid Q] {k : T.localization_map Q} {A : Type u_5} [add_comm_monoid A] {U : add_submonoid A} {R : Type u_6} [add_comm_monoid R] (j : U.localization_map R) {l : P →+ A} (hl : ∀ (w : ↥T), ⇑l ↑w ∈ U) :

(k.map hl j).comp (f.map hy k) = f.map _ j

If add_comm_monoid homs g : M →+ P, l : P →+ A induce maps of localizations, the composition of the induced maps equals the map of localizations induced by l ∘ g.

source

theorem submonoid.localization_map.map_comp_map {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} {T : submonoid P} (hy : ∀ (y : ↥S), ⇑g ↑y ∈ T) {Q : Type u_4} [comm_monoid Q] {k : T.localization_map Q} {A : Type u_5} [comm_monoid A] {U : submonoid A} {R : Type u_6} [comm_monoid R] (j : U.localization_map R) {l : P →* A} (hl : ∀ (w : ↥T), ⇑l ↑w ∈ U) :

(k.map hl j).comp (f.map hy k) = f.map _ j

If comm_monoid homs g : M →* P, l : P →* A induce maps of localizations, the composition of the induced maps equals the map of localizations induced by l ∘ g.

source

theorem add_submonoid.localization_map.map_map {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {g : M →+ P} {T : add_submonoid P} (hy : ∀ (y : ↥S), ⇑g ↑y ∈ T) {Q : Type u_4} [add_comm_monoid Q] {k : T.localization_map Q} {A : Type u_5} [add_comm_monoid A] {U : add_submonoid A} {R : Type u_6} [add_comm_monoid R] (j : U.localization_map R) {l : P →+ A} (hl : ∀ (w : ↥T), ⇑l ↑w ∈ U) (x : N) :

⇑(k.map hl j) (⇑(f.map hy k) x) = ⇑(f.map _ j) x

If add_comm_monoid homs g : M →+ P, l : P →+ A induce maps of localizations, the composition of the induced maps equals the map of localizations induced by l ∘ g.

source

theorem submonoid.localization_map.map_map {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {g : M →* P} {T : submonoid P} (hy : ∀ (y : ↥S), ⇑g ↑y ∈ T) {Q : Type u_4} [comm_monoid Q] {k : T.localization_map Q} {A : Type u_5} [comm_monoid A] {U : submonoid A} {R : Type u_6} [comm_monoid R] (j : U.localization_map R) {l : P →* A} (hl : ∀ (w : ↥T), ⇑l ↑w ∈ U) (x : N) :

⇑(k.map hl j) (⇑(f.map hy k) x) = ⇑(f.map _ j) x

If comm_monoid homs g : M →* P, l : P →* A induce maps of localizations, the composition of the induced maps equals the map of localizations induced by l ∘ g.

source

@[reducible]

def submonoid.localization_map.away_map {M : Type u_1} [comm_monoid M] (x : M) (N' : Type u_2) [comm_monoid N'] :

Type (max u_1 u_2)

Given x : M, the type of comm_monoid homomorphisms f : M →* N such that N is isomorphic to the localization of M at the submonoid generated by x.

Equations

submonoid.localization_map.away_map x N' = (submonoid.powers x).localization_map N'

source

@[reducible]

def add_submonoid.localization_map.away_map {M : Type u_1} [add_comm_monoid M] (x : M) (N' : Type u_2) [add_comm_monoid N'] :

Type (max u_1 u_2)

Given x : M, the type of add_comm_monoid homomorphisms f : M →+ N such that N is isomorphic to the localization of M at the submonoid generated by x.

Equations

add_submonoid.localization_map.away_map x N' = (add_submonoid.multiples x).localization_map N'

source

noncomputable def submonoid.localization_map.away_map.inv_self {M : Type u_1} [comm_monoid M] {N : Type u_2} [comm_monoid N] (x : M) (F : submonoid.localization_map.away_map x N) :

N

Given x : M and a localization map F : M →* N away from x, inv_self is (F x)⁻¹.

Equations

submonoid.localization_map.away_map.inv_self x F = submonoid.localization_map.mk' F 1 ⟨x, _⟩

source

noncomputable def submonoid.localization_map.away_map.lift {M : Type u_1} [comm_monoid M] {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] {g : M →* P} (x : M) (F : submonoid.localization_map.away_map x N) (hg : is_unit (⇑g x)) :

N →* P

Given x : M, a localization map F : M →* N away from x, and a map of comm_monoids g : M →* P such that g x is invertible, the homomorphism induced from N to P sending z : N to g y * (g x)⁻ⁿ, where y : M, n : ℕ are such that z = F y * (F x)⁻ⁿ.

Equations

submonoid.localization_map.away_map.lift x F hg = submonoid.localization_map.lift F _

source

@[simp]

theorem submonoid.localization_map.away_map.lift_eq {M : Type u_1} [comm_monoid M] {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] {g : M →* P} (x : M) (F : submonoid.localization_map.away_map x N) (hg : is_unit (⇑g x)) (a : M) :

⇑(submonoid.localization_map.away_map.lift x F hg) (⇑(submonoid.localization_map.to_map F) a) = ⇑g a

source

@[simp]

theorem submonoid.localization_map.away_map.lift_comp {M : Type u_1} [comm_monoid M] {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] {g : M →* P} (x : M) (F : submonoid.localization_map.away_map x N) (hg : is_unit (⇑g x)) :

(submonoid.localization_map.away_map.lift x F hg).comp (submonoid.localization_map.to_map F) = g

source

noncomputable def submonoid.localization_map.away_to_away_right {M : Type u_1} [comm_monoid M] {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (x : M) (F : submonoid.localization_map.away_map x N) (y : M) (G : submonoid.localization_map.away_map (x * y) P) :

N →* P

Given x y : M and localization maps F : M →* N, G : M →* P away from x and x * y respectively, the homomorphism induced from N to P.

Equations

submonoid.localization_map.away_to_away_right x F y G = submonoid.localization_map.away_map.lift x F _

source

noncomputable def add_submonoid.localization_map.away_map.neg_self {A : Type u_4} [add_comm_monoid A] (x : A) {B : Type u_5} [add_comm_monoid B] (F : add_submonoid.localization_map.away_map x B) :

B

Given x : A and a localization map F : A →+ B away from x, neg_self is - (F x).

Equations

add_submonoid.localization_map.away_map.neg_self x F = add_submonoid.localization_map.mk' F 0 ⟨x, _⟩

source

noncomputable def add_submonoid.localization_map.away_map.lift {A : Type u_4} [add_comm_monoid A] (x : A) {B : Type u_5} [add_comm_monoid B] (F : add_submonoid.localization_map.away_map x B) {C : Type u_6} [add_comm_monoid C] {g : A →+ C} (hg : is_add_unit (⇑g x)) :

B →+ C

Given x : A, a localization map F : A →+ B away from x, and a map of add_comm_monoids g : A →+ C such that g x is invertible, the homomorphism induced from B to C sending z : B to g y - n • g x, where y : A, n : ℕ are such that z = F y - n • F x.

Equations

add_submonoid.localization_map.away_map.lift x F hg = add_submonoid.localization_map.lift F _

source

@[simp]

theorem add_submonoid.localization_map.away_map.lift_eq {A : Type u_4} [add_comm_monoid A] (x : A) {B : Type u_5} [add_comm_monoid B] (F : add_submonoid.localization_map.away_map x B) {C : Type u_6} [add_comm_monoid C] {g : A →+ C} (hg : is_add_unit (⇑g x)) (a : A) :

⇑(add_submonoid.localization_map.away_map.lift x F hg) (⇑(add_submonoid.localization_map.to_map F) a) = ⇑g a

source

@[simp]

theorem add_submonoid.localization_map.away_map.lift_comp {A : Type u_4} [add_comm_monoid A] (x : A) {B : Type u_5} [add_comm_monoid B] (F : add_submonoid.localization_map.away_map x B) {C : Type u_6} [add_comm_monoid C] {g : A →+ C} (hg : is_add_unit (⇑g x)) :

(add_submonoid.localization_map.away_map.lift x F hg).comp (add_submonoid.localization_map.to_map F) = g

source

noncomputable def add_submonoid.localization_map.away_to_away_right {A : Type u_4} [add_comm_monoid A] (x : A) {B : Type u_5} [add_comm_monoid B] (F : add_submonoid.localization_map.away_map x B) {C : Type u_6} [add_comm_monoid C] (y : A) (G : add_submonoid.localization_map.away_map (x + y) C) :

B →+ C

Given x y : A and localization maps F : A →+ B, G : A →+ C away from x and x + y respectively, the homomorphism induced from B to C.

Equations

add_submonoid.localization_map.away_to_away_right x F y G = add_submonoid.localization_map.away_map.lift x F _

source

noncomputable def add_submonoid.localization_map.add_equiv_of_localizations {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) (k : S.localization_map P) :

N ≃+ P

If f : M →+ N and k : M →+ R are localization maps for a submonoid S, we get an isomorphism of N and R.

Equations

f.add_equiv_of_localizations k = {to_fun := ⇑(f.lift _), inv_fun := ⇑(k.lift _), left_inv := _, right_inv := _, map_add' := _}

source

noncomputable def submonoid.localization_map.mul_equiv_of_localizations {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) (k : S.localization_map P) :

N ≃* P

If f : M →* N and k : M →* P are localization maps for a submonoid S, we get an isomorphism of N and P.

Equations

f.mul_equiv_of_localizations k = {to_fun := ⇑(f.lift _), inv_fun := ⇑(k.lift _), left_inv := _, right_inv := _, map_mul' := _}

source

@[simp]

theorem submonoid.localization_map.mul_equiv_of_localizations_apply {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {k : S.localization_map P} {x : N} :

⇑(f.mul_equiv_of_localizations k) x = ⇑(f.lift _) x

source

@[simp]

theorem add_submonoid.localization_map.add_equiv_of_localizations_apply {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {k : S.localization_map P} {x : N} :

⇑(f.add_equiv_of_localizations k) x = ⇑(f.lift _) x

source

@[simp]

theorem add_submonoid.localization_map.add_equiv_of_localizations_symm_apply {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {k : S.localization_map P} {x : P} :

⇑((f.add_equiv_of_localizations k).symm) x = ⇑(k.lift _) x

source

@[simp]

theorem submonoid.localization_map.mul_equiv_of_localizations_symm_apply {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {k : S.localization_map P} {x : P} :

⇑((f.mul_equiv_of_localizations k).symm) x = ⇑(k.lift _) x

source

theorem add_submonoid.localization_map.add_equiv_of_localizations_symm_eq_add_equiv_of_localizations {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {k : S.localization_map P} :

(k.add_equiv_of_localizations f).symm = f.add_equiv_of_localizations k

source

theorem submonoid.localization_map.mul_equiv_of_localizations_symm_eq_mul_equiv_of_localizations {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {k : S.localization_map P} :

(k.mul_equiv_of_localizations f).symm = f.mul_equiv_of_localizations k

source

def add_submonoid.localization_map.of_add_equiv_of_localizations {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) (k : N ≃+ P) :

S.localization_map P

If f : M →+ N is a localization map for a submonoid S and k : N ≃+ P is an isomorphism of add_comm_monoids, k ∘ f is a localization map for M at S.

Equations

f.of_add_equiv_of_localizations k = (k.to_add_monoid_hom.comp f.to_map).to_localization_map _ _ _

source

def submonoid.localization_map.of_mul_equiv_of_localizations {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) (k : N ≃* P) :

S.localization_map P

If f : M →* N is a localization map for a submonoid S and k : N ≃* P is an isomorphism of comm_monoids, k ∘ f is a localization map for M at S.

Equations

f.of_mul_equiv_of_localizations k = (k.to_monoid_hom.comp f.to_map).to_localization_map _ _ _

source

@[simp]

theorem add_submonoid.localization_map.of_add_equiv_of_localizations_apply {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {k : N ≃+ P} (x : M) :

⇑((f.of_add_equiv_of_localizations k).to_map) x = ⇑k (⇑(f.to_map) x)

source

@[simp]

theorem submonoid.localization_map.of_mul_equiv_of_localizations_apply {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {k : N ≃* P} (x : M) :

⇑((f.of_mul_equiv_of_localizations k).to_map) x = ⇑k (⇑(f.to_map) x)

source

theorem add_submonoid.localization_map.of_add_equiv_of_localizations_eq {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {k : N ≃+ P} :

(f.of_add_equiv_of_localizations k).to_map = k.to_add_monoid_hom.comp f.to_map

source

theorem submonoid.localization_map.of_mul_equiv_of_localizations_eq {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {k : N ≃* P} :

(f.of_mul_equiv_of_localizations k).to_map = k.to_monoid_hom.comp f.to_map

source

theorem submonoid.localization_map.symm_comp_of_mul_equiv_of_localizations_apply {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {k : N ≃* P} (x : M) :

⇑(k.symm) (⇑((f.of_mul_equiv_of_localizations k).to_map) x) = ⇑(f.to_map) x

source

theorem add_submonoid.localization_map.symm_comp_of_add_equiv_of_localizations_apply {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {k : N ≃+ P} (x : M) :

⇑(k.symm) (⇑((f.of_add_equiv_of_localizations k).to_map) x) = ⇑(f.to_map) x

source

theorem add_submonoid.localization_map.symm_comp_of_add_equiv_of_localizations_apply' {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {k : P ≃+ N} (x : M) :

⇑k (⇑((f.of_add_equiv_of_localizations k.symm).to_map) x) = ⇑(f.to_map) x

source

theorem submonoid.localization_map.symm_comp_of_mul_equiv_of_localizations_apply' {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {k : P ≃* N} (x : M) :

⇑k (⇑((f.of_mul_equiv_of_localizations k.symm).to_map) x) = ⇑(f.to_map) x

source

theorem add_submonoid.localization_map.of_add_equiv_of_localizations_eq_iff_eq {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {k : N ≃+ P} {x : M} {y : P} :

⇑((f.of_add_equiv_of_localizations k).to_map) x = y ↔ ⇑(f.to_map) x = ⇑(k.symm) y

source

theorem submonoid.localization_map.of_mul_equiv_of_localizations_eq_iff_eq {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {k : N ≃* P} {x : M} {y : P} :

⇑((f.of_mul_equiv_of_localizations k).to_map) x = y ↔ ⇑(f.to_map) x = ⇑(k.symm) y

source

theorem submonoid.localization_map.mul_equiv_of_localizations_right_inv {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) (k : S.localization_map P) :

f.of_mul_equiv_of_localizations (f.mul_equiv_of_localizations k) = k

source

theorem add_submonoid.localization_map.add_equiv_of_localizations_right_inv {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) (k : S.localization_map P) :

f.of_add_equiv_of_localizations (f.add_equiv_of_localizations k) = k

source

@[simp]

theorem submonoid.localization_map.mul_equiv_of_localizations_right_inv_apply {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {k : S.localization_map P} {x : M} :

⇑((f.of_mul_equiv_of_localizations (f.mul_equiv_of_localizations k)).to_map) x = ⇑(k.to_map) x

source

@[simp]

theorem add_submonoid.localization_map.add_equiv_of_localizations_right_inv_apply {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {k : S.localization_map P} {x : M} :

⇑((f.of_add_equiv_of_localizations (f.add_equiv_of_localizations k)).to_map) x = ⇑(k.to_map) x

source

theorem submonoid.localization_map.mul_equiv_of_localizations_left_inv {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) (k : N ≃* P) :

f.mul_equiv_of_localizations (f.of_mul_equiv_of_localizations k) = k

source

theorem add_submonoid.localization_map.add_equiv_of_localizations_left_neg {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) (k : N ≃+ P) :

f.add_equiv_of_localizations (f.of_add_equiv_of_localizations k) = k

source

@[simp]

theorem submonoid.localization_map.mul_equiv_of_localizations_left_inv_apply {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {k : N ≃* P} (x : N) :

⇑(f.mul_equiv_of_localizations (f.of_mul_equiv_of_localizations k)) x = ⇑k x

source

@[simp]

theorem add_submonoid.localization_map.add_equiv_of_localizations_left_neg_apply {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {k : N ≃+ P} (x : N) :

⇑(f.add_equiv_of_localizations (f.of_add_equiv_of_localizations k)) x = ⇑k x

source

@[simp]

theorem add_submonoid.localization_map.of_add_equiv_of_localizations_id {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) :

f.of_add_equiv_of_localizations (add_equiv.refl N) = f

source

@[simp]

theorem submonoid.localization_map.of_mul_equiv_of_localizations_id {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) :

f.of_mul_equiv_of_localizations (mul_equiv.refl N) = f

source

theorem submonoid.localization_map.of_mul_equiv_of_localizations_comp {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {Q : Type u_4} [comm_monoid Q] {k : N ≃* P} {j : P ≃* Q} :

(f.of_mul_equiv_of_localizations (k.trans j)).to_map = j.to_monoid_hom.comp (f.of_mul_equiv_of_localizations k).to_map

source

theorem add_submonoid.localization_map.of_add_equiv_of_localizations_comp {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {Q : Type u_4} [add_comm_monoid Q] {k : N ≃+ P} {j : P ≃+ Q} :

(f.of_add_equiv_of_localizations (k.trans j)).to_map = j.to_add_monoid_hom.comp (f.of_add_equiv_of_localizations k).to_map

source

def add_submonoid.localization_map.of_add_equiv_of_dom {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {T : add_submonoid P} {k : P ≃+ M} (H : add_submonoid.map k.to_add_monoid_hom T = S) :

T.localization_map N

Given comm_monoids M, P and submonoids S ⊆ M, T ⊆ P, if f : M →* N is a localization map for S and k : P ≃* M is an isomorphism of comm_monoids such that k(T) = S, f ∘ k is a localization map for T.

Equations

f.of_add_equiv_of_dom H = let H' : add_submonoid.comap k.to_add_monoid_hom S = T := _ in (f.to_map.comp k.to_add_monoid_hom).to_localization_map _ _ _

source

def submonoid.localization_map.of_mul_equiv_of_dom {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {T : submonoid P} {k : P ≃* M} (H : submonoid.map k.to_monoid_hom T = S) :

T.localization_map N

Given comm_monoids M, P and submonoids S ⊆ M, T ⊆ P, if f : M →* N is a localization map for S and k : P ≃* M is an isomorphism of comm_monoids such that k(T) = S, f ∘ k is a localization map for T.

Equations

f.of_mul_equiv_of_dom H = let H' : submonoid.comap k.to_monoid_hom S = T := _ in (f.to_map.comp k.to_monoid_hom).to_localization_map _ _ _

source

@[simp]

theorem add_submonoid.localization_map.of_add_equiv_of_dom_apply {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {T : add_submonoid P} {k : P ≃+ M} (H : add_submonoid.map k.to_add_monoid_hom T = S) (x : P) :

⇑((f.of_add_equiv_of_dom H).to_map) x = ⇑(f.to_map) (⇑k x)

source

@[simp]

theorem submonoid.localization_map.of_mul_equiv_of_dom_apply {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {T : submonoid P} {k : P ≃* M} (H : submonoid.map k.to_monoid_hom T = S) (x : P) :

⇑((f.of_mul_equiv_of_dom H).to_map) x = ⇑(f.to_map) (⇑k x)

source

theorem submonoid.localization_map.of_mul_equiv_of_dom_eq {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {T : submonoid P} {k : P ≃* M} (H : submonoid.map k.to_monoid_hom T = S) :

(f.of_mul_equiv_of_dom H).to_map = f.to_map.comp k.to_monoid_hom

source

theorem add_submonoid.localization_map.of_add_equiv_of_dom_eq {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {T : add_submonoid P} {k : P ≃+ M} (H : add_submonoid.map k.to_add_monoid_hom T = S) :

(f.of_add_equiv_of_dom H).to_map = f.to_map.comp k.to_add_monoid_hom

source

theorem add_submonoid.localization_map.of_add_equiv_of_dom_comp_symm {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {T : add_submonoid P} {k : P ≃+ M} (H : add_submonoid.map k.to_add_monoid_hom T = S) (x : M) :

⇑((f.of_add_equiv_of_dom H).to_map) (⇑(k.symm) x) = ⇑(f.to_map) x

source

theorem submonoid.localization_map.of_mul_equiv_of_dom_comp_symm {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {T : submonoid P} {k : P ≃* M} (H : submonoid.map k.to_monoid_hom T = S) (x : M) :

⇑((f.of_mul_equiv_of_dom H).to_map) (⇑(k.symm) x) = ⇑(f.to_map) x

source

theorem add_submonoid.localization_map.of_add_equiv_of_dom_comp {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {T : add_submonoid P} {k : M ≃+ P} (H : add_submonoid.map k.symm.to_add_monoid_hom T = S) (x : M) :

⇑((f.of_add_equiv_of_dom H).to_map) (⇑k x) = ⇑(f.to_map) x

source

theorem submonoid.localization_map.of_mul_equiv_of_dom_comp {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {T : submonoid P} {k : M ≃* P} (H : submonoid.map k.symm.to_monoid_hom T = S) (x : M) :

⇑((f.of_mul_equiv_of_dom H).to_map) (⇑k x) = ⇑(f.to_map) x

source

@[simp]

theorem submonoid.localization_map.of_mul_equiv_of_dom_id {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) :

f.of_mul_equiv_of_dom _ = f

A special case of f ∘ id = f, f a localization map.

source

@[simp]

theorem add_submonoid.localization_map.of_add_equiv_of_dom_id {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) :

f.of_add_equiv_of_dom _ = f

A special case of f ∘ id = f, f a localization map.

source

noncomputable def submonoid.localization_map.mul_equiv_of_mul_equiv {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {T : submonoid P} {Q : Type u_4} [comm_monoid Q] (k : T.localization_map Q) {j : M ≃* P} (H : submonoid.map j.to_monoid_hom S = T) :

N ≃* Q

Given localization maps f : M →* N, k : P →* U for submonoids S, T respectively, an isomorphism j : M ≃* P such that j(S) = T induces an isomorphism of localizations N ≃* U.

Equations

f.mul_equiv_of_mul_equiv k H = f.mul_equiv_of_localizations (k.of_mul_equiv_of_dom H)

source

noncomputable def add_submonoid.localization_map.add_equiv_of_add_equiv {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {T : add_submonoid P} {Q : Type u_4} [add_comm_monoid Q] (k : T.localization_map Q) {j : M ≃+ P} (H : add_submonoid.map j.to_add_monoid_hom S = T) :

N ≃+ Q

Given localization maps f : M →+ N, k : P →+ U for submonoids S, T respectively, an isomorphism j : M ≃+ P such that j(S) = T induces an isomorphism of localizations N ≃+ U.

Equations

f.add_equiv_of_add_equiv k H = f.add_equiv_of_localizations (k.of_add_equiv_of_dom H)

source

@[simp]

theorem add_submonoid.localization_map.add_equiv_of_add_equiv_eq_map_apply {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {T : add_submonoid P} {Q : Type u_4} [add_comm_monoid Q] {k : T.localization_map Q} {j : M ≃+ P} (H : add_submonoid.map j.to_add_monoid_hom S = T) (x : N) :

⇑(f.add_equiv_of_add_equiv k H) x = ⇑(f.map _ k) x

source

@[simp]

theorem submonoid.localization_map.mul_equiv_of_mul_equiv_eq_map_apply {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {T : submonoid P} {Q : Type u_4} [comm_monoid Q] {k : T.localization_map Q} {j : M ≃* P} (H : submonoid.map j.to_monoid_hom S = T) (x : N) :

⇑(f.mul_equiv_of_mul_equiv k H) x = ⇑(f.map _ k) x

source

theorem add_submonoid.localization_map.add_equiv_of_add_equiv_eq_map {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {T : add_submonoid P} {Q : Type u_4} [add_comm_monoid Q] {k : T.localization_map Q} {j : M ≃+ P} (H : add_submonoid.map j.to_add_monoid_hom S = T) :

(f.add_equiv_of_add_equiv k H).to_add_monoid_hom = f.map _ k

source

theorem submonoid.localization_map.mul_equiv_of_mul_equiv_eq_map {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {T : submonoid P} {Q : Type u_4} [comm_monoid Q] {k : T.localization_map Q} {j : M ≃* P} (H : submonoid.map j.to_monoid_hom S = T) :

(f.mul_equiv_of_mul_equiv k H).to_monoid_hom = f.map _ k

source

@[simp]

theorem add_submonoid.localization_map.add_equiv_of_add_equiv_eq {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {T : add_submonoid P} {Q : Type u_4} [add_comm_monoid Q] {k : T.localization_map Q} {j : M ≃+ P} (H : add_submonoid.map j.to_add_monoid_hom S = T) (x : M) :

⇑(f.add_equiv_of_add_equiv k H) (⇑(f.to_map) x) = ⇑(k.to_map) (⇑j x)

source

@[simp]

theorem submonoid.localization_map.mul_equiv_of_mul_equiv_eq {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {T : submonoid P} {Q : Type u_4} [comm_monoid Q] {k : T.localization_map Q} {j : M ≃* P} (H : submonoid.map j.to_monoid_hom S = T) (x : M) :

⇑(f.mul_equiv_of_mul_equiv k H) (⇑(f.to_map) x) = ⇑(k.to_map) (⇑j x)

source

@[simp]

theorem add_submonoid.localization_map.add_equiv_of_add_equiv_mk' {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {T : add_submonoid P} {Q : Type u_4} [add_comm_monoid Q] {k : T.localization_map Q} {j : M ≃+ P} (H : add_submonoid.map j.to_add_monoid_hom S = T) (x : M) (y : ↥S) :

⇑(f.add_equiv_of_add_equiv k H) (f.mk' x y) = k.mk' (⇑j x) ⟨⇑j ↑y, _⟩

source

@[simp]

theorem submonoid.localization_map.mul_equiv_of_mul_equiv_mk' {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {T : submonoid P} {Q : Type u_4} [comm_monoid Q] {k : T.localization_map Q} {j : M ≃* P} (H : submonoid.map j.to_monoid_hom S = T) (x : M) (y : ↥S) :

⇑(f.mul_equiv_of_mul_equiv k H) (f.mk' x y) = k.mk' (⇑j x) ⟨⇑j ↑y, _⟩

source

@[simp]

theorem add_submonoid.localization_map.of_add_equiv_of_add_equiv_apply {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {T : add_submonoid P} {Q : Type u_4} [add_comm_monoid Q] {k : T.localization_map Q} {j : M ≃+ P} (H : add_submonoid.map j.to_add_monoid_hom S = T) (x : M) :

⇑((f.of_add_equiv_of_localizations (f.add_equiv_of_add_equiv k H)).to_map) x = ⇑(k.to_map) (⇑j x)

source

@[simp]

theorem submonoid.localization_map.of_mul_equiv_of_mul_equiv_apply {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {T : submonoid P} {Q : Type u_4} [comm_monoid Q] {k : T.localization_map Q} {j : M ≃* P} (H : submonoid.map j.to_monoid_hom S = T) (x : M) :

⇑((f.of_mul_equiv_of_localizations (f.mul_equiv_of_mul_equiv k H)).to_map) x = ⇑(k.to_map) (⇑j x)

source

theorem submonoid.localization_map.of_mul_equiv_of_mul_equiv {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {P : Type u_3} [comm_monoid P] (f : S.localization_map N) {T : submonoid P} {Q : Type u_4} [comm_monoid Q] {k : T.localization_map Q} {j : M ≃* P} (H : submonoid.map j.to_monoid_hom S = T) :

(f.of_mul_equiv_of_localizations (f.mul_equiv_of_mul_equiv k H)).to_map = k.to_map.comp j.to_monoid_hom

source

theorem add_submonoid.localization_map.of_add_equiv_of_add_equiv {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {P : Type u_3} [add_comm_monoid P] (f : S.localization_map N) {T : add_submonoid P} {Q : Type u_4} [add_comm_monoid Q] {k : T.localization_map Q} {j : M ≃+ P} (H : add_submonoid.map j.to_add_monoid_hom S = T) :

(f.of_add_equiv_of_localizations (f.add_equiv_of_add_equiv k H)).to_map = k.to_map.comp j.to_add_monoid_hom

source

def localization.monoid_of {M : Type u_1} [comm_monoid M] (S : submonoid M) :

S.localization_map (localization S)

Natural hom sending x : M, M a comm_monoid, to the equivalence class of (x, 1) in the localization of M at a submonoid.

Equations

localization.monoid_of S = {to_monoid_hom := {to_fun := λ (x : M), localization.mk x 1, map_one' := _, map_mul' := _}, map_units' := _, surj' := _, eq_iff_exists' := _}

source

def add_localization.add_monoid_of {M : Type u_1} [add_comm_monoid M] (S : add_submonoid M) :

S.localization_map (add_localization S)

Natural homomorphism sending x : M, M an add_comm_monoid, to the equivalence class of (x, 0) in the localization of M at a submonoid.

Equations

add_localization.add_monoid_of S = {to_add_monoid_hom := {to_fun := λ (x : M), add_localization.mk x 0, map_zero' := _, map_add' := _}, map_add_units' := _, surj' := _, eq_iff_exists' := _}

source

theorem add_localization.mk_zero_eq_add_monoid_of_mk {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} (x : M) :

add_localization.mk x 0 = ⇑((add_localization.add_monoid_of S).to_map) x

source

theorem localization.mk_one_eq_monoid_of_mk {M : Type u_1} [comm_monoid M] {S : submonoid M} (x : M) :

localization.mk x 1 = ⇑((localization.monoid_of S).to_map) x

source

theorem localization.mk_eq_monoid_of_mk'_apply {M : Type u_1} [comm_monoid M] {S : submonoid M} (x : M) (y : ↥S) :

localization.mk x y = (localization.monoid_of S).mk' x y

source

theorem add_localization.mk_eq_add_monoid_of_mk'_apply {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} (x : M) (y : ↥S) :

add_localization.mk x y = (add_localization.add_monoid_of S).mk' x y

source

@[simp]

theorem localization.mk_eq_monoid_of_mk' {M : Type u_1} [comm_monoid M] {S : submonoid M} :

localization.mk = (localization.monoid_of S).mk'

source

@[simp]

theorem add_localization.mk_eq_add_monoid_of_mk' {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} :

add_localization.mk = (add_localization.add_monoid_of S).mk'

source

@[simp]

theorem localization.lift_on_mk' {M : Type u_1} [comm_monoid M] {S : submonoid M} {p : Sort u} (f : M → ↥S → p) (H : ∀ {a c : M} {b d : ↥S}, ⇑(localization.r S) (a, b) (c, d) → f a b = f c d) (a : M) (b : ↥S) :

((localization.monoid_of S).mk' a b).lift_on f H = f a b

source

@[simp]

theorem add_localization.lift_on_mk' {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {p : Sort u} (f : M → ↥S → p) (H : ∀ {a c : M} {b d : ↥S}, ⇑(add_localization.r S) (a, b) (c, d) → f a b = f c d) (a : M) (b : ↥S) :

((add_localization.add_monoid_of S).mk' a b).lift_on f H = f a b

source

@[simp]

theorem localization.lift_on₂_mk' {M : Type u_1} [comm_monoid M] {S : submonoid M} {p : Sort u_2} (f : M → ↥S → M → ↥S → p) (H : ∀ {a a' : M} {b b' : ↥S} {c c' : M} {d d' : ↥S}, ⇑(localization.r S) (a, b) (a', b') → ⇑(localization.r S) (c, d) (c', d') → f a b c d = f a' b' c' d') (a c : M) (b d : ↥S) :

((localization.monoid_of S).mk' a b).lift_on₂ ((localization.monoid_of S).mk' c d) f H = f a b c d

source

@[simp]

theorem add_localization.lift_on₂_mk' {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {p : Sort u_2} (f : M → ↥S → M → ↥S → p) (H : ∀ {a a' : M} {b b' : ↥S} {c c' : M} {d d' : ↥S}, ⇑(add_localization.r S) (a, b) (a', b') → ⇑(add_localization.r S) (c, d) (c', d') → f a b c d = f a' b' c' d') (a c : M) (b d : ↥S) :

((add_localization.add_monoid_of S).mk' a b).lift_on₂ ((add_localization.add_monoid_of S).mk' c d) f H = f a b c d

source

noncomputable def add_localization.add_equiv_of_quotient {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] (f : S.localization_map N) :

add_localization S ≃+ N

Given a localization map f : M →+ N for a submonoid S, we get an isomorphism between the localization of M at S as a quotient type and N.

Equations

add_localization.add_equiv_of_quotient f = (add_localization.add_monoid_of S).add_equiv_of_localizations f

source

noncomputable def localization.mul_equiv_of_quotient {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] (f : S.localization_map N) :

localization S ≃* N

Given a localization map f : M →* N for a submonoid S, we get an isomorphism between the localization of M at S as a quotient type and N.

Equations

localization.mul_equiv_of_quotient f = (localization.monoid_of S).mul_equiv_of_localizations f

source

@[simp]

theorem localization.mul_equiv_of_quotient_apply {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {f : S.localization_map N} (x : localization S) :

⇑(localization.mul_equiv_of_quotient f) x = ⇑((localization.monoid_of S).lift _) x

source

@[simp]

theorem add_localization.add_equiv_of_quotient_apply {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {f : S.localization_map N} (x : add_localization S) :

⇑(add_localization.add_equiv_of_quotient f) x = ⇑((add_localization.add_monoid_of S).lift _) x

source

@[simp]

theorem add_localization.add_equiv_of_quotient_mk' {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {f : S.localization_map N} (x : M) (y : ↥S) :

⇑(add_localization.add_equiv_of_quotient f) ((add_localization.add_monoid_of S).mk' x y) = f.mk' x y

source

@[simp]

theorem localization.mul_equiv_of_quotient_mk' {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {f : S.localization_map N} (x : M) (y : ↥S) :

⇑(localization.mul_equiv_of_quotient f) ((localization.monoid_of S).mk' x y) = f.mk' x y

source

theorem add_localization.add_equiv_of_quotient_mk {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {f : S.localization_map N} (x : M) (y : ↥S) :

⇑(add_localization.add_equiv_of_quotient f) (add_localization.mk x y) = f.mk' x y

source

theorem localization.mul_equiv_of_quotient_mk {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {f : S.localization_map N} (x : M) (y : ↥S) :

⇑(localization.mul_equiv_of_quotient f) (localization.mk x y) = f.mk' x y

source

@[simp]

theorem add_localization.add_equiv_of_quotient_add_monoid_of {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {f : S.localization_map N} (x : M) :

⇑(add_localization.add_equiv_of_quotient f) (⇑((add_localization.add_monoid_of S).to_map) x) = ⇑(f.to_map) x

source

@[simp]

theorem localization.mul_equiv_of_quotient_monoid_of {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {f : S.localization_map N} (x : M) :

⇑(localization.mul_equiv_of_quotient f) (⇑((localization.monoid_of S).to_map) x) = ⇑(f.to_map) x

source

@[simp]

theorem add_localization.add_equiv_of_quotient_symm_mk' {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {f : S.localization_map N} (x : M) (y : ↥S) :

⇑((add_localization.add_equiv_of_quotient f).symm) (f.mk' x y) = (add_localization.add_monoid_of S).mk' x y

source

@[simp]

theorem localization.mul_equiv_of_quotient_symm_mk' {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {f : S.localization_map N} (x : M) (y : ↥S) :

⇑((localization.mul_equiv_of_quotient f).symm) (f.mk' x y) = (localization.monoid_of S).mk' x y

source

theorem localization.mul_equiv_of_quotient_symm_mk {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {f : S.localization_map N} (x : M) (y : ↥S) :

⇑((localization.mul_equiv_of_quotient f).symm) (f.mk' x y) = localization.mk x y

source

theorem add_localization.add_equiv_of_quotient_symm_mk {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {f : S.localization_map N} (x : M) (y : ↥S) :

⇑((add_localization.add_equiv_of_quotient f).symm) (f.mk' x y) = add_localization.mk x y

source

@[simp]

theorem localization.mul_equiv_of_quotient_symm_monoid_of {M : Type u_1} [comm_monoid M] {S : submonoid M} {N : Type u_2} [comm_monoid N] {f : S.localization_map N} (x : M) :

⇑((localization.mul_equiv_of_quotient f).symm) (⇑(f.to_map) x) = ⇑((localization.monoid_of S).to_map) x

source

@[simp]

theorem add_localization.add_equiv_of_quotient_symm_add_monoid_of {M : Type u_1} [add_comm_monoid M] {S : add_submonoid M} {N : Type u_2} [add_comm_monoid N] {f : S.localization_map N} (x : M) :

⇑((add_localization.add_equiv_of_quotient f).symm) (⇑(f.to_map) x) = ⇑((add_localization.add_monoid_of S).to_map) x

source

@[reducible]

def add_localization.away {M : Type u_1} [add_comm_monoid M] (x : M) :

Type u_1

Given x : M, the localization of M at the submonoid generated by x, as a quotient.

Equations

add_localization.away x = add_localization (add_submonoid.multiples x)

source

@[reducible]

def localization.away {M : Type u_1} [comm_monoid M] (x : M) :

Type u_1

Given x : M, the localization of M at the submonoid generated by x, as a quotient.

Equations

localization.away x = localization (submonoid.powers x)

source

def localization.away.inv_self {M : Type u_1} [comm_monoid M] (x : M) :

localization.away x

Given x : M, inv_self is x⁻¹ in the localization (as a quotient type) of M at the submonoid generated by x.

Equations

localization.away.inv_self x = localization.mk 1 ⟨x, _⟩

source

def add_localization.away.neg_self {M : Type u_1} [add_comm_monoid M] (x : M) :

add_localization.away x

Given x : M, neg_self is -x in the localization (as a quotient type) of M at the submonoid generated by x.

Equations

add_localization.away.neg_self x = add_localization.mk 0 ⟨x, _⟩

source

@[reducible]

def localization.away.monoid_of {M : Type u_1} [comm_monoid M] (x : M) :

submonoid.localization_map.away_map x (localization.away x)

Given x : M, the natural hom sending y : M, M a comm_monoid, to the equivalence class of (y, 1) in the localization of M at the submonoid generated by x.

Equations

localization.away.monoid_of x = localization.monoid_of (submonoid.powers x)

source

@[reducible]

def add_localization.away.add_monoid_of {M : Type u_1} [add_comm_monoid M] (x : M) :

add_submonoid.localization_map.away_map x (add_localization.away x)

Given x : M, the natural hom sending y : M, M an add_comm_monoid, to the equivalence class of (y, 0) in the localization of M at the submonoid generated by x.

Equations

add_localization.away.add_monoid_of x = add_localization.add_monoid_of (add_submonoid.multiples x)

source

@[simp]

theorem add_localization.away.mk_eq_add_monoid_of_mk' {M : Type u_1} [add_comm_monoid M] (x : M) :

add_localization.mk = add_submonoid.localization_map.mk' (add_localization.away.add_monoid_of x)

source

@[simp]

theorem localization.away.mk_eq_monoid_of_mk' {M : Type u_1} [comm_monoid M] (x : M) :

localization.mk = submonoid.localization_map.mk' (localization.away.monoid_of x)

source

noncomputable def localization.away.mul_equiv_of_quotient {M : Type u_1} [comm_monoid M] {N : Type u_2} [comm_monoid N] (x : M) (f : submonoid.localization_map.away_map x N) :

localization.away x ≃* N

Given x : M and a localization map f : M →* N away from x, we get an isomorphism between the localization of M at the submonoid generated by x as a quotient type and N.

Equations

localization.away.mul_equiv_of_quotient x f = localization.mul_equiv_of_quotient f

source

noncomputable def add_localization.away.add_equiv_of_quotient {M : Type u_1} [add_comm_monoid M] {N : Type u_2} [add_comm_monoid N] (x : M) (f : add_submonoid.localization_map.away_map x N) :

add_localization.away x ≃+ N

Given x : M and a localization map f : M →+ N away from x, we get an isomorphism between the localization of M at the submonoid generated by x as a quotient type and N.

Equations

add_localization.away.add_equiv_of_quotient x f = add_localization.add_equiv_of_quotient f

source

@[nolint]

structure submonoid.localization_with_zero_map {M : Type u_1} [comm_monoid_with_zero M] (S : submonoid M) (N : Type u_2) [comm_monoid_with_zero N] :

Type (max u_1 u_2)

to_localization_map : S.localization_map N
map_zero' : self.to_localization_map.to_monoid_hom.to_fun 0 = 0

The type of homomorphisms between monoids with zero satisfying the characteristic predicate: if f : M →*₀ N satisfies this predicate, then N is isomorphic to the localization of M at S.

Instances for submonoid.localization_with_zero_map

submonoid.localization_with_zero_map.has_sizeof_inst

source

def submonoid.localization_with_zero_map.to_monoid_with_zero_hom {M : Type u_1} [comm_monoid_with_zero M] {S : submonoid M} {N : Type u_2} [comm_monoid_with_zero N] (f : S.localization_with_zero_map N) :

M →*₀ N

The monoid with zero hom underlying a localization_map.

Equations

f.to_monoid_with_zero_hom = {to_fun := f.to_localization_map.to_monoid_hom.to_fun, map_zero' := _, map_one' := _, map_mul' := _}

source

@[protected, irreducible]

def localization.zero {M : Type u_1} [comm_monoid_with_zero M] (S : submonoid M) :

localization S

The zero element in a localization is defined as (0, 1).

Should not be confused with add_localization.zero which is (0, 0).

Equations

localization.zero S = localization.mk 0 1

source

@[protected, instance]

def localization.has_zero {M : Type u_1} [comm_monoid_with_zero M] (S : submonoid M) :

has_zero (localization S)

Equations

localization.has_zero S = {zero := localization.zero S}

source

@[protected, instance]

def localization.comm_monoid_with_zero {M : Type u_1} [comm_monoid_with_zero M] (S : submonoid M) :

comm_monoid_with_zero (localization S)

Equations

localization.comm_monoid_with_zero S = {mul := comm_monoid.mul (localization.comm_monoid S), mul_assoc := _, one := comm_monoid.one (localization.comm_monoid S), one_mul := _, mul_one := _, npow := comm_monoid.npow (localization.comm_monoid S), npow_zero' := _, npow_succ' := _, mul_comm := _, zero := 0, zero_mul := _, mul_zero := _}

source

theorem localization.mk_zero {M : Type u_1} [comm_monoid_with_zero M] {S : submonoid M} (x : ↥S) :

localization.mk 0 x = 0

source

theorem localization.lift_on_zero {M : Type u_1} [comm_monoid_with_zero M] {S : submonoid M} {p : Type u_2} (f : M → ↥S → p) (H : ∀ {a c : M} {b d : ↥S}, ⇑(localization.r S) (a, b) (c, d) → f a b = f c d) :

0.lift_on f H = f 0 1

source

@[simp]

theorem submonoid.localization_map.sec_zero_fst {M : Type u_1} [comm_monoid_with_zero M] {S : submonoid M} {N : Type u_2} [comm_monoid_with_zero N] {f : S.localization_map N} :

⇑(f.to_map) (f.sec 0).fst = 0

source

noncomputable def submonoid.localization_with_zero_map.lift {M : Type u_1} [comm_monoid_with_zero M] {S : submonoid M} {N : Type u_2} [comm_monoid_with_zero N] {P : Type u_3} [comm_monoid_with_zero P] (f : S.localization_with_zero_map N) (g : M →*₀ P) (hg : ∀ (y : ↥S), is_unit (⇑g ↑y)) :

N →*₀ P

Given a localization map f : M →*₀ N for a submonoid S ⊆ M and a map of comm_monoid_with_zeros g : M →*₀ P such that g y is invertible for all y : S, the homomorphism induced from N to P sending z : N to g x * (g y)⁻¹, where (x, y) : M × S are such that z = f x * (f y)⁻¹.

Equations

f.lift g hg = {to_fun := (f.to_localization_map.lift hg).to_fun, map_zero' := _, map_one' := _, map_mul' := _}

source

theorem localization.mk_left_injective {α : Type u_1} [cancel_comm_monoid α] {s : submonoid α} (b : ↥s) :

function.injective (λ (a : α), localization.mk a b)

source

theorem add_localization.mk_left_injective {α : Type u_1} [add_cancel_comm_monoid α] {s : add_submonoid α} (b : ↥s) :

function.injective (λ (a : α), add_localization.mk a b)

source

theorem localization.mk_eq_mk_iff' {α : Type u_1} [cancel_comm_monoid α] {s : submonoid α} {a₁ b₁ : α} {a₂ b₂ : ↥s} :

localization.mk a₁ a₂ = localization.mk b₁ b₂ ↔ ↑b₂ * a₁ = ↑a₂ * b₁

source

theorem add_localization.mk_eq_mk_iff' {α : Type u_1} [add_cancel_comm_monoid α] {s : add_submonoid α} {a₁ b₁ : α} {a₂ b₂ : ↥s} :

add_localization.mk a₁ a₂ = add_localization.mk b₁ b₂ ↔ ↑b₂ + a₁ = ↑a₂ + b₁

source

@[protected, instance]

def localization.decidable_eq {α : Type u_1} [cancel_comm_monoid α] {s : submonoid α} [decidable_eq α] :

decidable_eq (localization s)

Equations

localization.decidable_eq = λ (a b : localization s), a.rec_on_subsingleton₂ b (λ (a₁ a₂ : α) (b₁ b₂ : ↥s), decidable_of_iff' (↑b₂ * a₁ = ↑b₁ * a₂) localization.mk_eq_mk_iff')

source

@[protected, instance]

def add_localization.decidable_eq {α : Type u_1} [add_cancel_comm_monoid α] {s : add_submonoid α} [decidable_eq α] :

decidable_eq (add_localization s)

Equations

add_localization.decidable_eq = λ (a b : add_localization s), a.rec_on_subsingleton₂ b (λ (a₁ a₂ : α) (b₁ b₂ : ↥s), decidable_of_iff' (↑b₂ + a₁ = ↑b₁ + a₂) add_localization.mk_eq_mk_iff')

source

@[protected, instance]

def localization.has_le {α : Type u_1} [ordered_cancel_comm_monoid α] {s : submonoid α} :

has_le (localization s)

Equations

localization.has_le = {le := λ (a b : localization s), a.lift_on₂ b (λ (a₁ : α) (a₂ : ↥s) (b₁ : α) (b₂ : ↥s), ↑b₂ * a₁ ≤ ↑a₂ * b₁) localization.has_le._proof_1}

source

@[protected, instance]

def add_localization.has_le {α : Type u_1} [ordered_cancel_add_comm_monoid α] {s : add_submonoid α} :

has_le (add_localization s)

Equations

add_localization.has_le = {le := λ (a b : add_localization s), a.lift_on₂ b (λ (a₁ : α) (a₂ : ↥s) (b₁ : α) (b₂ : ↥s), ↑b₂ + a₁ ≤ ↑a₂ + b₁) add_localization.has_le._proof_1}

source

@[protected, instance]

def add_localization.has_lt {α : Type u_1} [ordered_cancel_add_comm_monoid α] {s : add_submonoid α} :

has_lt (add_localization s)

Equations

add_localization.has_lt = {lt := λ (a b : add_localization s), a.lift_on₂ b (λ (a₁ : α) (a₂ : ↥s) (b₁ : α) (b₂ : ↥s), ↑b₂ + a₁ < ↑a₂ + b₁) add_localization.has_lt._proof_1}

source

@[protected, instance]

def localization.has_lt {α : Type u_1} [ordered_cancel_comm_monoid α] {s : submonoid α} :

has_lt (localization s)

Equations

localization.has_lt = {lt := λ (a b : localization s), a.lift_on₂ b (λ (a₁ : α) (a₂ : ↥s) (b₁ : α) (b₂ : ↥s), ↑b₂ * a₁ < ↑a₂ * b₁) localization.has_lt._proof_1}

source

theorem localization.mk_le_mk {α : Type u_1} [ordered_cancel_comm_monoid α] {s : submonoid α} {a₁ b₁ : α} {a₂ b₂ : ↥s} :

localization.mk a₁ a₂ ≤ localization.mk b₁ b₂ ↔ ↑b₂ * a₁ ≤ ↑a₂ * b₁

source

theorem add_localization.mk_le_mk {α : Type u_1} [ordered_cancel_add_comm_monoid α] {s : add_submonoid α} {a₁ b₁ : α} {a₂ b₂ : ↥s} :

add_localization.mk a₁ a₂ ≤ add_localization.mk b₁ b₂ ↔ ↑b₂ + a₁ ≤ ↑a₂ + b₁

source

theorem add_localization.mk_lt_mk {α : Type u_1} [ordered_cancel_add_comm_monoid α] {s : add_submonoid α} {a₁ b₁ : α} {a₂ b₂ : ↥s} :

add_localization.mk a₁ a₂ < add_localization.mk b₁ b₂ ↔ ↑b₂ + a₁ < ↑a₂ + b₁

source

theorem localization.mk_lt_mk {α : Type u_1} [ordered_cancel_comm_monoid α] {s : submonoid α} {a₁ b₁ : α} {a₂ b₂ : ↥s} :

localization.mk a₁ a₂ < localization.mk b₁ b₂ ↔ ↑b₂ * a₁ < ↑a₂ * b₁

source

@[protected, instance]

def add_localization.partial_order {α : Type u_1} [ordered_cancel_add_comm_monoid α] {s : add_submonoid α} :

partial_order (add_localization s)

Equations

add_localization.partial_order = {le := has_le.le add_localization.has_le, lt := has_lt.lt add_localization.has_lt, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

source

@[protected, instance]

def localization.partial_order {α : Type u_1} [ordered_cancel_comm_monoid α] {s : submonoid α} :

partial_order (localization s)

Equations

localization.partial_order = {le := has_le.le localization.has_le, lt := has_lt.lt localization.has_lt, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}

source

@[protected, instance]

def localization.ordered_cancel_comm_monoid {α : Type u_1} [ordered_cancel_comm_monoid α] {s : submonoid α} :

ordered_cancel_comm_monoid (localization s)

Equations

localization.ordered_cancel_comm_monoid = {mul := comm_monoid.mul (localization.comm_monoid s), mul_assoc := _, one := comm_monoid.one (localization.comm_monoid s), one_mul := _, mul_one := _, npow := comm_monoid.npow (localization.comm_monoid s), npow_zero' := _, npow_succ' := _, mul_comm := _, le := partial_order.le localization.partial_order, lt := partial_order.lt localization.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, le_of_mul_le_mul_left := _}

source

@[protected, instance]

def add_localization.ordered_cancel_add_comm_monoid {α : Type u_1} [ordered_cancel_add_comm_monoid α] {s : add_submonoid α} :

ordered_cancel_add_comm_monoid (add_localization s)

Equations

add_localization.ordered_cancel_add_comm_monoid = {add := add_comm_monoid.add (add_localization.add_comm_monoid s), add_assoc := _, zero := add_comm_monoid.zero (add_localization.add_comm_monoid s), zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul (add_localization.add_comm_monoid s), nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := partial_order.le add_localization.partial_order, lt := partial_order.lt add_localization.partial_order, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _}

source

@[protected, instance]

def add_localization.decidable_le {α : Type u_1} [ordered_cancel_add_comm_monoid α] {s : add_submonoid α} [decidable_rel has_le.le] :

decidable_rel has_le.le

Equations

add_localization.decidable_le = λ (a b : add_localization s), a.rec_on_subsingleton₂ b (λ (a₁ a₂ : α) (b₁ b₂ : ↥s), decidable_of_iff' (↑b₂ + a₁ ≤ ↑b₁ + a₂) add_localization.mk_le_mk)

source

@[protected, instance]

def localization.decidable_le {α : Type u_1} [ordered_cancel_comm_monoid α] {s : submonoid α} [decidable_rel has_le.le] :

decidable_rel has_le.le

Equations

localization.decidable_le = λ (a b : localization s), a.rec_on_subsingleton₂ b (λ (a₁ a₂ : α) (b₁ b₂ : ↥s), decidable_of_iff' (↑b₂ * a₁ ≤ ↑b₁ * a₂) localization.mk_le_mk)

source

@[protected, instance]

def add_localization.decidable_lt {α : Type u_1} [ordered_cancel_add_comm_monoid α] {s : add_submonoid α} [decidable_rel has_lt.lt] :

decidable_rel has_lt.lt

Equations

add_localization.decidable_lt = λ (a b : add_localization s), a.rec_on_subsingleton₂ b (λ (a₁ a₂ : α) (b₁ b₂ : ↥s), decidable_of_iff' (↑b₂ + a₁ < ↑b₁ + a₂) add_localization.mk_lt_mk)

source

@[protected, instance]

def localization.decidable_lt {α : Type u_1} [ordered_cancel_comm_monoid α] {s : submonoid α} [decidable_rel has_lt.lt] :

decidable_rel has_lt.lt

Equations

localization.decidable_lt = λ (a b : localization s), a.rec_on_subsingleton₂ b (λ (a₁ a₂ : α) (b₁ b₂ : ↥s), decidable_of_iff' (↑b₂ * a₁ < ↑b₁ * a₂) localization.mk_lt_mk)

source

def localization.mk_order_embedding {α : Type u_1} [ordered_cancel_comm_monoid α] {s : submonoid α} (b : ↥s) :

α ↪o localization s

An ordered cancellative monoid injects into its localization by sending a to a / b.

Equations

localization.mk_order_embedding b = {to_embedding := {to_fun := λ (a : α), localization.mk a b, inj' := _}, map_rel_iff' := _}

source

def add_localization.mk_order_embedding {α : Type u_1} [ordered_cancel_add_comm_monoid α] {s : add_submonoid α} (b : ↥s) :

α ↪o add_localization s

An ordered cancellative monoid injects into its localization by sending a to a - b.

Equations

add_localization.mk_order_embedding b = {to_embedding := {to_fun := λ (a : α), add_localization.mk a b, inj' := _}, map_rel_iff' := _}

source

@[simp]

theorem add_localization.mk_order_embedding_apply {α : Type u_1} [ordered_cancel_add_comm_monoid α] {s : add_submonoid α} (b : ↥s) (a : α) :

⇑(add_localization.mk_order_embedding b) a = add_localization.mk a b

source

@[simp]

theorem localization.mk_order_embedding_apply {α : Type u_1} [ordered_cancel_comm_monoid α] {s : submonoid α} (b : ↥s) (a : α) :

⇑(localization.mk_order_embedding b) a = localization.mk a b

source

@[protected, instance]

def add_localization.linear_ordered_cancel_add_comm_monoid {α : Type u_1} [linear_ordered_cancel_add_comm_monoid α] {s : add_submonoid α} :

linear_ordered_cancel_add_comm_monoid (add_localization s)

Equations

add_localization.linear_ordered_cancel_add_comm_monoid = {add := ordered_cancel_add_comm_monoid.add add_localization.ordered_cancel_add_comm_monoid, add_assoc := _, zero := ordered_cancel_add_comm_monoid.zero add_localization.ordered_cancel_add_comm_monoid, zero_add := _, add_zero := _, nsmul := ordered_cancel_add_comm_monoid.nsmul add_localization.ordered_cancel_add_comm_monoid, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, le := ordered_cancel_add_comm_monoid.le add_localization.ordered_cancel_add_comm_monoid, lt := ordered_cancel_add_comm_monoid.lt add_localization.ordered_cancel_add_comm_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, add_le_add_left := _, le_of_add_le_add_left := _, le_total := _, decidable_le := add_localization.decidable_le has_le.le.decidable, decidable_eq := linear_ordered_add_comm_monoid.decidable_eq._default ordered_cancel_add_comm_monoid.le ordered_cancel_add_comm_monoid.lt add_localization.linear_ordered_cancel_add_comm_monoid._proof_14 add_localization.linear_ordered_cancel_add_comm_monoid._proof_15 add_localization.linear_ordered_cancel_add_comm_monoid._proof_16 add_localization.linear_ordered_cancel_add_comm_monoid._proof_17 add_localization.decidable_le, decidable_lt := add_localization.decidable_lt has_lt.lt.decidable, max := linear_ordered_add_comm_monoid.max._default ordered_cancel_add_comm_monoid.le ordered_cancel_add_comm_monoid.lt add_localization.linear_ordered_cancel_add_comm_monoid._proof_18 add_localization.linear_ordered_cancel_add_comm_monoid._proof_19 add_localization.linear_ordered_cancel_add_comm_monoid._proof_20 add_localization.linear_ordered_cancel_add_comm_monoid._proof_21 add_localization.decidable_le, max_def := _, min := linear_ordered_add_comm_monoid.min._default ordered_cancel_add_comm_monoid.le ordered_cancel_add_comm_monoid.lt add_localization.linear_ordered_cancel_add_comm_monoid._proof_23 add_localization.linear_ordered_cancel_add_comm_monoid._proof_24 add_localization.linear_ordered_cancel_add_comm_monoid._proof_25 add_localization.linear_ordered_cancel_add_comm_monoid._proof_26 add_localization.decidable_le, min_def := _}

source

@[protected, instance]

def localization.linear_ordered_cancel_comm_monoid {α : Type u_1} [linear_ordered_cancel_comm_monoid α] {s : submonoid α} :

linear_ordered_cancel_comm_monoid (localization s)

Equations

localization.linear_ordered_cancel_comm_monoid = {mul := ordered_cancel_comm_monoid.mul localization.ordered_cancel_comm_monoid, mul_assoc := _, one := ordered_cancel_comm_monoid.one localization.ordered_cancel_comm_monoid, one_mul := _, mul_one := _, npow := ordered_cancel_comm_monoid.npow localization.ordered_cancel_comm_monoid, npow_zero' := _, npow_succ' := _, mul_comm := _, le := ordered_cancel_comm_monoid.le localization.ordered_cancel_comm_monoid, lt := ordered_cancel_comm_monoid.lt localization.ordered_cancel_comm_monoid, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, mul_le_mul_left := _, le_of_mul_le_mul_left := _, le_total := _, decidable_le := localization.decidable_le has_le.le.decidable, decidable_eq := linear_ordered_comm_monoid.decidable_eq._default ordered_cancel_comm_monoid.le ordered_cancel_comm_monoid.lt localization.linear_ordered_cancel_comm_monoid._proof_14 localization.linear_ordered_cancel_comm_monoid._proof_15 localization.linear_ordered_cancel_comm_monoid._proof_16 localization.linear_ordered_cancel_comm_monoid._proof_17 localization.decidable_le, decidable_lt := localization.decidable_lt has_lt.lt.decidable, max := linear_ordered_comm_monoid.max._default ordered_cancel_comm_monoid.le ordered_cancel_comm_monoid.lt localization.linear_ordered_cancel_comm_monoid._proof_18 localization.linear_ordered_cancel_comm_monoid._proof_19 localization.linear_ordered_cancel_comm_monoid._proof_20 localization.linear_ordered_cancel_comm_monoid._proof_21 localization.decidable_le, max_def := _, min := linear_ordered_comm_monoid.min._default ordered_cancel_comm_monoid.le ordered_cancel_comm_monoid.lt localization.linear_ordered_cancel_comm_monoid._proof_23 localization.linear_ordered_cancel_comm_monoid._proof_24 localization.linear_ordered_cancel_comm_monoid._proof_25 localization.linear_ordered_cancel_comm_monoid._proof_26 localization.decidable_le, min_def := _}

mathlib3 documentation

Localizations of commutative monoids #

Implementation notes #

TODO #

Tags #

Order #