Localizing commutative monoids away from an alement

We treat the special case of localizing away from an element in the sections AwayMap and Away.

Tags

localization, monoid localization, quotient monoid, congruence relation, characteristic predicate, commutative monoid, grothendieck group

@[reducible, inline]

abbrev AddSubmonoid.LocalizationMap.AwayMap {M : Type u_1} [AddCommMonoid M] (x : M) (N' : Type u_4) [AddCommMonoid N'] : Type (max u_1 u_4)

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

Equations

• AddSubmonoid.LocalizationMap.AwayMap x N' = (AddSubmonoid.multiples x).LocalizationMap N'

@[reducible, inline]

abbrev Submonoid.LocalizationMap.AwayMap {M : Type u_1} [CommMonoid M] (x : M) (N' : Type u_4) [CommMonoid N'] : Type (max u_1 u_4)

Given x : M, the type of CommMonoid homomorphisms f : M →* N such that N is isomorphic to the Localization of M at the Submonoid generated by x.

Equations

• Submonoid.LocalizationMap.AwayMap x N' = (Submonoid.powers x).LocalizationMap N'

noncomputable def Submonoid.LocalizationMap.AwayMap.invSelf {M : Type u_1} [CommMonoid M] {N : Type u_2} [CommMonoid N] (x : M) (F : Submonoid.LocalizationMap.AwayMap x N) : N

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

Equations

• Submonoid.LocalizationMap.AwayMap.invSelf x F = Submonoid.LocalizationMap.mk' F 1 ⟨x, ⋯⟩

noncomputable def Submonoid.LocalizationMap.AwayMap.lift {M : Type u_1} [CommMonoid M] {N : Type u_2} [CommMonoid N] {P : Type u_3} [CommMonoid P] {g : M →* P} (x : M) (F : Submonoid.LocalizationMap.AwayMap x N) (hg : IsUnit (g x)) : N →* P

Given x : M, a Localization map F : M →* N away from x, and a map of CommMonoids 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.LocalizationMap.AwayMap.lift x F hg = Submonoid.LocalizationMap.lift F ⋯

@[simp]

theorem Submonoid.LocalizationMap.AwayMap.lift_eq {M : Type u_1} [CommMonoid M] {N : Type u_2} [CommMonoid N] {P : Type u_3} [CommMonoid P] {g : M →* P} (x : M) (F : Submonoid.LocalizationMap.AwayMap x N) (hg : IsUnit (g x)) (a : M) : (Submonoid.LocalizationMap.AwayMap.lift x F hg) ((Submonoid.LocalizationMap.toMap F) a) = g a

@[simp]

theorem Submonoid.LocalizationMap.AwayMap.lift_comp {M : Type u_1} [CommMonoid M] {N : Type u_2} [CommMonoid N] {P : Type u_3} [CommMonoid P] {g : M →* P} (x : M) (F : Submonoid.LocalizationMap.AwayMap x N) (hg : IsUnit (g x)) : (Submonoid.LocalizationMap.AwayMap.lift x F hg).comp (Submonoid.LocalizationMap.toMap F) = g

