AddSubmonoid.LocalizationMap.eq_iff_exists
theorem AddSubmonoid.LocalizationMap.eq_iff_exists :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
(f : S.LocalizationMap N) {x y : M}, f.toMap x = f.toMap y ↔ ∃ c, ↑c + x = ↑c + y
The theorem `AddSubmonoid.LocalizationMap.eq_iff_exists` states that for any type `M` which is an instance of the `AddCommMonoid` typeclass, a submonoid `S` of `M`, another type `N` which is also an instance of the `AddCommMonoid` typeclass, and a localization map `f` from `S` to `N`, for any `x` and `y` of type `M`, the localization map applied to `x` equals the localization map applied to `y` if and only if there exists an element `c` from the submonoid such that `c` plus `x` equals `c` plus `y`. This theorem essentially describes a property of the commutativity of addition after the localization map is applied to elements of the original monoid.
More concisely: For any AddCommMonoid M, submonoid S, AddCommMonoid N, localization map f from S to N, and x, y in M, f(x) = f(y) if and only if there exists c in S such that x + c = y + c.
|
Submonoid.LocalizationMap.lift_spec
theorem Submonoid.LocalizationMap.lift_spec :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
[inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} (hg : ∀ (y : ↥S), IsUnit (g ↑y)) (z : N) (v : P),
(f.lift hg) z = v ↔ g (f.sec z).1 = g ↑(f.sec z).2 * v
This theorem is about the behavior of a localization map in the context of commutative monoids. Specifically, suppose we have a localization map `f : M →* N` from a commutative monoid `M` to another commutative monoid `N` with respect to a submonoid `S ⊆ M`. Additionally, let's say we have a map `g : M →* P` from `M` to a third commutative monoid `P`, which induces a map `f.lift hg : N →* P`.
The theorem then states that for any elements `z : N` and `v : P`, the equality `f.lift hg z = v` holds if and only if `g x = g y * v`, where `x : M` and `y : S` are elements such that `z * f y = f x`.
In other words, the lift of the localization map evaluated at `z` equals `v` precisely when the mapping of `x` under `g` is equal to the mapping of `y` under `g` times `v`. This provides a characterization of those elements that get mapped to `v` by the lift of the localization map.
More concisely: Given a localization map `f : M →* N` from commutative monoid `M` to `N` with respect to submonoid `S`, and a map `g : M →* P` to a third commutative monoid `P`, the equality `f.lift hg z = v` holds if and only if there exist `x : M` and `y : S` such that `z * f y = f x` and `g x = g y * v`.
|
AddSubmonoid.LocalizationMap.map_injective_of_injective
theorem AddSubmonoid.LocalizationMap.map_injective_of_injective :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
{P : Type u_3} [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} {Q : Type u_4}
[inst_3 : AddCommMonoid Q],
Function.Injective ⇑g → ∀ (k : (AddSubmonoid.map g S).LocalizationMap Q), Function.Injective ⇑(f.map ⋯ k)
This theorem states that given a function `g` which is an injective homomorphism from an additive commutative monoid `M` to another additive commutative monoid `P`, and given a submonoid `S` of `M`, the induced monoid homomorphism from the localization of `M` at `S` to the localization of `P` at the image of `S` under `g`, is also injective. In other words, if `g` is injective, then the map from the localization of `M` at `S` to the localization of `P` at `g(S)` preserves distinctness of elements.
More concisely: If `g` is an injective homomorphism from an additive commutative monoid `M` to another additive commutative monoid `P`, then the induced homomorphism from the localization of `M` at a submonoid `S` to the localization of `P` at `g(S)` is injective.
|
AddLocalization.induction_on₂
theorem AddLocalization.induction_on₂ :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {p : AddLocalization S → AddLocalization S → Prop}
(x y : AddLocalization S),
(∀ (x y : M × ↥S), p (AddLocalization.mk x.1 x.2) (AddLocalization.mk y.1 y.2)) → p x y
The theorem `AddLocalization.induction_on₂` states that for a given additive commutative monoid `M` and a submonoid `S` of `M`, if a property `p` holds for any two equivalence classes that are generated by `AddLocalization.mk` from pairs of elements in `M` and `S`, then the same property `p` holds for any two elements in the localization of `M` at `S`. In other words, this theorem provides a principle of induction for proving properties about pairs of elements in the localization.
More concisely: Given an additive commutative monoid `M` and a submonoid `S`, if a property `p` holds for any pair of elements in the equivalence classes generated by `AddLocalization.mk` from elements in `M` and `S`, then `p` holds for any pair of elements in the localization of `M` at `S`.
|
Submonoid.LocalizationWithZeroMap.isLeftRegular_of_le_IsCancelMulZero
theorem Submonoid.LocalizationWithZeroMap.isLeftRegular_of_le_IsCancelMulZero :
∀ {M : Type u_1} [inst : CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoidWithZero N],
S.LocalizationWithZeroMap N →
∀ [inst_2 : IsCancelMulZero M], (∀ ⦃x : M⦄, x ∈ S → IsRegular x) → IsCancelMulZero N
This theorem, `Submonoid.LocalizationWithZeroMap.isLeftRegular_of_le_IsCancelMulZero`, states that given a localization map `f : M →*₀ N` for a submonoid `S` of a commutative monoid with zero `M`, if `M` is a cancellative monoid with zero, and all elements of `S` are regular (i.e., non-zero divisors), then `N` is also a cancellative monoid with zero. In other words, the cancellation property and the property of being a monoid with zero are preserved under the localization map for regular elements of the submonoid.
More concisely: Given a localization map from a commutative submonoid with zero and cancellative elements to a commutative monoid with zero, if all elements of the submonoid are regular, then the localization is a cancellative monoid with zero.
|
Submonoid.LocalizationMap.isUnit_comp
theorem Submonoid.LocalizationMap.isUnit_comp :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
[inst_2 : CommMonoid P] (f : S.LocalizationMap N) (j : N →* P) (y : ↥S), IsUnit ((j.comp f.toMap) ↑y)
This theorem states that for any commutative monoid `M`, a submonoid `S` of `M`, another commutative monoid `N`, yet another commutative monoid `P`, a localization map `f` from `S` to `N`, a monoid homomorphism `j` from `N` to `P`, and an element `y` of `S`, the result of first applying the localization map `f` on `y` and then applying the monoid homomorphism `j` on the result, is a unit of the final monoid `P`. In other words, the result has a two-sided inverse in `P`. This can be expressed as `IsUnit ((MonoidHom.comp j (Submonoid.LocalizationMap.toMap f)) ↑y)`. The notation `MonoidHom.comp j (Submonoid.LocalizationMap.toMap f)` refers to the composition of the monoid homomorphism `j` and the localization map `f`.
More concisely: For any commutative monoids M, N, and P, a submonoid S of M, a localization map f from S to N, a monoid homomorphism j from N to P, and any element y in S, the composite of j and the localization map f at y is a unit in P.
|
AddLocalization.r_iff_exists
theorem AddLocalization.r_iff_exists :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {x y : M × ↥S},
(AddLocalization.r S) x y ↔ ∃ c, ↑c + (↑y.2 + x.1) = ↑c + (↑x.2 + y.1)
The theorem `AddLocalization.r_iff_exists` states that for any pair of elements `x` and `y` in the cartesian product of an additive commutative monoid `M` and an additive submonoid `S` of `M`, the elements `x` and `y` are related by the localization relation `AddLocalization.r` of `M` at `S` if and only if there exists an element `c` in `S` such that the sum of the second component of `y` and the first component of `x`, both lifted to `M` via the canonical map, equals the sum of the second component of `x` and the first component of `y`, again both lifted to `M`. This theorem thus gives a criterion for two elements of the cartesian product `M × S` to be related by the localization relation in terms of the existence of such a `c` in `S`.
More concisely: For elements `(x, y)` in the cartesian product of an additive commutative monoid `M` and an additive submonoid `S`, `AddLocalization.r(x, y)` if and only if there exists `c` in `S` such that `x + S.(y) = y + S.(x)` in `M`.
|
Localization.induction_on
theorem Localization.induction_on :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {p : Localization S → Prop} (x : Localization S),
(∀ (y : M × ↥S), p (Localization.mk y.1 y.2)) → p x
The theorem `Localization.induction_on` states that for any type `M` with a `CommMonoid` instance and any submonoid `S` of `M`, for any property `p` of the localization of `M` at `S`, if the property holds for all elements formed by the `Localization.mk` function (which takes a pair consisting of an element `y` of `M` and a member of `S`), then this property holds for all elements of the localization. Essentially, this theorem provides a method of induction for proving properties about all elements of the localization of a commutative monoid at a submonoid.
More concisely: If a property holds for the images of all elements of a commutative monoid and their submonoid under the localization construction, then it holds for all elements of the localization.
|
Submonoid.LocalizationMap.lift_comp
theorem Submonoid.LocalizationMap.lift_comp :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
[inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} (hg : ∀ (y : ↥S), IsUnit (g ↑y)),
(f.lift hg).comp f.toMap = g
This theorem is about monoid homomorphisms and submonoid localization maps in the context of commutative monoids. The theorem states that for any commutative monoids `M`, `N` and `P`, with `S` being a submonoid of `M`, given a localization map `f` from `S` to `N`, and a monoid homomorphism `g` from `M` to `P`, if every element of the submonoid `S` is a unit under the homomorphism `g`, then the composition of the lift of the localization map `f` (with respect to `g` and the condition on `S`) and the map of `f` itself is equal to `g`. In other words, the lift of `f` followed by the map of `f` gives back the original homomorphism `g`.
More concisely: If `f` is a localization map from a submonoid `S` of commutative monoids `M` to `N`, `g` is a monoid homomorphism from `M` to `P`, and every element in `S` is a unit under `g`, then the composition of `g` and the lift of `f` with respect to `g` is equal to `f`.
|
Submonoid.LocalizationMap.surj
theorem Submonoid.LocalizationMap.surj :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
(f : S.LocalizationMap N) (z : N), ∃ x, z * f.toMap ↑x.2 = f.toMap x.1
The theorem `Submonoid.LocalizationMap.surj` states that for any commutative monoid `M`, submonoid `S` of `M`, commutative monoid `N` and localization map `f` from `S` to `N`, and for any element `z` in `N`, there exists an element `x` such that multiplying `z` by the application of the localization map `f` to the second component of `x` equals the application of the localization map `f` to the first component of `x`. In other words, it says that the localization map is surjective, i.e., for every element in the codomain, there exists a corresponding element in the domain.
More concisely: For any commutative monoid homomorphism (localization map) from a submonoid to a commutative monoid, the image of the homomorphism is the entire codomain.
|
Localization.r_eq_r'
theorem Localization.r_eq_r' :
∀ {M : Type u_1} [inst : CommMonoid M] (S : Submonoid M), Localization.r S = Localization.r' S
The theorem `Localization.r_eq_r'` states that, in the context of a `CommMonoid` M and a submonoid S of M, the congruence relation (`Localization.r`) used to localize M at S can be equivalently expressed either as an infimum of a certain set or explicitly as per `Localization.r'`. In other words, these two definitions for the congruence relation, one through the infimum and the other through an explicit expression, are equivalent for any commutative monoid and its submonoid.
More concisely: In the context of a commutative monoid M and a submonoid S, the congruence relation for localizing M at S defined as the infimum of a certain set is equivalent to the explicitly defined relation `Localization.r'`.
|
Submonoid.LocalizationWithZeroMap.isLeftRegular_of_le_isCancelMulZero
theorem Submonoid.LocalizationWithZeroMap.isLeftRegular_of_le_isCancelMulZero :
∀ {M : Type u_1} [inst : CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoidWithZero N],
S.LocalizationWithZeroMap N →
∀ [inst_2 : IsCancelMulZero M], (∀ ⦃x : M⦄, x ∈ S → IsRegular x) → IsCancelMulZero N
The theorem `Submonoid.LocalizationWithZeroMap.isLeftRegular_of_le_isCancelMulZero` states that for a given localization map `f` from a monoid `M` to another monoid `N` where `M` is a cancellative monoid with zero, if all elements of a submonoid `S` of `M` are regular, then `N` is also a cancellative monoid with zero. In the context of algebra, a cancellative monoid with zero means that for any elements a, b, and c in the monoid, if the multiplication a*b equals a*c, then b equals c, except when a equals zero. Regular elements of a monoid are those for which there exists a "multiplicative inverse".
More concisely: If `f` is a localization map from a cancellative monoid `M` with zero to another monoid `N`, and all elements of a submonoid `S` of `M` have multiplicative inverses, then `N` is a cancellative monoid with zero.
|
Submonoid.LocalizationMap.mul_mk'_eq_mk'_of_mul
theorem Submonoid.LocalizationMap.mul_mk'_eq_mk'_of_mul :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
(f : S.LocalizationMap N) (x₁ x₂ : M) (y : ↥S), f.toMap x₁ * f.mk' x₂ y = f.mk' (x₁ * x₂) y
This theorem states that for any commutative monoid `M`, submonoid `S` of `M`, and commutative monoid `N`, given a localization map `f` from `M` to `N`, and elements `x₁`, `x₂` of `M` and `y` of `S`, the image of `x₁` under the localization map `f` multiplied by the image of the pair `(x₂, y)` under the mk' function of the localization map `f` is equal to the image of the pair `(x₁ * x₂, y)` under the mk' function of the localization map `f`. In other words, it asserts that applying the function `mk'` after a multiplication in `M` is the same as applying `mk'` first and then performing the multiplication in `N`.
More concisely: For any commutative monoids `M`, `N`, commutative monoid homomorphism `f` from `M` to `N`, submonoid `S` of `M`, and elements `x₁`, `x₂` in `M` and `y` in `S`, we have `f(x₁) * f(mk' x₂, y) = f(mk' (x₁ * x₂), y)`.
|
Submonoid.LocalizationMap.lift_eq
theorem Submonoid.LocalizationMap.lift_eq :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
[inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} (hg : ∀ (y : ↥S), IsUnit (g ↑y)) (x : M),
(f.lift hg) (f.toMap x) = g x
The theorem `Submonoid.LocalizationMap.lift_eq` states that for any commutative monoids `M`, `N`, and `P`, a submonoid `S` of `M`, a localization map `f` from the submonoid `S` of `M` to `N`, a monoid homomorphism `g` from `M` to `P` such that each element of `S` (when mapped by `g`) is a unit in `P`, and any element `x` of `M`, applying the function `lift` to the result of applying the function `toMap` of the localization map `f` to `x` is the same as applying the monoid homomorphism `g` to `x`. In other words, the lifted version of the localization map `f` is equal to the monoid homomorphism `g` when applied to elements of `M`.
More concisely: For any commutative monoids M, N, and P, a submonoid S of M, a localization map f from S to N, a monoid homomorphism g from M to P with g(s) a unit in P for all s in S, the lifted function of f via g is equal to g.
|
AddLocalization.add_def
theorem AddLocalization.add_def :
∀ {M : Type u_4} [inst : AddCommMonoid M] (S : AddSubmonoid M), AddLocalization.add S = Add.add
The theorem `AddLocalization.add_def` states that for any type `M` that forms an additive commutative monoid and any additive submonoid `S` of `M`, the addition operation defined on the localization of `M` at `S` is identical to the regular addition operation. Remember that the addition in `AddLocalization` is defined such that the sum of two elements `⟨a, b⟩` and `⟨c, d⟩` is `⟨a + c, b + d⟩`. This should not be confused with the counterpart in ring localization, which gives a different result.
More concisely: For any additive commutative monoid M and its additive submonoid S, the addition operation in the localization of M at S is equivalent to the regular addition operation on M.
|
AddLocalization.r_eq_r'
theorem AddLocalization.r_eq_r' :
∀ {M : Type u_1} [inst : AddCommMonoid M] (S : AddSubmonoid M), AddLocalization.r S = AddLocalization.r' S := by
sorry
This theorem states that two different definitions of the additive congruence relation, which is used to create a localization of an additive commutative monoid at a submonoid, are actually equivalent. The first definition, `AddLocalization.r`, describes the congruence relation as the infimum of all congruence relations that equate each element in the submonoid to zero. The second definition, `AddLocalization.r'`, provides a more explicit characterization of the congruence relation using an existential quantifier. The theorem asserts that for any additive commutative monoid `M` and any submonoid `S` of `M`, these two definitions of the additive congruence relation are identical.
More concisely: For any additive commutative monoid M and submonoid S, the additive congruence relation on M defined as the infimum of congruences equating elements in S to zero is equivalent to the relation defined existentially as the class of pairs (a, b) in M such that there exist x in S and n in ℕ with a = b + nx.
|
AddSubmonoid.LocalizationMap.map_map
theorem AddSubmonoid.LocalizationMap.map_map :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
{P : Type u_3} [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} {T : AddSubmonoid P}
(hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_4} [inst_3 : AddCommMonoid Q] {k : T.LocalizationMap Q} {A : Type u_5}
[inst_4 : AddCommMonoid A] {U : AddSubmonoid A} {R : Type u_6} [inst_5 : AddCommMonoid R]
(j : U.LocalizationMap 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
The theorem `AddSubmonoid.LocalizationMap.map_map` in Lean 4 states that for given additive commutative monoids `M`, `N`, `P`, `Q`, `A` and `R`, and submonoids `S` of `M`, `T` of `P`, and `U` of `A`, along with the localization maps `f : S.LocalizationMap N`, `k : T.LocalizationMap Q`, and `j : U.LocalizationMap R`, and the additive homomorphisms `g : M →+ P` and `l : P →+ A` satisfying certain conditions, the composition of the induced maps of localizations equals the map of localizations induced by the composition `l ∘ g`. Specifically, for any element `x` in `N`, `(k.map hl j) ((f.map hy k) x) = (f.map (λ y, hl (hy y)) j) x`.
More concisely: For additive commutative monoids M, N, P, Q, A, submonoids S of M, T of P, and U of A, localization maps f, k, j, and additive homomorphisms g and l satisfying certain conditions, the diagram commutes: (f.map (λ y, hl (hy y)) j) ∘ f = k ∘ (g.map hl)
(Note: hl denotes the localization homomorphism from N to Q, and hy denotes the homomorphism from P to Y induced by g.)
|
Submonoid.LocalizationMap.inv_inj
theorem Submonoid.LocalizationMap.inv_inj :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {f : M →* N}
(hf : ∀ (y : ↥S), IsUnit (f ↑y)) {y z : ↥S},
((IsUnit.liftRight (f.restrict S) hf) y)⁻¹ = ((IsUnit.liftRight (f.restrict S) hf) z)⁻¹ → f ↑y = f ↑z
This theorem states that given a commutative monoid `M`, a submonoid `S` of `M`, a monoid homomorphism `f` from `M` to another commutative monoid `N`, and if every element of `S` maps to a unit in `N` under `f`, then for all elements `y` and `z` in `S`, if the inverses of the images of `y` and `z` under the lift of `f` to `Nˣ` are equal, then the images of `y` and `z` under `f` are equal. In other words, if two elements in the submonoid have the same inverse under the lifted homomorphism, then they are mapped to the same element under the original homomorphism.
More concisely: If `f : M -> N` is a monoid homomorphism between commutative monoids `M` and `N`, `S` is a submonoid of `M` such that for all `s in S`, `f(s)` has a multiplicative inverse in `N`, then for all `y, z in S` with `f(y)^(-1) = f(z)^(-1)`, it follows that `f(y) = f(z)`.
|
Localization.mk_mul
theorem Localization.mk_mul :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} (a c : M) (b d : ↥S),
Localization.mk a b * Localization.mk c d = Localization.mk (a * c) (b * d)
The theorem `Localization.mk_mul` states that for any type `M` that forms a commutative monoid and any submonoid `S` of `M`, if you take two elements `a` and `c` from the commutative monoid `M` and two elements `b` and `d` from the submonoid `S`, the product of the localizations of `a` and `b`, and `c` and `d` is equal to the localization of the product of `a` and `c`, and `b` and `d`. In other words, the process of localization respects the multiplication operation of the original monoid.
More concisely: Let `M` be a commutative monoid and `S` a submonoid. For all `a, c in M` and `b, d in S`, the localization of `a` and `b` times the localization of `c` and `d` equals the localization of `a` times `c` and `b` times `d`.
|
Submonoid.LocalizationMap.eq_iff_exists
theorem Submonoid.LocalizationMap.eq_iff_exists :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
(f : S.LocalizationMap N) {x y : M}, f.toMap x = f.toMap y ↔ ∃ c, ↑c * x = ↑c * y
The theorem `Submonoid.LocalizationMap.eq_iff_exists` states that for any commutative monoid `M`, submonoid `S` of `M`, and commutative monoid `N`, if `f` is a localization map from `S` to `N`, then for any elements `x` and `y` of `M`, the equality of `f(x)` and `f(y)` in `N` is equivalent to there being an element `c` in `S` such that `c * x = c * y` in `M`. In other words, the images of two elements under the localization map are equal if and only if their products with some element in the submonoid are equal.
More concisely: For any commutative monoids M, S, and N, and localization map f from S to N, the equality of f(x) and f(y) in N holds if and only if there exists c in S such that x * c = y * c in M.
|
Submonoid.LocalizationMap.map_injective_of_injective
theorem Submonoid.LocalizationMap.map_injective_of_injective :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
[inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} {Q : Type u_4} [inst_3 : CommMonoid Q],
Function.Injective ⇑g → ∀ (k : (Submonoid.map g S).LocalizationMap Q), Function.Injective ⇑(f.map ⋯ k)
This theorem states that given a commutative monoid `M` and a submonoid `S` of `M`, if you have an injective commutative monoid homomorphism `g` from `M` to another commutative monoid `P`, then the induced monoid homomorphism from the localization of `M` at `S` to the localization of `P` at the image of `S` under `g`, i.e., `g(S)`, is also injective. This essentially means that if a function preserves the monoid structure and is injective, then even after localizing at some submonoids, the homomorphism induced by the function remains injective.
More concisely: If `g` is an injective commutative monoid homomorphism from a commutative monoid `M` to another commutative monoid `P`, then the induced homomorphism from the localization of `M` at a submonoid `S` to the localization of `P` at `g(S)` is injective.
|
AddSubmonoid.LocalizationMap.lift_spec
theorem AddSubmonoid.LocalizationMap.lift_spec :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
{P : Type u_3} [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P}
(hg : ∀ (y : ↥S), IsAddUnit (g ↑y)) (z : N) (v : P), (f.lift hg) z = v ↔ g (f.sec z).1 = g ↑(f.sec z).2 + v
The theorem `AddSubmonoid.LocalizationMap.lift_spec` states that for a given localization map `f: M →+ N` for a submonoid `S ⊆ M`, if an additive commutative monoid map `g : M →+ P` induces another map `f.lift hg : N →+ P`, then for any elements `z : N` and `v : P`, the statement `f.lift hg z = v` is equivalent to `g x = g y + v`, where `x : M` and `y ∈ S` are elements fulfilling the condition `z + f y = f x`.
Here, `M`, `N`, and `P` are types representing additive commutative monoids, `f : M →+ N` is a localization map, `S` is a submonoid of `M`, and `g : M →+ P` is an additive commutative monoid map. The function `f.lift hg : N →+ P` is a map induced by `g` such that for any `y` in `S`, `g y` is an add unit. The term `AddSubmonoid.LocalizationMap.sec f z` provides a pair of elements `(x, y)` from `M × S` such that `z + f y = f x`.
More concisely: Given a localization map `f : M → N` for a submonoid `S ⊆ M`, if there exists an additive commutative monoid map `g : M → P` such that `f.lift (g) (z) = v` if and only if `g(x) = g(y) + v` for some `x ∈ M` and `y ∈ S` with `z + f(y) = f(x)`, then `f.lift (g)` is the unique additive commutative monoid map from `N` to `P` making the diagram commute.
|
Localization.liftOn_mk
theorem Localization.liftOn_mk :
∀ {M : Type u_1} [inst : CommMonoid 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).liftOn f H = f a b
The theorem `Localization.liftOn_mk` states that, for a given commutative monoid `M` and a submonoid `S`, for any type `p` and function `f : M → ↥S → p` satisfying the property that if the congruence relation `Localization.r S` holds between `(a, b)` and `(c, d)`, then `f a b` equals `f c d`, then the `Localization.liftOn` operation on the equivalence class of `(a, b)` (created by `Localization.mk a b`) with function `f` and property `H` is equal to `f a b`. In other words, when we lift a function `f` to the entire localization under these conditions, applying this lifted function to the localization of `a` and `b` retrieves the original function `f` applied to `a` and `b`.
More concisely: If `M` is a commutative monoid, `S` a submonoid, `f : M → ↥S → p`, and for any `(a, b)` and `(c, d)` such that `Localization.r S` holds between them implies `f a b = f c d`, then `Localization.liftOn (Localization.mk a b) f = f a b`.
|
AddSubmonoid.LocalizationMap.eq_of_eq
theorem AddSubmonoid.LocalizationMap.eq_of_eq :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
{P : Type u_3} [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P},
(∀ (y : ↥S), IsAddUnit (g ↑y)) → ∀ {x y : M}, f.toMap x = f.toMap y → g x = g y
The theorem `AddSubmonoid.LocalizationMap.eq_of_eq` states that given an additive localization map `f` from an additive commutative monoid `M` to an additive commutative monoid `N` with respect to a submonoid `S` of `M`, and another additive monoid homomorphism `g` from `M` to an additive commutative monoid `P` such that the image under `g` of `S` is a subset of the additive units of `P`, if for any two elements `x` and `y` in `M`, `f(x)` equals `f(y)`, then `g(x)` must be equal to `g(y)`.
In simpler terms, if two elements in `M` map to the same value in `N` under the localization map `f`, and if the homomorphism `g` transforms the submonoid `S` into additive units in `P`, then these two elements will also map to the same value under the homomorphism `g`.
More concisely: If `f` is an additive localization map from an additive commutative monoid `M` to an additive commutative monoid `N` with respect to a submonoid `S`, and `g` is an additive monoid homomorphism from `M` to an additive commutative monoid `P` such that the image of `S` under `g` are additive units in `P`, then `x = y` in `M` implies `g(x) = g(y)` in `P`.
|
Submonoid.LocalizationMap.surj₂
theorem Submonoid.LocalizationMap.surj₂ :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
(f : S.LocalizationMap N) (z w : N), ∃ z' w' d, z * f.toMap ↑d = f.toMap z' ∧ w * f.toMap ↑d = f.toMap w'
The theorem `Submonoid.LocalizationMap.surj₂` states that for any given localization map `f` from a commutative monoid `M` to another commutative monoid `N`, and any two elements `z` and `w` from `N`, there exist three elements `z'`, `w'`, and `d` from `M` and `S` (which is a submonoid of `M`) such that `z` and `w` are respectively equivalent to the fractions `f(z') / f(d)` and `f(w') / f(d)`. In other words, every element of `N` can be represented as a fraction of elements from `M`, mapped by `f`, divided by an element from `S`, also mapped by `f`.
More concisely: For any commutative monoid homomorphism `f` from `M` to `N` and any `z, w` in `N`, there exist `z'` and `w'` in `M` and `d` in the submonoid `S` of `M` such that `z = f(z')/f(d)` and `w = f(w')/f(d)`.
|
AddSubmonoid.LocalizationMap.surj
theorem AddSubmonoid.LocalizationMap.surj :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
(f : S.LocalizationMap N) (z : N), ∃ x, z + f.toMap ↑x.2 = f.toMap x.1
This theorem, `AddSubmonoid.LocalizationMap.surj`, states that for any given types `M` and `N`, where `M` is an additive commutative monoid and `N` is also an additive commutative monoid, for any localization map `f` from a submonoid `S` of `M` to `N` and for any element `z` of `N`, there exists an element `x` such that adding `z` to the image of `x.2` under `f` equals the image of `x.1` under `f`. In other words, every element in `N` can be represented as the sum of the localization map applied to some element of `M` plus the localization map applied to an element of `S`.
More concisely: For any additive commutative monoids M and N, any submonoid S of M, and any localization map f from S to N, for every element z in N, there exists an element x in S such that f(x.1 + s) = f(x.1) + z for some s in S.
|
AddSubmonoid.LocalizationMap.map_add_left
theorem AddSubmonoid.LocalizationMap.map_add_left :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
{P : Type u_3} [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} {T : AddSubmonoid P}
(hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_4} [inst_3 : AddCommMonoid Q] {k : T.LocalizationMap Q} (z : N),
k.toMap (g ↑(f.sec z).2) + (f.map hy k) z = k.toMap (g (f.sec z).1)
This theorem states that for any additive commutative monoids `M`, `N`, `P`, and `Q`, given localization maps `f : M →+ N` for a submonoid `S` and `k : P →+ Q` for a submonoid `T`, if an additive (or commutative) monoid homomorphism `g : M →+ P` induces a map `f.map hy k : N →+ Q`, then for any element `z` in `N`, we have `k (g y) + f.map hy k z = k (g x)`, where `x` is an element in `M` and `y` is an element in `S` such that `z + f y = f x`.
More concisely: Given additive commutative monoids `M`, `N`, `P`, `Q`, localization maps `f : M →+ N` and `k : P →+ Q`, if a homomorphism `g : M →+ P` induces `f.map hy k` and `x ∈ M`, `y ∈ S` satisfy `z + f y = f x`, then `k (g x) = k (g y) + f.map hy k z`.
|
AddSubmonoid.LocalizationMap.lift_comp
theorem AddSubmonoid.LocalizationMap.lift_comp :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
{P : Type u_3} [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P}
(hg : ∀ (y : ↥S), IsAddUnit (g ↑y)), (f.lift hg).comp f.toMap = g
The theorem `AddSubmonoid.LocalizationMap.lift_comp` states that for any additive commutative monoid `M`, an additive submonoid `S` of `M`, additive commutative monoids `N` and `P`, a localization map `f` from `S` to `N`, and an additive monoid homomorphism `g` from `M` to `P` such that every element `y` in `S` is an add-unit under `g`, the composition of the lift of `f` with respect to `g` and the map from `M` to `N` induced by `f` is equal to `g`. In other words, it expresses the unique property of the lifting operation in the context of localization of additive monoids.
More concisely: For any additive commutative monoids $M$, $N$, $P$, an additive submonoid $S$ of $M$, an additive commutative monoid homomorphism $g : M \to P$ such that every element in $S$ is an add-unit under $g$, and a localization map $f : S \to N$, the composition of the lift of $f$ with respect to $g$ and the map induced by $f$ is equal to $g$.
|
Localization.mk_eq_monoidOf_mk'_apply
theorem Localization.mk_eq_monoidOf_mk'_apply :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} (x : M) (y : ↥S),
Localization.mk x y = (Localization.monoidOf S).mk' x y
This theorem states that, for any commutative monoid `M` and any submonoid `S` of `M`, and for any elements `x` in `M` and `y` in `S`, the localization of `M` at `S` created by the `Localization.mk` function applied to `x` and `y` is equal to the result of applying the `Submonoid.LocalizationMap.mk'` function to the natural homomorphism `Localization.monoidOf S` and the elements `x` and `y`. In other words, these two methods of creating a localization of a commutative monoid at a submonoid yield the same result.
More concisely: For any commutative monoid M and submonoid S, the localization of M at S using `Localization.mk` equals the localization of the submonoid homomorphism from M to S using `Submonoid.LocalizationMap.mk`.
|
AddSubmonoid.LocalizationMap.sec_spec
theorem AddSubmonoid.LocalizationMap.sec_spec :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
{f : S.LocalizationMap N} (z : N), z + f.toMap ↑(f.sec z).2 = f.toMap (f.sec z).1
This theorem states that for any type `M` with an additive commutative monoid structure, a submonoid `S` of `M`, another type `N` with an additive commutative monoid structure, and a localization map `f` from `S` to `N`, for any element `z` of `N`, the sum of `z` and the application of the `toMap` function of `f` to the second element of the pair returned by the `sec` function of `f` applied to `z`, is equal to the result of applying the `toMap` function of `f` to the first element of the pair returned by the `sec` function of `f` applied to `z`. In other words, the theorem establishes an important property connecting the `sec` function and the `toMap` function in the context of localization maps in additive commutative monoid structures.
More concisely: For any additive commutative monoid homomorphism (localization map) `f` from `S` to `N`, and for any `z` in `N`, we have `f (z + f! (s, t).2) = f (s + t)`, where `s` is the first component of `f! (z, t)` and `f!` is the localization map's section function.
|
AddSubmonoid.LocalizationMap.mk'_eq_iff_eq
theorem AddSubmonoid.LocalizationMap.mk'_eq_iff_eq :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
(f : S.LocalizationMap N) {x₁ x₂ : M} {y₁ y₂ : ↥S},
f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ f.toMap (↑y₂ + x₁) = f.toMap (↑y₁ + x₂)
This theorem states that for any additive commutative monoid `M`, any additive submonoid `S` of `M`, any other additive commutative monoid `N`, and any localization map `f` from `S` to `N`, for any two elements `x₁` and `x₂` in `M`, and any two elements `y₁` and `y₂` in `S`, the two elements obtained by applying the localization map to the pairs `(x₁, y₁)` and `(x₂, y₂)` are equal if and only if the result of applying the map to the element `y₂ + x₁` is equal to the result of applying the map to the element `y₁ + x₂`. In other words, the equality of the images under the localization map of two pairs is equivalent to a certain equality involving the map's action on the sums of the pair elements.
More concisely: For any additive commutative monoids M, N and localization map f from an additive submonoid S of M to N, the pairs (x, y) in MxS and (x', y') in SxS have the same image under f if and only if y + x = y' + x'.
|
Submonoid.LocalizationMap.map_mul_right
theorem Submonoid.LocalizationMap.map_mul_right :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
[inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} {T : Submonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T)
{Q : Type u_4} [inst_3 : CommMonoid Q] {k : T.LocalizationMap Q} (z : N),
(f.map hy k) z * k.toMap (g ↑(f.sec z).2) = k.toMap (g (f.sec z).1)
This theorem states that for any localization maps `f : M →* N` and `k : P →* Q` corresponding to submonoids `S` and `T`, and a `CommMonoid` homomorphism `g : M →* P` that induces a new map `f.map hy k : N →* Q`, the product of the image of any `z : N` under this new map and the image of `g y` under `k` is equal to the image of `g x` under `k`. This holds for all `z : N` and for any `x : M` and `y ∈ S` such that `z * f y = f x`. The theorem encapsulates a key property of the interactions between localization maps and homomorphisms in the context of commutative monoids.
More concisely: For any commutative monoid homomorphism $g : M \to P$, localization maps $f : M \to* N$ and $k : P \to* Q$, and $x \in M$, $y \in S$, and $z \in N$ such that $z \cdot f(y) = f(x)$, we have $k(g(x)) \cdot z = k(g(y)) \cdot f(x)$.
|
Submonoid.LocalizationMap.inv_unique
theorem Submonoid.LocalizationMap.inv_unique :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {f : M →* N}
(h : ∀ (y : ↥S), IsUnit (f ↑y)) {y : ↥S} {z : N}, f ↑y * z = 1 → ↑((IsUnit.liftRight (f.restrict S) h) y)⁻¹ = z
This theorem states that, given a homomorphism `f` from a commutative monoid `M` to another commutative monoid `N` and a submonoid `S` of `M` such that the image of `S` under `f` lies in the units of `N` (i.e., `f(S) ⊆ Nˣ`), for every element `y` in `S`, the inverse of `f(y)` is unique. Specifically, if `f(y) * z = 1`, then `z` is equal to the inverse of the unit that `y` maps to under the lift of `f` to `Nˣ`, which is denoted as `IsUnit.liftRight (f.restrict S) h`, where `h` is a proof that for every `y` in `S`, `f(y)` is a unit.
More concisely: Given a homomorphism `f` from a commutative monoid `M` to another commutative monoid `N` with `f(S) ⊆ N^1` for some submonoid `S` of `M`, every element `y` in `S` has a unique right inverse in `N` among elements that map to units of `N` under `f`.
|
Submonoid.LocalizationMap.map_map
theorem Submonoid.LocalizationMap.map_map :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
[inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} {T : Submonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T)
{Q : Type u_4} [inst_3 : CommMonoid Q] {k : T.LocalizationMap Q} {A : Type u_5} [inst_4 : CommMonoid A]
{U : Submonoid A} {R : Type u_6} [inst_5 : CommMonoid R] (j : U.LocalizationMap 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
This theorem states that given two commutative monoid homomorphisms `g : M →* P` and `l : P →* A` that induce maps of localizations, the composition of the induced maps equals the map of localizations induced by the composition `l ∘ g`. This holds for all elements `x : N` in the domain of the first induced map. The theorem requires that for every element in the source submonoid `S`, `g` maps it into the target submonoid `T`, and similarly, `l` maps every element in `T` into the submonoid `U`. The theorem applies to any commutative monoids `M, N, P, Q, A, R` and their submonoids `S, T, U`.
More concisely: Given commutative monoid homomorphisms `g : M →* P` and `l : P →* A` that induce maps of localizations and map submonoids `S` of `M` into `T` of `P` and `T` into `U` of `A`, respectively, the induced maps `l∘g` and `l∘g^l` agree on elements of `S`.
|
AddSubmonoid.LocalizationMap.add_neg
theorem AddSubmonoid.LocalizationMap.add_neg :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
{f : M →+ N} (h : ∀ (y : ↥S), IsAddUnit (f ↑y)) {x₁ x₂ : M} {y₁ y₂ : ↥S},
f x₁ + ↑(-(IsAddUnit.liftRight (f.restrict S) h) y₁) = f x₂ + ↑(-(IsAddUnit.liftRight (f.restrict S) h) y₂) ↔
f (x₁ + ↑y₂) = f (x₂ + ↑y₁)
The theorem `AddSubmonoid.LocalizationMap.add_neg` states that for a given additive monoid homomorphism `f : M →+ N` and a submonoid `S` of `M` such that the image of `S` through `f` lies entirely in the additive units of `N`, for any two elements `x₁` and `x₂` from `M` and any two elements `y₁` and `y₂` from `S`, the equality `f x₁ - f y₁ = f x₂ - f y₂` is equivalent to `f (x₁ + y₂) = f (x₂ + y₁)`. In other words, under the conditions mentioned, the difference in the function's image values for two pairs of elements is the same if and only if the function's image values for the sum of each pair swapped between the pairs are the same. This is an important property in the study of localizations of additive monoids.
More concisely: Given an additive monoid homomorphism `f` and a submonoid `S` of its domain such that `f(S)` lies in the additive units of the codomain, for all `x₁, x₂ in M` and `y₁, y₂ in S`, `f(x₁ + y₂) = f(x₂ + y₁)` if and only if `f(x₁) - f(y₁) = f(x₂) - f(y₂)`.
|
Localization.mk_zero
theorem Localization.mk_zero :
∀ {M : Type u_1} [inst : CommMonoidWithZero M] {S : Submonoid M} (x : ↥S), Localization.mk 0 x = 0
The theorem `Localization.mk_zero` states that for any commutative monoid with zero `M` and any submonoid `S` of `M`, and for any element `x` in `S`, the localization of `M` at `S` of the pair `(0, x)` is equal to zero. Here, `0` represents the zero element of the monoid `M`. Essentially, this says that the zero of the original monoid maps to the zero in the localization.
More concisely: For any commutative monoid with zero `M`, submonoid `S`, and element `x` in `S`, the localization of `M` at `S` of the pair `(0, x)` equals the zero element in the localization.
|
AddSubmonoid.LocalizationMap.ofAddEquivOfDom_id
theorem AddSubmonoid.LocalizationMap.ofAddEquivOfDom_id :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
(f : S.LocalizationMap N), f.ofAddEquivOfDom ⋯ = f
This theorem states that for any localization map `f` from an additive commutative monoid `M` to another additive commutative monoid `N`, with `S` as an additive submonoid of `M`, the function `f.ofAddEquivOfDom` composed with the identity function is equal to `f` itself. In other words, applying the function `f.ofAddEquivOfDom` to any element in the domain of the localization map has no effect, the output is the same as just applying `f`. This is a special case of a more general property in function theory, that for any function `f`, `f ∘ id = f`.
More concisely: For any localization map `f` from an additive commutative monoid `M` to another additive commutative monoid `N` and additive submonoid `S` of `M`, `f.ofAddEquivOfDom = f`.
|
Submonoid.LocalizationMap.eq_of_eq
theorem Submonoid.LocalizationMap.eq_of_eq :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
[inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P},
(∀ (y : ↥S), IsUnit (g ↑y)) → ∀ {x y : M}, f.toMap x = f.toMap y → g x = g y
This theorem states that, given a localization map `f` from a commutative monoid `M` to another commutative monoid `N`, associated with a submonoid `S` of `M`, and another map `g` from `M` to a third commutative monoid `P` such that the image of `S` under `g` lies within the group of units of `P`, if two elements `x` and `y` of `M` are mapped to the same element under `f`, then they must also be mapped to the same element under `g`. This is a property of localization maps in the context of commutative monoids.
More concisely: Given a localization map `f` from commutative monoid `M` to `N` with respect to submonoid `S`, and a map `g` from `M` to commutative monoid `P` with `g(S)` in the group of units of `P`, if `f(x) = f(y)` for all `x, y` in `M`, then `g(x) = g(y)`.
|
AddSubmonoid.LocalizationMap.surj₂
theorem AddSubmonoid.LocalizationMap.surj₂ :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
(f : S.LocalizationMap N) (z w : N), ∃ z' w' d, z + f.toMap ↑d = f.toMap z' ∧ w + f.toMap ↑d = f.toMap w'
This theorem states that for any localization map `f` from an additive commutative monoid `M` to another additive commutative monoid `N`, and any two elements `z` and `w` of `N`, there exists three elements `z'`, `w'`, and `d` in `M` such that the image of `z'` under `f`, plus the image of `d`, equals `z`, and similarly, the image of `w'` under `f`, plus the image of `d`, equals `w`. The important point here is that the same `d` works for both `z` and `w`. This theorem is fundamental in the study of localization of rings and modules in algebra.
More concisely: For any additive commutative monoid homomorphism `f` from an additive commutative monoid `M` to another such monoid `N`, and for any elements `z` and `w` in `N`, there exists an element `d` in `M` such that `f(d)` can be added to the images of `z` and `w` under `f` to obtain `z` and `w` respectively.
|
Submonoid.LocalizationMap.mul_inv_right
theorem Submonoid.LocalizationMap.mul_inv_right :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {f : M →* N}
(h : ∀ (y : ↥S), IsUnit (f ↑y)) (y : ↥S) (w z : N),
z = w * ↑((IsUnit.liftRight (f.restrict S) h) y)⁻¹ ↔ z * f ↑y = w
This theorem describes a property of homomorphisms between monoids in the context of localization of a monoid at a submonoid. Given a monoid homomorphism `f` from a monoid `M` to another monoid `N`, and a submonoid `S` of `M` such that the image of `S` under `f` lies in the group of units of `N`, the theorem states that for any elements `w` and `z` of `N` and any element `y` of `S`, the equation `z = w * (f(y))⁻¹` is equivalent to `z * f(y) = w`. Here, `(f(y))⁻¹` refers to the multiplicative inverse of `f(y)` in the monoid `N`. This property can be useful in the study of localizations in algebra, where we often consider the relation between elements of a ring and its localization.
More concisely: Given a monoid homomorphism `f` from a monoid `M` to another monoid `N` with `S` a submonoid of `M` such that `f(S)` lies in the group of units of `N`, the equation `z * f(y) = w` is equivalent to `z = w * f(y)⁻¹` for any `w, z ∈ N` and `y ∈ S`.
|
AddSubmonoid.LocalizationMap.lift_spec_add
theorem AddSubmonoid.LocalizationMap.lift_spec_add :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
{P : Type u_3} [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P}
(hg : ∀ (y : ↥S), IsAddUnit (g ↑y)) (z : N) (w v : P),
(f.lift hg) z + w = v ↔ g (f.sec z).1 + w = g ↑(f.sec z).2 + v
The theorem, named as `AddSubmonoid.LocalizationMap.lift_spec_add`, states that for any given Localization map `f` from an `AddCommMonoid` `M` to another `AddCommMonoid` `N` with respect to a Submonoid `S` of `M`, if there exists an `AddCommMonoid` map `g` from `M` to `P` which induces another map `f.lift hg` from `N` to `P`, then for all `z` in `N` and `v, w` in `P`, the sum of the images of `z` under `f.lift hg` and `w` is equal to `v` if and only if the sum of the images under `g` of `x` in `M` and `w` is equal to the sum of the images under `g` of `y` in `S` and `v`. Here `x` and `y` are such that the sum of `z` and `f y` is equal to `f x`.
In simpler terms, it relates the additive properties of elements under certain mappings and conditions in the context of Commutative Monoids and Localization maps, ensuring the preservation of addition operation while lifting from one additive commutative monoid to another.
More concisely: Given a Localization map `f` from an AddCommMonoid `M` to another AddCommMonoid `N` with respect to a Submonoid `S` of `M`, and AddCommMonoid maps `g: M -> P` and its induced map `hg: N -> P`, if the sum of `z` in `N` and `fy` equals `fx` for some `x` in `M`, then the sum of the images of `z` and `w` in `P` under `f.lift hg` is equal to the sum of the images of `x` and `w` under `g`.
|
Submonoid.LocalizationMap.mk'_eq_iff_eq
theorem Submonoid.LocalizationMap.mk'_eq_iff_eq :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
(f : S.LocalizationMap N) {x₁ x₂ : M} {y₁ y₂ : ↥S},
f.mk' x₁ y₁ = f.mk' x₂ y₂ ↔ f.toMap (↑y₂ * x₁) = f.toMap (↑y₁ * x₂)
The theorem `Submonoid.LocalizationMap.mk'_eq_iff_eq` states that for any given localization map `f` of a commutative monoid `M` into a commutative monoid `N` with respect to a submonoid `S` of `M`, and any elements `x₁, x₂` of `M` and `y₁, y₂` of `S`, the equality of the images of `(x₁, y₁)` and `(x₂, y₂)` under the map `Submonoid.LocalizationMap.mk' f` is equivalent to the equality of the images of `y₂ * x₁` and `y₁ * x₂` under the map `Submonoid.LocalizationMap.toMap f`. This captures a key property of the localization construction in algebra, providing a criterion for equality in the localized monoid `N`.
More concisely: For any commutative monoid homomorphism `f` from `M` to `N` with respect to a submonoid `S` of `M`, the images of `(y₁ * x₁)` and `(y₂ * x₂)` under `Submonoid.LocalizationMap.toMap f` are equal if and only if the images of `(x₁, y₁)` and `(x₂, y₂)` under `Submonoid.LocalizationMap.mk' f` are equal.
|
Submonoid.LocalizationMap.map_units
theorem Submonoid.LocalizationMap.map_units :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
(f : S.LocalizationMap N) (y : ↥S), IsUnit (f.toMap ↑y)
The theorem `Submonoid.LocalizationMap.map_units` states that for any commutative monoid `M`, any submonoid `S` of `M`, any commutative monoid `N` and any localization map `f` from `S` to `N`, if we have an element `y` of the submonoid `S`, then the image of `y` under the localization map `f` (obtained by applying the `Submonoid.LocalizationMap.toMap` function to `f` and `y`) is a unit in the monoid. In other words, it has a two-sided inverse. The `IsUnit` function checks whether this is the case.
More concisely: For any commutative monoids M, N, submonoid S of M, and localization map f from S to N, the image of any element y in S under f is a unit in N.
|
Submonoid.LocalizationMap.sec_spec
theorem Submonoid.LocalizationMap.sec_spec :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
{f : S.LocalizationMap N} (z : N), z * f.toMap ↑(f.sec z).2 = f.toMap (f.sec z).1
The theorem `Submonoid.LocalizationMap.sec_spec` states that for any commutative monoid `M`, any submonoid `S` of `M`, any commutative monoid `N`, and any localization map `f` from `S` to `N`, given any element `z` of `N`, the result of multiplying `z` by the image under `f` of the second component of the pair obtained by applying the section function to `z` is equal to the image under `f` of the first component of that pair. This essentially says that each element of the target monoid `N` can be expressed as the product of the image of an element of `M` and the inverse of the image of an element of `S`, which is a central property of the localization at a submonoid.
More concisely: For any commutative monoids M, N, submonoid S of M, and localization map f from S to N, for all z in N and (x, y) in S, f(y) * f(x) = f(x * y).
|
AddSubmonoid.LocalizationMap.add_mk'_eq_mk'_of_add
theorem AddSubmonoid.LocalizationMap.add_mk'_eq_mk'_of_add :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
(f : S.LocalizationMap N) (x₁ x₂ : M) (y : ↥S), f.toMap x₁ + f.mk' x₂ y = f.mk' (x₁ + x₂) y
This theorem is about localization maps from one additive commutative monoid to another. Specifically, for any additive commutative monoids `M` and `N`, a localization map `f` from `M` to `N`, elements `x₁` and `x₂` in `M`, and an element `y` in the submonoid `S` of `M`, the result of applying `f` to `x₁` and then adding the result of applying the localization map creation function `mk'` to `f`, `x₂`, and `y`, is equal to the result of applying `mk'` to `f`, the sum of `x₁` and `x₂`, and `y`. Expressed more compactly, for all `f`, `x₁`, `x₂`, and `y` as above, we have `f(x₁) + mk'(f, x₂, y) = mk'(f, x₁ + x₂, y)`. This theorem effectively expresses the distributivity of the localization map over the addition operation in the original monoid.
More concisely: Given additive commutative monoids M and N, a localization map f from M to N, and elements x₁, x₂, and y in M, the localization of the sum x₁ + x₂ under f is equal to the sum of the localizations of x₁ and x₂ under f and the localization of y. That is, f(x₁ + x₂) = mk'(f, x₁, y) + mk'(f, x₂, y).
|
AddSubmonoid.LocalizationMap.comp_eq_of_eq
theorem AddSubmonoid.LocalizationMap.comp_eq_of_eq :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
{P : Type u_3} [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} {T : AddSubmonoid P}
{Q : Type u_4} [inst_3 : AddCommMonoid Q],
(∀ (y : ↥S), g ↑y ∈ T) →
∀ (k : T.LocalizationMap Q) {x y : M}, f.toMap x = f.toMap y → k.toMap (g x) = k.toMap (g y)
The theorem `AddSubmonoid.LocalizationMap.comp_eq_of_eq` asserts that given additive commutative monoids `M, N, P, Q` and localization maps `f : M →+ N` and `k : P →+ Q` for submonoids `S` of `M` and `T` of `P` respectively, as well as a map `g : M →+ P` such that the image of `S` under `g` is a subset of `T`, if `f` maps two elements `x, y` of `M` to the same element in `N`, then `k` maps `g(x)` and `g(y)` to the same element in `Q`.
More concisely: If `f : M -> N` is a localization map of additive commutative monoids `M` and `N`, `k : P -> Q` is another localization map of additive commutative monoids `P` and `Q`, `S` is a submonoid of `M`, `T` is a submonoid of `P`, `g : M -> P` is a map with `S` subset of `T`, and `x, y` are elements of `M` with `f(x) = f(y)`, then `k(g(x)) = k(g(y))`.
|
Submonoid.LocalizationMap.map_mul_left
theorem Submonoid.LocalizationMap.map_mul_left :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
[inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} {T : Submonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T)
{Q : Type u_4} [inst_3 : CommMonoid Q] {k : T.LocalizationMap Q} (z : N),
k.toMap (g ↑(f.sec z).2) * (f.map hy k) z = k.toMap (g (f.sec z).1)
This theorem states that for given localizations maps `f` and `k` that map from monoids `M` and `P` to monoids `N` and `Q`, respectively, for submonoids `S` and `T`, if a commutative monoid homomorphism `g` from `M` to `P` induces another map from `N` to `Q`, then for any `z` in `N`, the product of mapping `g` on an element from `S` (that is related to `z` via `f`) and applying the induced map on `z` equals to applying `k` on the result of mapping `g` on another element in `M` (also related to `z` via `f`). Here, the elements from `M` and `S` are such that `z` times the image of `S` element under `f` equals to the image of `M` element under `f`.
More concisely: Given commutative monoid homomorphisms $f:\ M\to P$ and $k:\ N\to Q$, if for some elements $x\in M$ and $z\in N$ with $z\cdot f(S) = f(M)$, then $(g(x)\cdot k(z)) = k(g(y))$ for any $y\in M$ related to $z$ via $f$, where $g:\ M\to P$ is the homomorphism inducing $k:\ N\to Q$.
|
Submonoid.LocalizationMap.mk'_self'
theorem Submonoid.LocalizationMap.mk'_self' :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
(f : S.LocalizationMap N) (y : ↥S), f.mk' (↑y) y = 1
The theorem `Submonoid.LocalizationMap.mk'_self'` states that for any commutative monoid `M`, any submonoid `S` of `M`, any commutative monoid `N`, any localization map `f` from `S` to `N`, and any element `y` of `S`, if we use the localization map `f` on the pair `(y, y)`, where `y` is considered in `M` and `S` respectively, then the result is the multiplicative identity of `N`, that is, one. This is essentially checking a property of the localization map where an element and its localization to `N` are equivalent in the localization.
More concisely: For any commutative monoids M, N, submonoid S of M, localization map f from S to N, and element y in S, the localization of the pair (y, y) under f equals the multiplicative identity of N.
|
AddSubmonoid.LocalizationMap.neg_inj
theorem AddSubmonoid.LocalizationMap.neg_inj :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
{f : M →+ N} (hf : ∀ (y : ↥S), IsAddUnit (f ↑y)) {y z : ↥S},
-(IsAddUnit.liftRight (f.restrict S) hf) y = -(IsAddUnit.liftRight (f.restrict S) hf) z → f ↑y = f ↑z
The theorem `AddSubmonoid.LocalizationMap.neg_inj` states that given an additive monoid homomorphism `f : M →+ N` and a submonoid `S` of `M` such that the image of `S` under `f` is contained within the additive units of `N`, then for any two elements `y` and `z` in `S`, if the negatives of their images under the lifted homomorphism (to additive units of `N`) are equal, then their images under the original homomorphism `f` are also equal. In mathematical terms, if `- (f y) = - (f z)` then `f y = f z`.
More concisely: Given an additive monoid homomorphism `f : M -> N` and a submonoid `S` of `M` with `f S` contained in the additive units of `N`, if `- (fy) = - (fz)` for any `y, z in S`, then `fy = fz`.
|
Localization.one_def
theorem Localization.one_def : ∀ {M : Type u_4} [inst : CommMonoid M] (S : Submonoid M), Localization.one S = One.one
This theorem states that for any type `M` which is a commutative monoid, and for any submonoid `S` of `M`, the identity element of the localization of `S` is equal to the identity element of the underlying set. In other words, the identity of the localization of a submonoid is the same as the identity of the set itself. This identity element in both cases is represented as `⟨1, 1⟩`. So, regardless of the specific submonoid `S` or the exact type `M`, the identity for any Localization is always the same as the identity for the set.
More concisely: For any commutative monoid M and its submonoid S, the identity element of S's localization is equal to the identity element of M's underlying set.
|
Localization.mk_eq_monoidOf_mk'
theorem Localization.mk_eq_monoidOf_mk' :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M}, Localization.mk = (Localization.monoidOf S).mk' := by
sorry
The theorem `Localization.mk_eq_monoidOf_mk'` states that for any commutative monoid `M` and any submonoid `S` of `M`, the function `Localization.mk`, which sends a pair `(x, y)` where `x` is in `M` and `y` is in `S` to the equivalence class of `(x, y)` in the localization of `M` at `S`, is equal to the composite function `Submonoid.LocalizationMap.mk'` followed by `Localization.monoidOf S`. In other words, these two functions, which both map elements of `M` and `S` to the localization of `M` at `S`, are the same.
More concisely: The function `Localization.mk` from a pair of an element in a commutative monoid `M` and a submonoid `S` to their equivalence class in the localization of `M` at `S` is equal to the composition of `Localization.monoidOf S` and `Submonoid.LocalizationMap.mk'`.
|
AddLocalization.nsmul_def
theorem AddLocalization.nsmul_def :
∀ {M : Type u_4} [inst : AddCommMonoid M] (S : AddSubmonoid M), AddLocalization.nsmul S = AddMonoid.nsmul := by
sorry
The theorem `AddLocalization.nsmul_def` states that for any type `M` that forms an additive commutative monoid and any additive submonoid `S` of `M`, the operation of multiplication with a natural number in an `AddLocalization` is defined the same way as the multiplication by a natural number in the `AddMonoid`. In other words, the function `AddLocalization.nsmul S` which multiplies a natural number with an element of the `AddLocalization` of `S` is equivalent to the function `AddMonoid.nsmul`, which multiplies a natural number with an element of the `AddMonoid` of `M`.
More concisely: For any additive commutative monoid M and its submonoid S, the multiplication by a natural number in the AddLocalization of S is equivalent to the multiplication by a natural number in the AddMonoid of M.
|
Submonoid.LocalizationMap.lift_mul_right
theorem Submonoid.LocalizationMap.lift_mul_right :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
[inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} (hg : ∀ (y : ↥S), IsUnit (g ↑y)) (z : N),
(f.lift hg) z * g ↑(f.sec z).2 = g (f.sec z).1
This theorem is about the interaction of localization maps and commutative monoids. If we have a localization map `f` from a commutative monoid `M` to another commutative monoid `N`, associated with a submonoid `S` of `M`, and a commutative monoid map `g : M →* P` induces another map `f.lift hg : N →* P`, then for every element `z` in `N`, the equation `(f.lift hg) z * g y = g x` holds. Here, `x` is an element of `M` and `y` is an element of `S` such that multiplying `z` with the image of `y` under `f` equals to the image of `x` under `f`. This theorem is important in the study of localizations in commutative algebra.
More concisely: Given a localization map from a commutative monoid to another and a commutative monoid map, if the images of an element in the source monoid and an element in the submonoid under the map and the localization map respectively multiply to the image of another element in the source monoid under the map, then their images under the induced map on the target monoid and the original map on the source monoid multiply.
|
AddSubmonoid.LocalizationMap.map_add_right
theorem AddSubmonoid.LocalizationMap.map_add_right :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
{P : Type u_3} [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} {T : AddSubmonoid P}
(hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_4} [inst_3 : AddCommMonoid Q] {k : T.LocalizationMap Q} (z : N),
(f.map hy k) z + k.toMap (g ↑(f.sec z).2) = k.toMap (g (f.sec z).1)
The theorem `AddSubmonoid.LocalizationMap.map_add_right` states that given two localization maps `f : M →+ N` and `k : P →+ Q` for submonoids `S` and `T` respectively, if there's an additive commutative monoid homomorphism `g : M →+ P` such that it induces a map `f.map hy k : N →+ Q`, then for every element `z : N`, `f.map hy k z + k (g y) = k (g x)` holds. Here, `x : M, y ∈ S` are such that `z + f y = f x`. This theorem is essentially an identity that holds in the context of additive commutative monoids and localization maps.
More concisely: Given localization maps `f : M → N` and `k : P → Q` for submonoids `S` and `T`, if there's an additive commutative monoid homomorphism `g : M → P` such that `f.map g k` is defined, then for all `x in M` and `y in S` with `z + f y = f x`, it holds that `f.map g k z + k (g y) = k (g x)`.
|
Submonoid.LocalizationMap.lift_mul_left
theorem Submonoid.LocalizationMap.lift_mul_left :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
[inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} (hg : ∀ (y : ↥S), IsUnit (g ↑y)) (z : N),
g ↑(f.sec z).2 * (f.lift hg) z = g (f.sec z).1
This theorem is about a localization map and its properties. Let `M`, `N`, and `P` be commutative monoids. Given a localization map `f : M →* N` for a submonoid `S` of `M`, and a commutative monoid map `g : M →* P` that induces another map `f.lift hg : N →* P`, then for any element `z : N`, the equation `g y * f.lift hg z = g x` holds. Here `x : M` and `y` is an element of `S` such that `z * f y = f x`. The assumption is that for each `y` in `S`, `g y` is a unit in the monoid.
More concisely: Given a localization map `f : M →* N` for a submonoid `S` of `commutative monoid M`, a commutative monoid map `g : M →* P`, and `z : N` such that `z * f(s) = f(x)` for some `s in S` with `g(s)` a unit in `P`, then `g(x) = g(s) * f.lift(hg)(z)`.
|
Submonoid.LocalizationMap.subsingleton
theorem Submonoid.LocalizationMap.subsingleton :
∀ {M : Type u_1} [inst : CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoidWithZero N],
S.LocalizationMap N → 0 ∈ S → Subsingleton N
The theorem `Submonoid.LocalizationMap.subsingleton` states that if a set `S` of the type `M` (where `M` is a commutative monoid with zero) contains the element `0`, then the localization of `M` at `S` is a trivial (or singleton) set. This theorem applies to any `M` and `N` that are both commutative monoids with zero, and any localization map from `M` to `N` associated with the submonoid `S`.
More concisely: If a commutative monoid with zero `M` contains its zero element `0`, then the localization of `M` at the submonoid generated by `0` is a singleton.
|
Submonoid.LocalizationMap.exists_of_sec_mk'
theorem Submonoid.LocalizationMap.exists_of_sec_mk' :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
(f : S.LocalizationMap N) (x : M) (y : ↥S),
∃ c, ↑c * (↑(f.sec (f.mk' x y)).2 * x) = ↑c * (↑y * (f.sec (f.mk' x y)).1)
This theorem states that given a Localization map `f : M →* N` for a submonoid `S ⊆ M`, for all elements `x₁ : M` and `y₁` in `S`, if there exist elements `x₂ : M, y₂ ∈ S` such that the product of `f x₁`, the multiplicative inverse of `f y₁`, and `f y₂` equals `f x₂`, then there exists an element `c` in `S` such that the product of `x₁`, `y₂`, and `c` equals the product of `x₂`, `y₁`, and `c`. In other words, this theorem guarantees the existence of an element in the submonoid that makes the two expressions equal when multiplying with it.
More concisely: Given a Localization map `f : M →* N` for a submonoid `S ⊆ M`, if `x₁, x₂, y₁, y₂ ∈ S` satisfy `f x₁ * f (y₁^(-1)) * f y₂ = f x₂`, then there exists `c ∈ S` such that `x₁ * y₂ * c = x₂ * y₁ * c`.
|
Submonoid.LocalizationMap.mul_inv
theorem Submonoid.LocalizationMap.mul_inv :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {f : M →* N}
(h : ∀ (y : ↥S), IsUnit (f ↑y)) {x₁ x₂ : M} {y₁ y₂ : ↥S},
f x₁ * ↑((IsUnit.liftRight (f.restrict S) h) y₁)⁻¹ = f x₂ * ↑((IsUnit.liftRight (f.restrict S) h) y₂)⁻¹ ↔
f (x₁ * ↑y₂) = f (x₂ * ↑y₁)
This theorem states that for a given commutative monoid `M`, a submonoid `S` of `M`, and a monoid homomorphism `f` from `M` to another commutative monoid `N` such that `f` maps every element of `S` to a unit of `N`, the following holds true for all elements `x₁` and `x₂` of `M` and `y₁`, `y₂` of `S`: The multiplication of `f(x₁)` and the multiplicative inverse of `f(y₁)` is equal to the multiplication of `f(x₂)` and the multiplicative inverse of `f(y₂)` if and only if `f` of the multiplication of `x₁` and `y₂` is equal to `f` of the multiplication of `x₂` and `y₁`. In other words, it establishes an equivalence between two expressions involving the homomorphism `f` and the multiplicative structure of the monoids `M` and `N`.
More concisely: For a commutative monoid homomorphism `f` from a commutative monoid `M` to another commutative monoid `N` that maps every element of a submonoid `S` of `M` to a unit of `N`, `f(x₁ * y₁) = f(x₂ * y₂)` if and only if `f(x₁) * f(y₁⁻¹) = f(x₂) * f(y₂⁻¹)`, where `*` denotes multiplication and `⁻¹` denotes the multiplicative inverse, for all `x₁, x₂ ∈ M` and `y₁, y₂ ∈ S`.
|
AddSubmonoid.LocalizationMap.ext
theorem AddSubmonoid.LocalizationMap.ext :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
{f g : S.LocalizationMap N}, (∀ (x : M), f.toMap x = g.toMap x) → f = g
The theorem `AddSubmonoid.LocalizationMap.ext` states that for any two localization maps `f` and `g` from an additive submonoid `S` of an additive commutative monoid `M` to an additive commutative monoid `N`, if the two maps are equal when applied to any element `x` from `M` (i.e., `f(x) = g(x)` for all `x` in `M`), then the two localization maps `f` and `g` are identical. In other words, the theorem provides a criterion for proving the equality of two localization maps based on their action on elements of the monoid `M`.
More concisely: If two localization maps from an additive submonoid of an additive commutative monoid to an additive commutative monoid agree on all elements of the monoid, then they are equal.
|
Submonoid.LocalizationMap.lift_id
theorem Submonoid.LocalizationMap.lift_id :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
(f : S.LocalizationMap N) (x : N), (f.lift ⋯) x = x
This theorem asserts that for any commutative monoid `M` with a submonoid `S`, and any other commutative monoid `N`, if `f` is a localization map from `S` to `N`, then the "lift" operation applied to `f` and any element `x` of `N` is equal to `x` itself. In other words, lifting the localization map `f` leaves any element of `N` unchanged. This theorem is about a certain property of the lifting operation in the context of localization of commutative monoids.
More concisely: Given a commutative monoid Homomorphism `f` from a submonoid `S` to `N` in commutative monoids, the lift operation applied to `f` and any element `x` in `N` equals `x` itself.
|
Localization.mk_eq_mk_iff
theorem Localization.mk_eq_mk_iff :
∀ {M : Type u_1} [inst : CommMonoid 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)
The theorem `Localization.mk_eq_mk_iff` states that for any commutative monoid `M` and any submonoid `S` of `M`, and any elements `a, c` of `M` and `b, d` of `S`, the equivalence classes of `(a, b)` and `(c, d)` in the localization of `M` at `S` are equal if and only if `(a, b)` and `(c, d)` are related by the congruence relation `Localization.r S`. This congruence relation is defined as the smallest relation such that `(1, 1)` is equivalent to `(y, y)` for all `y` in `S`, and for any other such relation on `M × S`, the relation `Localization.r S` implies it.
More concisely: For any commutative monoid M and submonoid S, the equivalence classes of (a, b) and (c, d) in the localization of M at S are equal if and only if (a, b) and (c, d) are related by the congruence relation Localization.r S.
|
Submonoid.LocalizationMap.comp_eq_of_eq
theorem Submonoid.LocalizationMap.comp_eq_of_eq :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
[inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} {T : Submonoid P} {Q : Type u_4}
[inst_3 : CommMonoid Q],
(∀ (y : ↥S), g ↑y ∈ T) →
∀ (k : T.LocalizationMap Q) {x y : M}, f.toMap x = f.toMap y → k.toMap (g x) = k.toMap (g y)
This theorem asserts that given two commutative monoids `M` and `P`, with submonoids `S` and `T` respectively, and two localization maps `f : M → N` & `k : P → Q`, along with a map `g : M → P` such that `g(S)` is a subset of `T`. If for any two elements `x` and `y` of `M`, `f(x)` is equal to `f(y)`, then `k(g(x))` is also equal to `k(g(y))`. In other words, if two elements map to the same place under `f`, they also map to the same place under the composition of `k` and `g`.
More concisely: Given commutative monoids `M`, `P`, submonoids `S` and `T`, localization maps `f : M -> N` and `k : P -> Q`, and a map `g : M -> P` with `g(S)` subset of `T`, if `f` maps equal elements to equal images and `g(x)` is in `T` for all `x` in `M`, then `k(g(x))` maps equal elements in `M` to equal images.
|
AddSubmonoid.LocalizationMap.neg_unique
theorem AddSubmonoid.LocalizationMap.neg_unique :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
{f : M →+ N} (h : ∀ (y : ↥S), IsAddUnit (f ↑y)) {y : ↥S} {z : N},
f ↑y + z = 0 → ↑(-(IsAddUnit.liftRight (f.restrict S) h) y) = z
The theorem states that for a given additive monoid homomorphism `f` from `M` to `N` and a submonoid `S` of `M` such that the image of `S` under `f` maps to the additive units of `N`, for every element `y` in `S`, the negative of `f(y)` is unique. In other words, if we have an element `z` in `N` such that `f(y) + z = 0`, then `z` is equal to the negative of the image of `y` in the additive units of `N` obtained by lifting `f` from `S` to the additive units of `N`.
More concisely: Given an additive monoid homomorphism `f` from `M` to `N` and a submonoid `S` of `M` such that the image of `S` under `f` generates the additive units of `N`, for every `y` in `S`, there exists a unique `z` in `N` such that `f(y) + z = 0`.
|
AddLocalization.mk_eq_mk_iff
theorem AddLocalization.mk_eq_mk_iff :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {a c : M} {b d : ↥S},
AddLocalization.mk a b = AddLocalization.mk c d ↔ (AddLocalization.r S) (a, b) (c, d)
The theorem `AddLocalization.mk_eq_mk_iff` states that for any type `M` that is an instance of `AddCommMonoid`, any `AddSubmonoid` `S` of `M`, and any elements `a` and `c` of `M` and `b` and `d` of `S`, the equality of the localization of `a` at `b` and the localization of `c` at `d` is equivalent to the congruence of the pair `(a, b)` and the pair `(c, d)` under the relation `AddLocalization.r S`. In other words, two localized elements of an additive commutative monoid are equal if and only if their corresponding pairs in the original monoid are congruent under the localization relation.
More concisely: For any additive commutative monoid `M` with submonoid `S`, and elements `a`, `c` of `M` and `b` of `d` of `S`, the localization of `a` at `b` equals the localization of `c` at `d` if and only if `(a, b)` and `(c, d)` are congruent under `AddLocalization.r S`.
|
Mathlib.GroupTheory.MonoidLocalization._auxLemma.12
theorem Mathlib.GroupTheory.MonoidLocalization._auxLemma.12 :
∀ {α : Type u_1} [inst : OrderedCancelCommMonoid α] {s : Submonoid α} {a₁ b₁ : α} {a₂ b₂ : ↥s},
(Localization.mk a₁ a₂ ≤ Localization.mk b₁ b₂) = (↑b₂ * a₁ ≤ ↑a₂ * b₁)
This theorem, named `Mathlib.GroupTheory.MonoidLocalization._auxLemma.12`, expresses an important property relating to localizations of a commutative monoid. Specifically, for any ordered cancelable commutative monoid `α` and any submonoid `s` of `α`, it states that given any four elements `a₁`, `b₁` from `α` and `a₂`, `b₂` from `s`, the inequality `Localization.mk a₁ a₂ ≤ Localization.mk b₁ b₂` holds if and only if the inequality `↑b₂ * a₁ ≤ ↑a₂ * b₁` holds. Here, `Localization.mk` is a function that maps elements `x : M` and `y ∈ S` to the equivalence class `[x, y]` in the localization of `M` at `S`, and `↑x` denotes the embedding of an element `x` from the submonoid `s` into the monoid `α`.
More concisely: For any ordered cancelable commutative monoid `α` and submonoid `s`, the localization `[a₁, a₂] ≤ [b₁, b₂]` in the quotient monoid of `α` at `s` if and only if `↑a₂ * a₁ ≤ ↑a₂ * b₁` in `α`.
|
Submonoid.LocalizationMap.mk'_sec
theorem Submonoid.LocalizationMap.mk'_sec :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
(f : S.LocalizationMap N) (z : N), f.mk' (f.sec z).1 (f.sec z).2 = z
This theorem states that for a given localization map `f` from a commutative monoid `M` to a commutative monoid `N`, corresponding to a submonoid `S` of `M`, for every element `z` of `N`, there exist elements `x` in `M` and `y` in `S` such that `z * f y = f x`. In this case, the resulting value of `f x * (f y)⁻¹` will be `z`. This theorem ensures that the process of localization is reversible for any `z` in the codomain `N`.
More concisely: For every localization map from a commutative monoid to another and any element in the codomain, there exist preimages in the domain such that their product through the map equals the given element, and their quotients invert the image under the map.
|
AddSubmonoid.LocalizationMap.lift_add_right
theorem AddSubmonoid.LocalizationMap.lift_add_right :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
{P : Type u_3} [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P}
(hg : ∀ (y : ↥S), IsAddUnit (g ↑y)) (z : N), (f.lift hg) z + g ↑(f.sec z).2 = g (f.sec z).1
The theorem states that for any commutative monoid `M`, its submonoid `S`, a localization map `f` from `M` to another commutative monoid `N`, and a map `g` from `M` to a third commutative monoid `P` which is compatible with `f` (in the sense that it induces a map `f.lift hg` from `N` to `P`), the following holds for any `z` in `N`: the sum of `f.lift hg z` and `g` applied to the second element in `S` related to `z` through `f`, is equal to `g` applied to the first element in `M` related to `z` through `f`. Here, `f.sec z` is a pair `(x, y)` such that `x` is in `M`, `y` is in `S`, and `z + f(y)` equals `f(x)`.
More concisely: For any commutative monoids `M`, `N`, `P`, a commutative monoid homomorphism `f: M → N`, a submonoid `S` of `M`, and a map `g: M → P` compatible with `f`, the sum of `f.lift hg(z)` and `g(y)` equals `g(x)`, where `(x, y) = f.sec z` with `x ∈ M`, `y ∈ S`, and `z + f(y) = f(x)`.
|
AddSubmonoid.LocalizationMap.lift_of_comp
theorem AddSubmonoid.LocalizationMap.lift_of_comp :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
{P : Type u_3} [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) (j : N →+ P), f.lift ⋯ = j
This theorem, `AddSubmonoid.LocalizationMap.lift_of_comp`, stipulates that for any types `M`, `N`, and `P`, where `M` and `N` are additive commutative monoids and `S` is a submonoid of `M`, if we have a localization map `f` from `S` to `N` and an additive map `j` from `N` to `P`, then the composition of localization lifting of `f` with `j` equals to `j`. This is a property of localization in the context of additive monoids.
More concisely: Given additive commutative monoids M, N, and P, a submonoid S of M, a localization map f from S to N, and an additive map j from N to P, we have f.lift (j) = j.
|
Submonoid.LocalizationMap.map_comp_map
theorem Submonoid.LocalizationMap.map_comp_map :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
[inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} {T : Submonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T)
{Q : Type u_4} [inst_3 : CommMonoid Q] {k : T.LocalizationMap Q} {A : Type u_5} [inst_4 : CommMonoid A]
{U : Submonoid A} {R : Type u_6} [inst_5 : CommMonoid R] (j : U.LocalizationMap R) {l : P →* A}
(hl : ∀ (w : ↥T), l ↑w ∈ U), (k.map hl j).comp (f.map hy k) = f.map ⋯ j
This theorem is about the composition of induced maps in the context of localizations of commutative monoids. It states that if you have homomorphisms `g : M →* P` and `l : P →* A` in `CommMonoid`, which induce maps of localizations, then the composition of these induced maps is equal to the map of localizations induced by the composition `l ∘ g`. In other words, the order of map composition is not changed when maps are transformed into maps of localizations. This is under the condition that for every element of the submonoids `S` and `T`, `g` maps elements of `S` into `T` and `l` maps elements of `T` into `U`.
More concisely: Given homomorphisms `g : M →* P` and `l : P →* A` in a commutative monoid such that `g(S) ⊆ T` and `l(T) ⊆ U` for some submonoids `S` and `T` of `M` and `P`, respectively, the induced maps of localizations `l∘g : M/S → A/U` are equal to the composition of the induced maps `g∘l : M/S → P/T → A/U`.
|
Submonoid.LocalizationMap.eq
theorem Submonoid.LocalizationMap.eq :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
(f : S.LocalizationMap N) {a₁ b₁ : M} {a₂ b₂ : ↥S},
f.mk' a₁ a₂ = f.mk' b₁ b₂ ↔ ∃ c, ↑c * (↑b₂ * a₁) = ↑c * (↑a₂ * b₁)
This theorem states that, given a commutative monoid `M`, a submonoid `S` of `M`, another commutative monoid `N`, and a localization map `f` from `S` to `N`, for any elements `a₁, b₁` in `M` and `a₂, b₂` in `S`, the result of applying the defined function `Submonoid.LocalizationMap.mk'` on `a₁, a₂` equals the result of applying the same function `Submonoid.LocalizationMap.mk'` on `b₁, b₂` if and only if there exists an element `c` in `S` such that the product of `c` and the product of `b₂` and `a₁` equals the product of `c` and the product of `a₂` and `b₁`. In mathematical terms, we have `f(a₁) / f(a₂) = f(b₁) / f(b₂)` if and only if there exists `c` in `S` such that `c * b₂ * a₁ = c * a₂ * b₁`.
More concisely: Given commutative monoids M, a submonoid S, a localization map f from S to another commutative monoid N, and elements a₁, a₂, b₁, b₂ in S, the localization map evaluations f(a₁) and f(a₂) have the same quotient if and only if there exists an element c in S such that b₁ a₁ and a₂ b₂ have the same product as c² in S.
|
Localization.smul_mk
theorem Localization.smul_mk :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {R : Type u_4} [inst_1 : SMul R M]
[inst_2 : IsScalarTower R M M] (c : R) (a : M) (b : ↥S), c • Localization.mk a b = Localization.mk (c • a) b
The theorem `Localization.smul_mk` states that for any commutative monoid `M`, a submonoid `S` of `M`, a scalar multiplication operation `SMul` on `M` by a scalar `R`, and a scalar tower structure `IsScalarTower` on `M` (which implies that the scalar multiplication on `M` is associative), for any scalar `c` from `R`, any element `a` from `M`, and any element `b` from `S`, the scalar multiplication of the localization of `a` and `b` by `c` is equivalent to the localization of the scalar multiplication of `a` by `c` and `b`. In mathematical terms, this theorem says if we have a localization $(a,b)$, and we scalar multiply the entire localization by a scalar `c`, we get the same result as if we had just multiplied `a` by `c`.
More concisely: For any commutative monoid `M` with a submonoid `S`, scalar multiplication `SMul` by a scalar `R`, and an associative scalar tower structure `IsScalarTower` on `M`, the localization of `a * c` and `b` is equal to the localization of `a` multiplied by `c` for all `a` in `M` and `b` in `S`.
|
AddLocalization.zero_def
theorem AddLocalization.zero_def :
∀ {M : Type u_4} [inst : AddCommMonoid M] (S : AddSubmonoid M), AddLocalization.zero S = Zero.zero
The theorem `AddLocalization.zero_def` states that for any type `M` that is an instance of the additive commutative monoid, and for any additive submonoid `S` of `M`, the zero element of the additive localization of `S` is the same as the zero element of the underlying type. This means that the identity element in this additive localization context, represented as the pair `⟨0, 0⟩`, is equivalent to the zero of the underlying structure. This definition should not be confused with the zero of ring localization, which is defined as `⟨0, 1⟩`.
More concisely: For any additive commutative monoid M and its submonoid S, the zero element of the additive localization of S is identical to the zero element of M.
|
Localization.induction_on₂
theorem Localization.induction_on₂ :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {p : Localization S → Localization S → Prop}
(x y : Localization S), (∀ (x y : M × ↥S), p (Localization.mk x.1 x.2) (Localization.mk y.1 y.2)) → p x y
The theorem `Localization.induction_on₂` states that for any commutative monoid `M`, any submonoid `S` of `M`, and any binary predicate `p` on the localization of `M` at `S`, if `p` holds for all pairs of elements from `M` and `S` when mapped to the localization using the `Localization.mk` function, then `p` holds for all pairs of elements in the localization of `M` at `S`. In mathematical terms, given `x, y` as pairs in the localization, if `p` is true for all pairs `(x', y')` in `M × S` such that `Localization.mk x'.1 x'.2` and `Localization.mk y'.1 y'.2` correspond to `x, y`, respectively, then `p` is true for `x, y` in the localization.
More concisely: If a binary predicate holds for all pairs in a commutative monoid and their images under localization at a submonoid, then it holds for the corresponding pairs in the localization.
|
Submonoid.LocalizationMap.mul_inv_left
theorem Submonoid.LocalizationMap.mul_inv_left :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {f : M →* N}
(h : ∀ (y : ↥S), IsUnit (f ↑y)) (y : ↥S) (w z : N),
w * ↑((IsUnit.liftRight (f.restrict S) h) y)⁻¹ = z ↔ w = f ↑y * z
This theorem states that for a given monoid homomorphism `f` mapping from monoid `M` to `N`, and a submonoid `S` of `M` such that the image of `S` under `f` is contained in `Nˣ` (the group of units in `N`), for all `w, z` in `N` and `y` in `S`, the equality `w * (f(y))⁻¹ = z` holds if and only if `w = f(y) * z`. This theorem allows us to simplify expressions involving the inverse of the image of an element under a monoid homomorphism.
More concisely: For a monoid homomorphism `f` from monoid `M` to `N` with image of a submonoid `S` of `M` contained in `Nˣ`, the equation `w * (f(y))⁻¹ = z` holds if and only if `w = f(y) * z` for all `w, z` in `N` and `y` in `S`.
|
AddSubmonoid.LocalizationMap.lift_left_inverse
theorem AddSubmonoid.LocalizationMap.lift_left_inverse :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
{P : Type u_3} [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {k : S.LocalizationMap P} (z : N),
(k.lift ⋯) ((f.lift ⋯) z) = z
This theorem states that for any two Localization maps `f : M →+ N` and `k : M →+ P`, where `M` is an additive commutative monoid and `S` is a submonoid of `M`, the homomorphism from `P` to `N` induced by `f` is a left inverse to the homomorphism from `N` to `P` induced by `k`. In other words, for any element `z` of `N`, applying the `lift` function of `k` to the result of applying the `lift` function of `f` to `z` will yield `z` again. This property is fundamental in the theory of Localization in algebra.
More concisely: Given additive commutative monoids M, N, and P, and submonoid S of M, for any homomorphisms f : M →+ N and k : M →+ P with respect to S, the induced homomorphisms from P to N via f and from N to P via k are left inverses of each other.
|
Localization.r_iff_exists
theorem Localization.r_iff_exists :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {x y : M × ↥S},
(Localization.r S) x y ↔ ∃ c, ↑c * (↑y.2 * x.1) = ↑c * (↑x.2 * y.1)
This theorem states that for any commutative monoid `M`, a submonoid `S` of `M`, and any pairs `x` and `y` from `M` and `S`, `(Localization.r S) x y` is true if and only if there exists a `c` in `S` such that the product of `c`, the second element of `y` and the first element of `x` equals the product of `c`, the second element of `x` and the first element of `y`. The `Localization.r S` relation is a specific congruence relation related to the localization of the commutative monoid `M` at the submonoid `S`. This theorem forms the foundation of the notion of "equivalence" in the localization of a commutative monoid at a submonoid.
More concisely: For any commutative monoid `M`, submonoid `S`, and elements `x, y` in `M`, `Localization.r S x y` holds if and only if there exists `c` in `S` such that `c * y.2 * x.1 = c * x.2 * y.1`.
|
AddLocalization.induction_on
theorem AddLocalization.induction_on :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {p : AddLocalization S → Prop}
(x : AddLocalization S), (∀ (y : M × ↥S), p (AddLocalization.mk y.1 y.2)) → p x
This theorem states that, given an additive commutative monoid `M`, a submonoid `S` of `M`, a property `p` that applies to elements of the localization of `M` at `S`, and an element `x` of this localization, if every pair `(y.1, y.2)` where `y.1` belongs to `M` and `y.2` belongs to `S` satisfies this property when passed to `AddLocalization.mk`, then the property `p` is satisfied by `x`. Essentially, this theorem provides an induction principle for reasoning about all elements of the localization of a commutative monoid at one of its submonoids.
More concisely: Given an additive commutative monoid `M`, a submonoid `S`, and a property `p`, if for all `y` with `y.1` in `M` and `y.2` in `S`, `p(AddLocalization.mk y)` holds, then `p(x)` holds for every element `x` in the localization of `M` at `S`.
|
Localization.mul_def
theorem Localization.mul_def : ∀ {M : Type u_4} [inst : CommMonoid M] (S : Submonoid M), Localization.mul S = Mul.mul
The theorem `Localization.mul_def` states that for any type `M` that forms a commutative monoid and any submonoid `S` of `M`, the multiplication operation in the localization of `M` at `S` is the same as the built-in multiplication operation for the type of `Localization S`. In other words, the multiplication of elements in the localized version of the monoid (represented as pairs of elements from `M` and `S`) is equivalent to the usual multiplication of elements in the monoid, which is represented as `⟨a, b⟩ * ⟨c, d⟩ = ⟨a * c, b * d⟩`.
More concisely: In the localization of a commutative monoid `M` at a submonoid `S`, the multiplication operation is equal to the usual multiplication of elements represented as pairs `⟨a, s⟩` from `M x S`, that is, `⟨a, s⟩ * ⟨b, t⟩ = ⟨a * b, s * t⟩`.
|
Submonoid.LocalizationMap.lift_spec_mul
theorem Submonoid.LocalizationMap.lift_spec_mul :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
[inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} (hg : ∀ (y : ↥S), IsUnit (g ↑y)) (z : N) (w v : P),
(f.lift hg) z * w = v ↔ g (f.sec z).1 * w = g ↑(f.sec z).2 * v
This theorem states that for any given localization map `f`, mapping from a commutative monoid `M` to another commutative monoid `N` for a submonoid `S` in `M`, and a commutative monoid map `g` from `M` to a third commutative monoid `P` that induces a map `f.lift hg` from `N` to `P`, the following condition holds for all elements `z` in `N` and `v`, `w` in `P`: `(f.lift hg) z * w = v` if and only if `g (f.sec z).1 * w = g ↑(f.sec z).2 * v`, where `(f.sec z).1` is an element `x` of `M` and `(f.sec z).2` is an element `y` in `S` such that `z * f y = f x`. This essentially says that multiplication in the image of `g` is determined by multiplication in `P`, under the assumption that each element of `S` under `g` is a unit.
More concisely: Given a localization map `f` from a commutative monoid `M` to `N`, a submonoid `S` of `M`, and a commutative monoid map `g` from `M` to a third commutative monoid `P`, if for all `z` in `N` and `y` in `S` such that `z * f y = f x`, `(f.lift hg) z * w = v` if and only if `g x * w = g y * v`, then each element of `S` under `g` is a unit.
|
Submonoid.LocalizationMap.sec_spec'
theorem Submonoid.LocalizationMap.sec_spec' :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
{f : S.LocalizationMap N} (z : N), f.toMap (f.sec z).1 = f.toMap ↑(f.sec z).2 * z
The theorem `Submonoid.LocalizationMap.sec_spec'` states that for any types `M` and `N` that form commutative monoids, given a submonoid `S` of `M`, and a localization map `f` from `S` to `N`, for any element `z` of `N`, the value of the localization map `f` at the first component of `f.sec z` equals the product of the value of `f` at the "coerced" second component of `f.sec z` and `z`. In other words, if `(x, y)` is a pair such that `f x * (f y)⁻¹ = z` (which is the role of the `sec` function), then `f(x) = f(y) * z`.
More concisely: For any commutative monoids M and N, submonoid S of M, and localization map f from S to N, if x and y are in S with f(x) * f(y)^-1 = z, then f(x) = f(y) * z.
|
Mathlib.GroupTheory.MonoidLocalization._auxLemma.6
theorem Mathlib.GroupTheory.MonoidLocalization._auxLemma.6 :
∀ {M : Type u_1} [inst : CommMonoid 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)
This theorem states that for any commutative monoid `M` and any submonoid `S` of `M`, and for any elements `a`, `c` of `M` and `b`, `d` of `S`, the equality of two localizations `Localization.mk a b` and `Localization.mk c d` is equivalent to the congruence of the pairs `(a, b)` and `(c, d)` under the congruence relation `Localization.r S` defined on `M × S`. In other words, two localizations are equal if and only if their associated pairs are related by the specific congruence relation that characterizes the localization.
More concisely: For any commutative monoid `M` and submonoid `S`, two localizations `Localization.mk a b` and `Localization.mk c d` of `M` with respect to `S` are equal if and only if `(a, b)` and `(c, d)` are related by the congruence relation `Localization.r S` on `M × S`.
|
Submonoid.LocalizationMap.map_spec
theorem Submonoid.LocalizationMap.map_spec :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
[inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} {T : Submonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T)
{Q : Type u_4} [inst_3 : CommMonoid Q] {k : T.LocalizationMap Q} (z : N) (u : Q),
(f.map hy k) z = u ↔ k.toMap (g (f.sec z).1) = k.toMap (g ↑(f.sec z).2) * u
This theorem states that for given localization maps `f: M →* N` and `k: P →* Q` for submonoids `S` and `T`, respectively, if a commutative monoid homomorphism `g: M →* P` induces another map `f.map hy k: N →* Q`, then for any elements `z` in `N` and `u` in `Q`, `f.map hy k z = u` if and only if `k(g(x)) = k(g(y)) * u`. Here, `x` and `y` are elements in `M` and `S` respectively, such that the equality `z * f y = f x` holds.
More concisely: For commutative monoid homomorphisms $g: M \to P$ and localization maps $f: M \to_* N$ and $k: P \to_* Q$, if $g$ induces $f.map\_hy\ k: N \to_* Q$ and $z \in N$ and $u \in Q$ satisfy $z \cdot f(y) = f(x)$ for some $x, y \in M$ and $x \in S, y \in T$, then $f.map\_hy\ k(z) = u$ if and only if $k(g(x)) = k(g(y)) \cdot u$.
|
Submonoid.LocalizationWithZeroMap.leftCancelMulZero_of_le_isLeftRegular
theorem Submonoid.LocalizationWithZeroMap.leftCancelMulZero_of_le_isLeftRegular :
∀ {M : Type u_1} [inst : CommMonoidWithZero M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoidWithZero N],
S.LocalizationWithZeroMap N →
∀ [inst_2 : IsLeftCancelMulZero M], (∀ ⦃x : M⦄, x ∈ S → IsLeftRegular x) → IsLeftCancelMulZero N
The theorem `Submonoid.LocalizationWithZeroMap.leftCancelMulZero_of_le_isLeftRegular` states that for any given localization map `f` from a multiplicative monoid `M` to another monoid `N` with respect to a submonoid `S` of `M`, if `M` is a left cancellative monoid with zero and every element of `S` is left regular (meaning that left multiplication by any element of `S` is an injective function), then `N` is also a left cancellative monoid with zero. In other words, the property of being a left cancellative monoid with zero is preserved under localization by a map for a submonoid whose elements have the left regular property.
More concisely: If `M` is a left cancellative monoid with zero and every element of the submonoid `S` of `M` is left regular, then the localization `N` of `M` with respect to `S` is also a left cancellative monoid with zero.
|
AddSubmonoid.LocalizationMap.exists_of_sec_mk'
theorem AddSubmonoid.LocalizationMap.exists_of_sec_mk' :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
(f : S.LocalizationMap N) (x : M) (y : ↥S),
∃ c, ↑c + (↑(f.sec (f.mk' x y)).2 + x) = ↑c + (↑y + (f.sec (f.mk' x y)).1)
The theorem `AddSubmonoid.LocalizationMap.exists_of_sec_mk'` states that for a given Localization map `f` from an additive commutative monoid `M` to another additive commutative monoid `N` with a specified submonoid `S` of `M`, for any `x` in `M` and `y` in `S`, if there exist elements `x₂` in `M` and `y₂` in `S` such that the sum of the difference of the images of `x₁` and `y₁` under `f` and the image of `y₂` under `f` equals to the image of `x₂` under `f`, then there exists an element `c` in `S` such that the sum of `x₁`, `y₂`, and `c` equals to the sum of `x₂`, `y₁`, and `c`.
More concisely: Given an additive commutative monoid homomorphism `f` from `M` to `N` and a submonoid `S` of `M`, if for all `x` in `M` and `y` in `S`, there exist `x₂` in `M` and `y₂` in `S` such that `f(x - y) + f(y₂) = f(x₂)`, then there exists `c` in `S` such that `x + y + c = x₂ + y₁ + c`.
|
Submonoid.LocalizationMap.ext
theorem Submonoid.LocalizationMap.ext :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
{f g : S.LocalizationMap N}, (∀ (x : M), f.toMap x = g.toMap x) → f = g
The theorem `Submonoid.LocalizationMap.ext` states that for any two localization maps `f` and `g` from a submonoid `S` of a commutative monoid `M` to another commutative monoid `N`, if for every element `x` in `M`, applying the function version of `f` to `x` yields the same result as applying the function version of `g` to `x`, then `f` and `g` are the same localization map. Here, `(Submonoid.LocalizationMap.toMap f) x` and `(Submonoid.LocalizationMap.toMap g) x` are the function versions of the localization maps `f` and `g` respectively.
More concisely: If for all `x` in a commutative monoid `M`, the function versions of localization maps `f` and `g` from a submonoid `S` of `M` to another commutative monoid `N` agree on `x`, then `f` and `g` are equal as localization maps.
|
Submonoid.LocalizationMap.ofMulEquivOfDom_id
theorem Submonoid.LocalizationMap.ofMulEquivOfDom_id :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
(f : S.LocalizationMap N), f.ofMulEquivOfDom ⋯ = f
This theorem, `Submonoid.LocalizationMap.ofMulEquivOfDom_id`, asserts a special case of the property `f ∘ id = f` in the context of localization maps in the context of commutative monoids. Specifically, given any commutative monoid `M`, a submonoid `S` of `M`, another commutative monoid `N`, and a localization map `f` from `S` to `N`, the result of applying the `ofMulEquivOfDom` function to `f` and the identity element, is equal to `f` itself.
More concisely: Given a commutative monoid `M`, a submonoid `S` of `M`, a commutative monoid `N`, and a localization map `f : S → N`, `ofMulEquivOfDom f id = f`.
|
AddLocalization.mk_add
theorem AddLocalization.mk_add :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} (a c : M) (b d : ↥S),
AddLocalization.mk a b + AddLocalization.mk c d = AddLocalization.mk (a + c) (b + d)
This theorem, `AddLocalization.mk_add`, states that for any given additive commutative monoid `M` and a submonoid `S`, if you have two pairs of elements `(a, b)` and `(c, d)` where `a` and `c` are from `M` and `b` and `d` are from `S`, then the sum of the equivalence classes of these two pairs in the localization of `M` at `S`, denoted by `AddLocalization.mk a b + AddLocalization.mk c d`, is equal to the equivalence class of the pair `(a + c, b + d)` in the same localization. Here, `a + c` and `b + d` denote the sums in the monoid `M` and the submonoid `S` respectively.
More concisely: Given an additive commutative monoid `M` and a submonoid `S`, the localization of pairs of elements from `M` and `S` in `AddLocalization M S` satisfies `AddLocalization.mk a b + AddLocalization.mk c d = AddLocalization.mk (a + c) (b + d)`, where `a`, `b`, `c`, and `d` are elements from `M` and `S` respectively.
|
AddSubmonoid.LocalizationMap.add_neg_right
theorem AddSubmonoid.LocalizationMap.add_neg_right :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
{f : M →+ N} (h : ∀ (y : ↥S), IsAddUnit (f ↑y)) (y : ↥S) (w z : N),
z = w + ↑(-(IsAddUnit.liftRight (f.restrict S) h) y) ↔ z + f ↑y = w
This theorem states that for any additive commutative monoid `M`, a submonoid `S` of `M`, an additive commutative monoid `N`, and a monoid homomorphism `f` from `M` to `N` (written as `f : M →+ N`), such that the image of `S` under `f` lies within the additive units of `N`, the following holds: for any element `y` in `S` and any two elements `w` and `z` in `N`, `z` is equal to `w - f(y)` if and only if `z + f(y)` is equal to `w`.
In other words, one can switch between subtracting `f(y)` from `w` and adding `f(y)` to `z` without changing the equality. This theorem is a variant of the basic property of addition and subtraction in the context of additive units and homomorphisms.
More concisely: For any additive commutative monoids M, N, monoid homomorphism f : M ->+ N with image of a submonoid S of M in additive units of N, if y is in S and w, z are in N with w = z + f(y), then w = z - f(y).
|
AddSubmonoid.LocalizationMap.mk'_spec
theorem AddSubmonoid.LocalizationMap.mk'_spec :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
(f : S.LocalizationMap N) (x : M) (y : ↥S), f.mk' x y + f.toMap ↑y = f.toMap x
The theorem `AddSubmonoid.LocalizationMap.mk'_spec` states that for any given localization map `f` from an additive commutative monoid `M` to another `N` with respect to a submonoid `S` of `M`, and for any element `x` in `M` and `y` in `S`, the sum of the result of applying the function `mk'` on `f`, `x`, and `y` and the result of applying the function `toMap` on `f` and `y` is equal to the result of applying the function `toMap` on `f` and `x`. In mathematical terms, this can be written as `f(x - y) + f(y) = f(x)`, where `f` is the localization map.
More concisely: For any localization map `f` from an additive commutative monoid `M` to another `N` with respect to a submonoid `S` of `M`, and for all `x` in `M` and `y` in `S`, we have `f(x - y) = f(x) - f(y)`.
|
AddSubmonoid.LocalizationMap.map_comp_map
theorem AddSubmonoid.LocalizationMap.map_comp_map :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
{P : Type u_3} [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} {T : AddSubmonoid P}
(hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_4} [inst_3 : AddCommMonoid Q] {k : T.LocalizationMap Q} {A : Type u_5}
[inst_4 : AddCommMonoid A] {U : AddSubmonoid A} {R : Type u_6} [inst_5 : AddCommMonoid R]
(j : U.LocalizationMap R) {l : P →+ A} (hl : ∀ (w : ↥T), l ↑w ∈ U), (k.map hl j).comp (f.map hy k) = f.map ⋯ j
This theorem states that if we have homomorphisms between additive commutative monoids (`g : M →+ P, l : P →+ A`) that induce maps of localizations, then the composition of the induced maps is equal to the map of localizations induced by the composition of `l` and `g`. In other words, it preserves the structure of localizations under the composition of homomorphisms. This is a property that is generally expected from localization maps in a mathematical context as it demonstrates their compatibility with other types of morphisms.
More concisely: If homomorphisms `g : M →+ P` and `l : P →+ A` between additive commutative monoids induce localization maps, then `l ∘ g` induces the same localization map as the composition of `l` and `g` induced maps.
|
AddSubmonoid.LocalizationMap.mk'_sec
theorem AddSubmonoid.LocalizationMap.mk'_sec :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
(f : S.LocalizationMap N) (z : N), f.mk' (f.sec z).1 (f.sec z).2 = z
The theorem `AddSubmonoid.LocalizationMap.mk'_sec` states that for any given localization map `f` from a commutative addmonoid `M` to another commutative addmonoid `N` and a submonoid `S` of `M`, for any `z` in `N`, if there exist an element `x` in `M` and an element `y` in `S` such that `z` plus `f` applied to `y` equals `f` applied to `x`, then subtracting `f` applied to `y` from `f` applied to `x` equals `z`. This theorem essentially establishes a relationship for elements in the image of a localization map that are sums of elements in the original addmonoid and the image of the submonoid under the map.
More concisely: If `f` is a localization map from commutative addmonoid `M` to commutative addmonoid `N`, and `S` is a submonoid of `M`, then for all `z` in `N` such that there exist `x` in `M` and `y` in `S` with `z = f(x) + f(y)`, we have `f(x) - f(y) = z`.
|
Submonoid.LocalizationMap.lift_of_comp
theorem Submonoid.LocalizationMap.lift_of_comp :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
[inst_2 : CommMonoid P] (f : S.LocalizationMap N) (j : N →* P), f.lift ⋯ = j
This theorem states that for any commutative monoids `M`, `N`, and `P`, a given submonoid `S` of `M`, and a localization map `f` from `S` to `N`, there is a homomorphism `j` from `N` to `P` such that the lift of the localization map `f` equals `j`. Essentially, this theorem is about lifting operations in the context of localization of commutative monoids.
More concisely: Given a commutative monoid homomorphism `f` from a submonoid `S` of `M` to `N`, there exists a homomorphism `j` from `N` to `P` such that `f` is the restriction of `j` to `S`.
|
AddSubmonoid.LocalizationMap.lift_add_left
theorem AddSubmonoid.LocalizationMap.lift_add_left :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
{P : Type u_3} [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P}
(hg : ∀ (y : ↥S), IsAddUnit (g ↑y)) (z : N), g ↑(f.sec z).2 + (f.lift hg) z = g (f.sec z).1
This theorem states that given a Localization map `f` from an `AddCommMonoid` `M` to another `AddCommMonoid` `N` for a submonoid `S` of `M`, if there exists a map `g` from `M` to an `AddCommMonoid` `P` that induces another map `f.lift hg` from `N` to `P`, then for all elements `z` of `N`, we have an equality `g y + f.lift hg z = g x`, where `x` is an element of `M`, `y` is an element of the submonoid `S`, satisfying the condition `z + f y = f x`. Here, the function `f.sec` returns a pair `(x, y)` such that `z + f y = f x` for a given `z`, and `f.lift hg` is the induced map from `N` to `P`. The proposition `IsAddUnit a` means that there exists an additive unit `u` such that `u` is equal to `a`. The `AddCommMonoid` structure ensures that the operation of addition is commutative (i.e., `a + b = b + a` for all `a` and `b`).
More concisely: Given a Localization map `f` from an AddCommMonoid `M` to another AddCommMonoid `N` for a submonoid `S` of `M`, if there exists a map `g` from `M` to an AddCommMonoid `P` such that `f.lift (g . f.sec)` exists, then for all `z` in `N` with `z + f y = f x` for some `(x, y)` in `M`, we have `g x + f.lift (g . f.sec) z = g y`.
|
AddSubmonoid.LocalizationMap.lift_mk'
theorem AddSubmonoid.LocalizationMap.lift_mk' :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
{P : Type u_3} [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P}
(hg : ∀ (y : ↥S), IsAddUnit (g ↑y)) (x : M) (y : ↥S),
(f.lift hg) (f.mk' x y) = g x + ↑(-(IsAddUnit.liftRight (g.restrict S) hg) y)
This theorem states that given a localization map `f : M →+ N` for a submonoid `S ⊆ M`, and a homomorphism `g : M →+ P` of additively commutative monoids such that the image `g y` is invertible for every `y` in `S`, the induced homomorphism from `N` to `P` maps the difference of images `f x - f y` to the difference of images `g x - g y` for every `x` in `M` and `y` in `S`. In other words, this theorem shows that the mapping behaves well under the subtraction operation in the context of additive localization.
More concisely: Given a localization map `f : M →+ N` of a submonoid `S ⊆ M` and a homomorphism `g : M →+ P` with invertible images `g(S)`, the induced homomorphism `fⁱ : N →+ P` satisfies `fⁱ(fx - fy) = gx - gy` for all `x ∈ M` and `y ∈ S`.
|
AddLocalization.mk_eq_addMonoidOf_mk'
theorem AddLocalization.mk_eq_addMonoidOf_mk' :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M},
AddLocalization.mk = (AddLocalization.addMonoidOf S).mk'
The theorem `AddLocalization.mk_eq_addMonoidOf_mk'` states that for any additive commutative monoid `M` and any submonoid `S` of `M`, the function `AddLocalization.mk`, which takes an element of `M` and an element of `S` and sends them to their equivalence class in the localization of `M` at `S`, is equal to the function `AddSubmonoid.LocalizationMap.mk'` applied to the natural homomorphism `AddLocalization.addMonoidOf S`. This natural homomorphism sends an element of `M` to the equivalence class of `(x, 0)` in the localization of `M` at `S`. The theorem thereby associates the addition operation in the base monoid `M` with the addition operation in the localized monoid.
More concisely: The theorem `AddLocalization.mk_eq_addMonoidOf_mk` asserts that for any additive commutative monoid `M` and submonoid `S`, the functions `AddLocalization.mk` and `AddSubmonoid.LocalizationMap.mk'` defining addition in the localization of `M` at `S` agree, i.e., `AddLocalization.mk (x, y) = AddSubmonoid.LocalizationMap.mk' (AddLocalization.addMonoidOf S) (x, 0)` for all `x, y` in `M`.
|
AddSubmonoid.LocalizationMap.map_spec
theorem AddSubmonoid.LocalizationMap.map_spec :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
{P : Type u_3} [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} {T : AddSubmonoid P}
(hy : ∀ (y : ↥S), g ↑y ∈ T) {Q : Type u_4} [inst_3 : AddCommMonoid Q] {k : T.LocalizationMap Q} (z : N) (u : Q),
(f.map hy k) z = u ↔ k.toMap (g (f.sec z).1) = k.toMap (g ↑(f.sec z).2) + u
This theorem states that given two Localization maps `f : M →+ N` and `k : P →+ Q` for Submonoids `S` and `T` respectively, if an additive commutative monoid homomorphism `g : M →+ P` induces a third map `f.map hy k : N →+ Q`, then for all `z` in `N` and `u` in `Q`, `f.map hy k z` equals to `u` if and only if `k (g x)` equals to `k (g y) + u`, where `x` is an element of `M`, `y` is an element of `S` and `z + f y = f x`.
More concisely: Given additive commutative monoid homomorphisms `g : M → P` and localization maps `f : M →+ N` and `k : P →+ Q`, if `f.map (g) k(z) = u` for all `z in N` and some `x in M` with `z + f(x) = f(y)` for some `y in S`, then `k(g(x)) = k(g(y)) + u`.
|
Submonoid.LocalizationMap.lift_left_inverse
theorem Submonoid.LocalizationMap.lift_left_inverse :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
[inst_2 : CommMonoid P] (f : S.LocalizationMap N) {k : S.LocalizationMap P} (z : N),
(k.lift ⋯) ((f.lift ⋯) z) = z
The theorem `Submonoid.LocalizationMap.lift_left_inverse` states that for any commutative monoids `M`, `N`, and `P`, a given submonoid `S` of `M`, and given localization maps `f : M →* N` and `k : M →* P` for `S`, the homomorphism from `P` to `N` that is induced by `f` is the left inverse to the homomorphism from `N` to `P` induced by `k`. In other words, for any element `z` in `N`, applying the homomorphism `f.lift` to `z` and then applying the homomorphism `k.lift` to the result, we get back the original element `z`.
More concisely: For any commutative monoids M, N, and P, a submonoid S of M, and localization maps f : M →* N and k : M →* P for S, the homomorphism induced by f is the left inverse of the homomorphism induced by k, i.e., f.lift ∘ k.lift = id\_N.
|
Mathlib.GroupTheory.MonoidLocalization._auxAddLemma.12
theorem Mathlib.GroupTheory.MonoidLocalization._auxAddLemma.12 :
∀ {α : Type u_1} [inst : OrderedCancelAddCommMonoid α] {s : AddSubmonoid α} {a₁ b₁ : α} {a₂ b₂ : ↥s},
(AddLocalization.mk a₁ a₂ ≤ AddLocalization.mk b₁ b₂) = (↑b₂ + a₁ ≤ ↑a₂ + b₁)
This theorem states that for any ordered, cancellative, commutative monoid `α`, a submonoid `s` of `α`, and elements `a₁`, `b₁` from `α` and `a₂`, `b₂` from `s`, the inequality `AddLocalization.mk a₁ a₂ ≤ AddLocalization.mk b₁ b₂` holds if and only if the inequality `↑b₂ + a₁ ≤ ↑a₂ + b₁` holds. Here, `AddLocalization.mk a₁ a₂` and `AddLocalization.mk b₁ b₂` represent the equivalence classes in the localization of `α` at `s` of the pairs `(a₁, a₂)` and `(b₁, b₂)`, respectively, and `↑a₂` and `↑b₂` denote the elements of `α` that `a₂` and `b₂` correspond to.
More concisely: For any ordered, cancellative, commutative monoid `α`, submonoid `s`, and elements `a₁, a₂, b₁, b₂` in `α` with `(a₂, a₁)` and `(b₂, b₁)` in `s`, the inequality `AddLocalization.mk a₁ a₂ ≤ AddLocalization.mk b₁ b₂` holds if and only if the inequality `↑a₂ + a₁ ≤ ↑b₂ + b₁` holds, where `AddLocalization.mk` denotes the equivalence classes in the localization of `α` at `s`.
|
AddSubmonoid.LocalizationMap.sec_spec'
theorem AddSubmonoid.LocalizationMap.sec_spec' :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
{f : S.LocalizationMap N} (z : N), f.toMap (f.sec z).1 = f.toMap ↑(f.sec z).2 + z
This theorem states that for any additive commutative monoid `M`, a submonoid `S` of `M`, an additive commutative monoid `N`, and a localization map `f` from `S` to `N`, for any element `z` in `N`, the result of applying the localization map `f` to the first element of the pair resulting from the section function `sec` applied to `z` equals the result of adding `z` to the result of applying `f` to the lifted (or referenced) second element of the pair produced by `sec` on `z`. In effect, this theorem asserts a specific property of the section of a localization map in the context of additive commutative monoids.
More concisely: For any additive commutative monoids M, an additive commutative monoid N, a submonoid S of M, and a localization map f from S to N, for all elements z in N, we have f(sec z.fst) = sec z.snd + z.
|
Localization.ind
theorem Localization.ind :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {p : Localization S → Prop},
(∀ (y : M × ↥S), p (Localization.mk y.1 y.2)) → ∀ (x : Localization S), p x
The `Localization.ind` theorem states that for any commutative monoid `M` and any of its submonoids `S`, given a property `p` that applies to localized elements of `M`, if this property holds for every pair `(y.1, y.2)` where `y.1` is an element of the monoid `M` and `y.2` is an element of the submonoid `S` localized by `Localization.mk`, then this property `p` is valid for all elements `x` in the localization of `S`. In essence, this theorem allows for the induction over the elements of the localization of a commutive monoid at one of its submonoids.
More concisely: If a property `p` holds for all pairs of elements `(y.1, y.2)` with `y.1` in a commutative monoid `M` and `y.2` in a submonoid `S`, then `p` holds for all elements in the localization of `S` in `M`.
|
AddLocalization.mk_eq_addMonoidOf_mk'_apply
theorem AddLocalization.mk_eq_addMonoidOf_mk'_apply :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} (x : M) (y : ↥S),
AddLocalization.mk x y = (AddLocalization.addMonoidOf S).mk' x y
This theorem states that for any additive commutative monoid `M` and any of its additive submonoids `S`, and for any element `x` from `M` and `y` from `S`, applying the `AddLocalization.mk` function to `x` and `y` is equivalent to applying the `AddSubmonoid.LocalizationMap.mk'` function to the additive monoid of the localization at `S`, `x`, and `y`. In other words, these two ways of creating an element in the localization of `M` at `S` are equivalent.
More concisely: For any additive commutative monoid `M`, submonoid `S`, and elements `x` from `M` and `y` from `S`, `AddLocalization.mk x y` is equal to `AddSubmonoid.LocalizationMap.mk' (localization at S) x y`.
|
AddSubmonoid.LocalizationMap.map_addUnits
theorem AddSubmonoid.LocalizationMap.map_addUnits :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
(f : S.LocalizationMap N) (y : ↥S), IsAddUnit (f.toMap ↑y)
This theorem states that for any additive commutative monoid `M` and its additive submonoid `S`, along with a localization map `f` to another additive commutative monoid `N`, every element `y` from the submonoid `S` is an additive unit when mapped to `N` using the localization map. In other words, every mapped element from the submonoid has a two-sided additive inverse in the monoid `N`. In mathematical terms, for any `y` in `S`, there exists an element in `N` such that their sum under the localization map `f` is the additive identity of the monoid `N`.
More concisely: For any additive commutative monoid `M` with submonoid `S`, and localization map from `S` to an additive commutative monoid `N`, every element in `S` is a local additive unit in `N`, meaning it has a two-sided additive inverse in `N`.
|
Submonoid.LocalizationMap.mk'_spec
theorem Submonoid.LocalizationMap.mk'_spec :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
(f : S.LocalizationMap N) (x : M) (y : ↥S), f.mk' x y * f.toMap ↑y = f.toMap x
The theorem `Submonoid.LocalizationMap.mk'_spec` establishes a property of localization maps between two commutative monoids. Given a commutative monoid `M`, a submonoid `S` of `M`, a commutative monoid `N`, and a localization map `f` from `S` to `N`, for any element `x` from `M` and `y` from `S`, the product of the map of `x` and `y` under `f` equals the map of `x` under `f`. In other words, for any `x` in `M` and `y` in `S`, it ensures that `f(x,y) * f(y) = f(x)`, where `f(x,y)` denotes the image of the pair `(x, y)` under the localization map `f`.
More concisely: Given a localization map from a submonoid of a commutative monoid to another commutative monoid, the image of the product of any two elements under the map is equal to the product of their images.
|
AddSubmonoid.LocalizationMap.lift_eq
theorem AddSubmonoid.LocalizationMap.lift_eq :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
{P : Type u_3} [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P}
(hg : ∀ (y : ↥S), IsAddUnit (g ↑y)) (x : M), (f.lift hg) (f.toMap x) = g x
The theorem `AddSubmonoid.LocalizationMap.lift_eq` states that for any given additive commutative monoids `M`, `N`, and `P`, with `S` being an add submonoid of `M`, and given a localization map `f` from `S` to `N`, and another additive monoid homomorphism `g` from `M` to `P` such that every element of `S` under `g` is an additive unit, then for every element `x` of `M`, applying the localization map `f` to `x`, then lifting it to `P` using the lift of `f` is equivalent to directly applying `g` to `x`. In other words, the lift of `f` is an extension of `g` on the image of `M` under the localization map `f`. This theorem is essentially saying that the lift of a localization map behaves well with respect to the original map.
More concisely: Given additive commutative monoids M, N, and P, a localization map f from add submonoid S of M to N, and an additive monoid homomorphism g from M to P such that every element of S under g is an additive unit, then for all x in M, f(x) in N and g(x) in P are related by the equation g(x) = lift(f)(f(x)).
|
AddSubmonoid.LocalizationMap.add_neg_left
theorem AddSubmonoid.LocalizationMap.add_neg_left :
∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
{f : M →+ N} (h : ∀ (y : ↥S), IsAddUnit (f ↑y)) (y : ↥S) (w z : N),
w + ↑(-(IsAddUnit.liftRight (f.restrict S) h) y) = z ↔ w = f ↑y + z
This theorem states that given an additive monoid homomorphism `f` from `M` to `N` and a submonoid `S` of `M` such that the image of `S` under `f` lies within the additive units of `N`, for any elements `w` and `z` from `N` and `y` from `S`, the equation `w - f(y) = z` holds if and only if `w` equals the sum of `f(y)` and `z`. The minus sign `-` in `w - f(y)` is actually representing the additive inverse of `f(y)`, as the context is within additive monoids. This theorem is essentially capturing the notion of manipulating equations in a setting of additive monoids.
More concisely: Given an additive monoid homomorphism `f` from `M` to `N` with image of submonoid `S` in the additive units of `N`, for any `w`, `z` in `N` and `y` in `S`, the equation `w = f(y) + z` if and only if `w - f(y) = z`.
|
Localization.npow_def
theorem Localization.npow_def :
∀ {M : Type u_4} [inst : CommMonoid M] (S : Submonoid M), Localization.npow S = Monoid.npow
This theorem states that, for any type `M` that is a commutative monoid (denoted by `[inst : CommMonoid M]`) and any submonoid `S` of `M`, the exponentiation function for localizations (`Localization.npow S`) is equivalent to the exponentiation function for monoids (`Monoid.npow`). In other words, raising an element of the localization of a submonoid to a natural number power in the localization is the same as raising it to that power in the original monoid.
More concisely: For any commutative monoid `M` and submonoid `S`, the exponentiation function in the localization `Localization S M` equals the exponentiation function in `M`.
|
Submonoid.LocalizationMap.lift_mk'
theorem Submonoid.LocalizationMap.lift_mk' :
∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
[inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} (hg : ∀ (y : ↥S), IsUnit (g ↑y)) (x : M) (y : ↥S),
(f.lift hg) (f.mk' x y) = g x * ↑((IsUnit.liftRight (g.restrict S) hg) y)⁻¹
This theorem states that for a given localization map `f` from a commutative monoid `M` to `N` with respect to a submonoid `S` of `M`, and a monoid homomorphism `g` from `M` to another commutative monoid `P` such that `g` maps each element of `S` to a unit in `P`, then the induced homomorphism from `N` to `P` maps each element expressed as `f(x) * (f(y))⁻¹` to `g(x) * (g(y))⁻¹` for all `x` in `M` and `y` in `S`. Here, `f(x)` and `g(x)` represent the image of an element `x` under the maps `f` and `g`, respectively, and `(f(y))⁻¹` and `(g(y))⁻¹` represent the inverse of `f(y)` and `g(y)`, respectively.
More concisely: For a commutative monoid homomorphism g from a commutative monoid M to another commutative monoid P, and a localization map f from M to N with respect to a submonoid S of M such that each element of S is mapped to a unit in P by g, the induced homomorphism from N to P maps f(x) * f(s)⁻¹ to g(x) * g(s)⁻¹ for all x in M and s in S.
|