LocalizedModule.smul'_mk
theorem LocalizedModule.smul'_mk :
∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type v} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] (r : R) (s : ↥S) (m : M), r • LocalizedModule.mk m s = LocalizedModule.mk (r • m) s
The theorem `LocalizedModule.smul'_mk` states that for any commutative semiring `R`, submonoid `S` of `R`, and an `R`-module `M`, and for any element `r` of `R`, element `s` of `S`, and element `m` of `M`, the act of scaling the localized module element `LocalizedModule.mk m s` by `r` is the same as first scaling `m` by `r` and then localizing. In other words, scalar multiplication commutes with the localization process.
More concisely: For any commutative semiring R, submonoid S of R, and R-module M, the scalar multiplication of an element m of M by r in the localized module M��ss is equivalent to the localization of the scalar multiplication of m by r in M.
|
LocalizedModule.lift_comp
theorem LocalizedModule.lift_comp :
∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M'' : Type u_4}
[inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M''] [inst_3 : Module R M] [inst_4 : Module R M'']
(g : M →ₗ[R] M'') (h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)),
LocalizedModule.lift S g h ∘ₗ LocalizedModule.mkLinearMap S M = g
The theorem `LocalizedModule.lift_comp` states that for any commutative semiring `R` and submonoid `S` of `R`, and for any modules `M` and `M''` over `R`, if `g` is a linear map from `M` to `M''` such that all scalar multiplications by elements of `S` are invertible (in the sense that they are units in the ring of endomorphisms of `M''`), then the composition of the lift of `g` and the linear map defined by the function `m ↦ m / 1` (given by `LocalizedModule.mkLinearMap`) is equal to `g`. In other words, it says that under these conditions, we can "lift" `g` to a map between localized modules in such a way that the localization process is "undone" by this composition.
More concisely: Given a commutative semiring `R`, a submonoid `S` of `R`, modules `M` and `M''` over `R`, and a linear map `g` from `M` to `M''` such that scalar multiplications by elements of `S` in `M''` are invertible, the composition of the lift of `g` and the map `m ↦ m / 1` equals `g`.
|
LocalizedModule.lift_unique
theorem LocalizedModule.lift_unique :
∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M'' : Type u_4}
[inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M''] [inst_3 : Module R M] [inst_4 : Module R M'']
(g : M →ₗ[R] M'') (h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x))
(l : LocalizedModule S M →ₗ[R] M''), l ∘ₗ LocalizedModule.mkLinearMap S M = g → LocalizedModule.lift S g h = l
The theorem `LocalizedModule.lift_unique` states that for a given commutative semiring `R`, a submonoid `S` of `R`, types `M` and `M''` with addition and scalar multiplication, and a linear map `g` from `M` to `M''`, if all scalar multiplications by `s : S` are invertible and there exists another linear map `l` from the localized module of `M` by `S` to `M''` such that `l` composed with `mkLinearMap` equals `g`, then `l` is uniquely determined as the lift of `g`. Simply put, this theorem states a uniqueness property for the lift operation in the context of localized modules.
More concisely: Given a commutative semiring `R`, a submonoid `S` of `R`, types `M` and `M''` with additions and scalar multiplications, and a linear map `g : M -> M''` such that all scalar multiplications by `s : S` are invertible, if there exists a linear map `l : S^(-1) * M -> M''` with `l * mkLinearMap = g`, then `l` is uniquely determined as the lift of `g` to the localized module `S^(-1) * M`.
|
IsLocalizedModule.mk'_one
theorem IsLocalizedModule.mk'_one :
∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
[inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
[inst_5 : IsLocalizedModule S f] (m : M), IsLocalizedModule.mk' f m 1 = f m
The `IsLocalizedModule.mk'_one` theorem states that for any commutative semiring `R`, a submonoid `S` of `R`, `M` and `M'` as types with `M` and `M'` being Additive Commutative Monoids and `R`-modules, and a linear map `f` from `M` to `M'` which is a localized module with respect to `S`, when the `mk'` function is applied on `f` with an element `m` from `M` and `1` from the submonoid `S`, the result is equal to applying the function `f` on the element `m`. In mathematical terms, it says that for a certain localization map `f`, `f(m) = m/1`.
More concisely: For a localized module homomorphism `f` from an `R`-module `M` to an `R`-module `M'` over a commutative semiring `R`, with respect to a submonoid `S`, the localization `f(m)/1` equals `f(m)` for all `m` in `M`.
|
IsLocalizedModule.is_universal
theorem IsLocalizedModule.is_universal :
∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4}
[inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M'] [inst_3 : AddCommMonoid M''] [inst_4 : Module R M]
[inst_5 : Module R M'] [inst_6 : Module R M''] (f : M →ₗ[R] M') [inst_7 : IsLocalizedModule S f]
(g : M →ₗ[R] M''), (∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)) → ∃! l, l ∘ₗ f = g
This theorem states a universal property of localized modules. Given a commutative semiring `R` and a submonoid `S` of `R`, if `(M', f : M ⟶ M')` is a localized `R`-module, then it has a property that for any `R`-module `M''` where every scalar multiplication by `s : S` is invertible, and for any `R`-linear map `g : M ⟶ M''`, there exists a unique `R`-linear map `l : M' ⟶ M''` such that the composition of `l` after `f` equals `g` (i.e., `l ∘ f = g`). In other words, given a specific `R`-module and `R`-linear map, there is a single `R`-linear map from the localized module that respects the original map.
More concisely: Given a commutative semiring `R`, a submonoid `S` of `R`, and an `R`-module `(M', f : M ⟶ M')` that is localized over `S`, for any `R`-module `M''` where every scalar multiplication by `s : S` is invertible, there exists a unique `R`-linear map `l : M' ⟶ M''` such that `l ∘ f = g` for any `R`-linear map `g : M ⟶ M''`.
|
IsLocalizedModule.mk'_smul
theorem IsLocalizedModule.mk'_smul :
∀ {R : Type u_1} [inst : CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
[inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
[inst_5 : IsLocalizedModule S f] (r : R) (m : M) (s : ↥S),
IsLocalizedModule.mk' f (r • m) s = r • IsLocalizedModule.mk' f m s
This theorem states that for all commutative semirings `R`, submonoids `S` of `R`, additive commutative monoids `M` and `M'`, and modules `M` and `M'` over `R`, if `f` is a linear map from `M` to `M'` which satisfies the property of being a localized module with respect to `S`, then for any element `r` of `R`, any element `m` of `M`, and any element `s` of `S`, the fraction `r • m / s` with respect to the localization map `f` (denoted as `IsLocalizedModule.mk' f (r • m) s`) is equal to `r` times the fraction `m / s` with respect to the localization map `f` (denoted as `r • IsLocalizedModule.mk' f m s`). In mathematical terms, this states that the localization map `f` respects the scalar multiplication operation of the modules.
More concisely: For all commutative semirings `R`, submonoids `S` of `R`, additive commutative `R`-modules `M` and `M'`, and linear maps `f` from `M` to `M'` that are localized module homomorphisms with respect to `S`, the scalar multiplication operation is respected, i.e., `f(r * m) = r * f(m)` for all `r` in `R` and `m` in `M`.
|
LocalizedModule.lift_mk
theorem LocalizedModule.lift_mk :
∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M'' : Type u_4}
[inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M''] [inst_3 : Module R M] [inst_4 : Module R M'']
(g : M →ₗ[R] M'') (h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)) (m : M) (s : ↥S),
(LocalizedModule.lift S g h) (LocalizedModule.mk m s) = ↑⋯.unit⁻¹ (g m)
The theorem `LocalizedModule.lift_mk` asserts that for a commutative semiring `R`, a submonoid `S` of `R`, and a linear map `g` from a module `M` to another module `M''` over `R`, if every scalar multiplication by an element `s` in `S` is a unit (i.e., has a multiplicative inverse), then the result of lifting `g` to the localized module at `s` and applying it to the localization of an element `m` from `M` at `s` is equal to the scalar multiplication of the inverse of the unit associated with `s` and the image of `m` under `g`. In mathematical notation, this is saying that `(LocalizedModule.lift S g h) (LocalizedModule.mk m s) = s⁻¹ • g m` where `s⁻¹` is the inverse of the unit associated with `s`.
More concisely: If `g` is a linear map from a module `M` to another module `M''` over a commutative semiring `R`, `S` is a submonoid of `R` such that every scalar multiplication by an element `s` in `S` is a unit, and `m` is an element of `M`, then `(LocalizedModule.lift S g h) (LocalizedModule.mk m s) = s⁻¹ • g m`, where `s⁻¹` is the multiplicative inverse of the unit associated with `s`.
|
IsLocalizedModule.mk'_eq_iff
theorem IsLocalizedModule.mk'_eq_iff :
∀ {R : Type u_1} [inst : CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
[inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] {f : M →ₗ[R] M'}
[inst_5 : IsLocalizedModule S f] {m : M} {s : ↥S} {m' : M'}, IsLocalizedModule.mk' f m s = m' ↔ f m = s • m'
This theorem, `IsLocalizedModule.mk'_eq_iff`, states that for any commutative semiring `R`, submonoid `S` of `R`, modules `M` and `M'` over `R`, localization map `f` from `M` to `M'`, element `m` of `M`, element `s` of `S`, and element `m'` of `M'`, the fraction `m/s` with respect to the localization map `f` is equal to `m'` if and only if the result of applying `f` to `m` is equal to the scalar multiplication of `s` and `m'`. In other words, it relates equality in the localized module to equality under the localization map in the original module.
More concisely: For any commutative semiring `R`, submonoid `S` of `R`, modules `M` and `M'` over `R`, localization map `f` from `M` to `M'`, and elements `m` of `M`, `s` of `S`, and `m'` of `M'`, `m/s ≡ m'` in the localized module if and only if `f(m) = s * m'`.
|
LocalizedModule.subsingleton
theorem LocalizedModule.subsingleton :
∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type v} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M], 0 ∈ S → Subsingleton (LocalizedModule S M)
The theorem `LocalizedModule.subsingleton` states that if `S` is a multiplicative subset of a commutative semiring `R` containing the element `0`, and `M` is an `R`-module, then the localization of `M` at `S` is a subsingleton. In other words, this means that if `0` is in `S`, then the localization of `M` by `S` has at most one element.
More concisely: If `S` is a multiplicative subset of a commutative semiring `R` containing `0`, then the localization of an `R`-module `M` at `S` has at most one element.
|
LocalizedModule.mk_cancel_common_right
theorem LocalizedModule.mk_cancel_common_right :
∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type v} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] (s s' : ↥S) (m : M), LocalizedModule.mk (s' • m) (s * s') = LocalizedModule.mk m s
The theorem `LocalizedModule.mk_cancel_common_right` states that for any commutative semiring `R`, any submonoid `S` of `R`, any additively commutative monoid `M` that is also a `R`-module, and any elements `s` and `s'` from `S` and `m` from `M`, the localization of `s'` scaled by `m` at the product `s * s'` is equal to the localization of `m` at `s`. In other words, the process of localizing `m` at `s` in a localized module `S` of `M` is not affected by scaling the module element `m` by an element `s'` from `S` and simultaneously multiplying the localizing element `s` by the same `s'`.
More concisely: For any commutative semiring R, submonoid S, additively commutative R-module M, and elements s, s' from S and m from M, the localization of m at s in the localized module S of M is equal to the localization of m scaled by s' at s * s'.
|
LocalizedModule.mk_eq
theorem LocalizedModule.mk_eq :
∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type v} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] {m m' : M} {s s' : ↥S},
LocalizedModule.mk m s = LocalizedModule.mk m' s' ↔ ∃ u, u • s' • m = u • s • m'
The theorem `LocalizedModule.mk_eq` states that for any commutative semiring `R`, any submonoid `S` of `R`, any additive commutative monoid `M` that is also an `R`-module, and any elements `m, m'` of `M` and `s, s'` of the submonoid `S`, the localized module elements `m/s` and `m'/s'` are equal if and only if there exists an element `u` in the submonoid `S` such that `u` multiplied by `s'` and then by `m` equals `u` multiplied by `s` and then by `m'`. In other words, if two fractions `m/s` and `m'/s'` in the localized module are equal, then there's a 'scaling factor' `u` that links `m` and `s'` with `m'` and `s`.
More concisely: For any commutative semiring R, submonoid S of R, additive commutative monoid M an R-module, and elements m, m' of M and s, s' of S, the localized module elements m/s and m'/s' are equal if and only if there exists u in S such that us = sm and um' = s'm'.
|
LocalizedModule.induction_on
theorem LocalizedModule.induction_on :
∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type v} [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] {β : LocalizedModule S M → Prop},
(∀ (m : M) (s : ↥S), β (LocalizedModule.mk m s)) → ∀ (x : LocalizedModule S M), β x
This theorem, called `LocalizedModule.induction_on`, states that for any commutative semiring `R`, a multiplicative subset `S` of `R`, an `R`-module `M`, and a property `β` defined on the localized module of `M` by `S`, if the property `β` holds for every element of the form `(m/s)` where `m` is an element of `M` and `s` is an element of the submonoid `S`, then the property `β` holds for every element of the localized module. This theorem essentially provides a method of induction for proving properties on the localized module.
More concisely: If a property holds for all elements of the form `m/s` in the localized module `M/S` of an `R`-module `M` over a commutative semiring `R` with multiplicative subset `S`, then the property holds for all elements in `M/S`.
|