noncomputable def Submonoid.LocalizationMap.awayToAwayRight {M : Type u_1} [CommMonoid M] {N : Type u_2} [CommMonoid N] {P : Type u_3} [CommMonoid P] (x : M) (F : Submonoid.LocalizationMap.AwayMap x N) (y : M) (G : Submonoid.LocalizationMap.AwayMap (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.LocalizationMap.awayToAwayRight x F y G = Submonoid.LocalizationMap.AwayMap.lift x F ⋯

noncomputable def AddSubmonoid.LocalizationMap.AwayMap.negSelf {A : Type u_4} [AddCommMonoid A] (x : A) {B : Type u_5} [AddCommMonoid B] (F : AddSubmonoid.LocalizationMap.AwayMap x B) : B

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

Equations

• AddSubmonoid.LocalizationMap.AwayMap.negSelf x F = AddSubmonoid.LocalizationMap.mk' F 0 ⟨x, ⋯⟩

noncomputable def AddSubmonoid.LocalizationMap.AwayMap.lift {A : Type u_4} [AddCommMonoid A] (x : A) {B : Type u_5} [AddCommMonoid B] (F : AddSubmonoid.LocalizationMap.AwayMap x B) {C : Type u_6} [AddCommMonoid C] {g : A →+ C} (hg : IsAddUnit (g x)) : B →+ C

Given x : A, a localization map F : A →+ B away from x, and a map of AddCommMonoids 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

• AddSubmonoid.LocalizationMap.AwayMap.lift x F hg = AddSubmonoid.LocalizationMap.lift F ⋯

@[simp]

theorem AddSubmonoid.LocalizationMap.AwayMap.lift_eq {A : Type u_4} [AddCommMonoid A] (x : A) {B : Type u_5} [AddCommMonoid B] (F : AddSubmonoid.LocalizationMap.AwayMap x B) {C : Type u_6} [AddCommMonoid C] {g : A →+ C} (hg : IsAddUnit (g x)) (a : A) : (AddSubmonoid.LocalizationMap.AwayMap.lift x F hg) ((AddSubmonoid.LocalizationMap.toMap F) a) = g a

@[simp]

theorem AddSubmonoid.LocalizationMap.AwayMap.lift_comp {A : Type u_4} [AddCommMonoid A] (x : A) {B : Type u_5} [AddCommMonoid B] (F : AddSubmonoid.LocalizationMap.AwayMap x B) {C : Type u_6} [AddCommMonoid C] {g : A →+ C} (hg : IsAddUnit (g x)) : (AddSubmonoid.LocalizationMap.AwayMap.lift x F hg).comp (AddSubmonoid.LocalizationMap.toMap F) = g

noncomputable def AddSubmonoid.LocalizationMap.awayToAwayRight {A : Type u_4} [AddCommMonoid A] (x : A) {B : Type u_5} [AddCommMonoid B] (F : AddSubmonoid.LocalizationMap.AwayMap x B) {C : Type u_6} [AddCommMonoid C] (y : A) (G : AddSubmonoid.LocalizationMap.AwayMap (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

• AddSubmonoid.LocalizationMap.awayToAwayRight x F y G = AddSubmonoid.LocalizationMap.AwayMap.lift x F ⋯

@[reducible, inline]

abbrev AddLocalization.Away {M : Type u_1} [AddCommMonoid M] (x : M) : Type u_1

Given x : M, the Localization of M at the Submonoid generated by x, as a quotient.

Equations

• AddLocalization.Away x = AddLocalization (AddSubmonoid.multiples x)

@[reducible, inline]

abbrev Localization.Away {M : Type u_1} [CommMonoid 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)

theorem AddLocalization.Away.negSelf.proof_1 {M : Type u_1} [AddCommMonoid M] (x : M) : x ∈ AddSubmonoid.multiples x

def AddLocalization.Away.negSelf {M : Type u_1} [AddCommMonoid M] (x : M) : AddLocalization.Away x

Given x : M, negSelf is -x in the Localization (as a quotient type) of M at the Submonoid generated by x.

Equations

• AddLocalization.Away.negSelf x = AddLocalization.mk 0 ⟨x, ⋯⟩

def Localization.Away.invSelf {M : Type u_1} [CommMonoid M] (x : M) : Localization.Away x

Given x : M, invSelf is x⁻¹ in the Localization (as a quotient type) of M at the Submonoid generated by x.

Equations

• Localization.Away.invSelf x = Localization.mk 1 ⟨x, ⋯⟩

@[reducible, inline]

abbrev AddLocalization.Away.addMonoidOf {M : Type u_1} [AddCommMonoid M] (x : M) : AddSubmonoid.LocalizationMap.AwayMap x (AddLocalization.Away x)

Given x : M, the natural hom sending y : M, M an AddCommMonoid, to the equivalence class of (y, 0) in the Localization of M at the Submonoid generated by x.

Equations

• AddLocalization.Away.addMonoidOf x = AddLocalization.addMonoidOf (AddSubmonoid.multiples x)

@[reducible, inline]

abbrev Localization.Away.monoidOf {M : Type u_1} [CommMonoid M] (x : M) : Submonoid.LocalizationMap.AwayMap x (Localization.Away x)

Given x : M, the natural hom sending y : M, M a CommMonoid, to the equivalence class of (y, 1) in the Localization of M at the Submonoid generated by x.

Equations

• Localization.Away.monoidOf x = Localization.monoidOf (Submonoid.powers x)

theorem AddLocalization.Away.mk_eq_addMonoidOf_mk' {M : Type u_1} [AddCommMonoid M] (x : M) : AddLocalization.mk = AddSubmonoid.LocalizationMap.mk' (AddLocalization.Away.addMonoidOf x)

theorem Localization.Away.mk_eq_monoidOf_mk' {M : Type u_1} [CommMonoid M] (x : M) : Localization.mk = Submonoid.LocalizationMap.mk' (Localization.Away.monoidOf x)

noncomputable def AddLocalization.Away.addEquivOfQuotient {M : Type u_1} [AddCommMonoid M] {N : Type u_2} [AddCommMonoid N] (x : M) (f : AddSubmonoid.LocalizationMap.AwayMap x N) : AddLocalization.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

• AddLocalization.Away.addEquivOfQuotient x f = AddLocalization.addEquivOfQuotient f

noncomputable def Localization.Away.mulEquivOfQuotient {M : Type u_1} [CommMonoid M] {N : Type u_2} [CommMonoid N] (x : M) (f : Submonoid.LocalizationMap.AwayMap 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.mulEquivOfQuotient x f = Localization.mulEquivOfQuotient f