HomogeneousLocalization.mul_val
theorem HomogeneousLocalization.mul_val :
โ {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [inst : AddCommMonoid ฮน] [inst_1 : DecidableEq ฮน]
[inst_2 : CommRing R] [inst_3 : CommRing A] [inst_4 : Algebra R A] {๐ : ฮน โ Submodule R A}
[inst_5 : GradedAlgebra ๐] {x : Submonoid A} (y1 y2 : HomogeneousLocalization ๐ x),
(y1 * y2).val = y1.val * y2.val
The theorem `HomogeneousLocalization.mul_val` states that for any given types ฮน, R, and A, where ฮน is an additive commutative monoid and R and A are commutative rings, and A is an algebra over R, given a function ๐ from ฮน to submodules of A over R forming a graded algebra, and a submonoid x of A, and any two elements y1 and y2 of the homogeneous localization of ๐ at x, the value of the product of y1 and y2 in the homogeneous localization is equal to the product of the values of y1 and y2. In other words, this is a statement of multiplicativity in the context of homogeneous localization, indicated by the equality `HomogeneousLocalization.val (y1 * y2) = HomogeneousLocalization.val y1 * HomogeneousLocalization.val y2`.
More concisely: In the context of commutative rings R, commutative monoid ฮน, and an algebra A over R, given a graded submodule algebra ๐ from ฮน to submodules of A, and a submonoid x of A, the product of two elements in the homogeneous localization of ๐ at x is equal to the product of their localized values.
|
HomogeneousLocalization.add_val
theorem HomogeneousLocalization.add_val :
โ {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [inst : AddCommMonoid ฮน] [inst_1 : DecidableEq ฮน]
[inst_2 : CommRing R] [inst_3 : CommRing A] [inst_4 : Algebra R A] {๐ : ฮน โ Submodule R A}
[inst_5 : GradedAlgebra ๐] {x : Submonoid A} (y1 y2 : HomogeneousLocalization ๐ x),
(y1 + y2).val = y1.val + y2.val
The theorem `HomogeneousLocalization.add_val` states that for any type `ฮน` which is an additive commutative monoid, a type `R` which is a commutative ring, and a type `A` which is also a commutative ring with an algebra over `R`, given a grading function `๐` from `ฮน` to submodules of `A`, a `GradedAlgebra` instance for `๐`, and a submonoid `x` of `A`, the operation `HomogeneousLocalization.val` is additive. In other words, for any two elements `y1` and `y2` of the homogeneous localization of `A` with respect to `๐` and `x`, the value of `HomogeneousLocalization.val` applied to the sum of `y1` and `y2` is equal to the sum of the values of `HomogeneousLocalization.val` applied to `y1` and `y2` individually. This essentially asserts that the `HomogeneousLocalization.val` function respects the addition operation of the ring.
More concisely: For any commutative ring `R`, additive commutative monoid `ฮน`, commutative ring `A` with an algebra structure over `R`, grading function `๐` from `ฮน` to submodules of `A`, and submonoid `x` of `A`, the `HomogeneousLocalization.val` function is additive on the homogeneous localization of `A` with respect to `๐` and `x`.
|
HomogeneousLocalization.one_val
theorem HomogeneousLocalization.one_val :
โ {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [inst : AddCommMonoid ฮน] [inst_1 : DecidableEq ฮน]
[inst_2 : CommRing R] [inst_3 : CommRing A] [inst_4 : Algebra R A] {๐ : ฮน โ Submodule R A}
[inst_5 : GradedAlgebra ๐] {x : Submonoid A}, HomogeneousLocalization.val 1 = 1
The theorem `HomogeneousLocalization.one_val` states that for any types `ฮน`, `R`, and `A`, where `ฮน` is an additive commutative monoid and `R` and `A` are commutative rings, and `A` is an `R`-algebra, and for any function `๐` from `ฮน` to the submodules of `R` in `A`, such that `๐` forms a graded algebra, and any submonoid `x` of `A`, the value function applied to the number one in the homogeneous localization of `๐` at `x` results in the number one. This theorem essentially asserts that the value function preserves the identity element under homogeneous localization.
More concisely: For any graded algebra ๐ from an additive commutative monoid ฮน to the submodules of an R-algebra A over a commutative ring R, the value function applied to one in the homogeneous localization of ๐ at any submonoid x is the identity element.
|
HomogeneousLocalization.zero_val
theorem HomogeneousLocalization.zero_val :
โ {ฮน : Type u_1} {R : Type u_2} {A : Type u_3} [inst : AddCommMonoid ฮน] [inst_1 : DecidableEq ฮน]
[inst_2 : CommRing R] [inst_3 : CommRing A] [inst_4 : Algebra R A] {๐ : ฮน โ Submodule R A}
[inst_5 : GradedAlgebra ๐] {x : Submonoid A}, HomogeneousLocalization.val 0 = 0
The theorem `HomogeneousLocalization.zero_val` states that for any graded algebra, represented by an index type `ฮน`, a commutative ring `R`, a commutative ring `A`, an algebra structure on `A` over `R`, a map `๐` from `ฮน` to submodules of `A` over `R`, and a submonoid `x` of `A`, the value of the homogeneous localization at zero is zero. In other words, the homogeneous localization does not change the zero element in the algebra.
More concisely: For any graded algebra `A` over a commutative ring `R`, the homogeneous localization of the zero element at any submonoid is still the zero element.
|