NonUnitalSubalgebra.unitization_range
theorem NonUnitalSubalgebra.unitization_range :
∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
[inst_3 : SetLike S A] [hSA : NonUnitalSubsemiringClass S A] [hSRA : SMulMemClass S R A] (s : S),
(NonUnitalSubalgebra.unitization s).range = Algebra.adjoin R ↑s
The theorem `NonUnitalSubalgebra.unitization_range` states that for any type `R` with commutative semiring structure, type `A` with semiring structure and algebra structure over `R`, type `S` that behaves like a set of elements from `A` with non-unital subsemiring structure and scalar multiplication behavior, and any `s` of type `S`, the range of the algebra homomorphism obtained by unitizing the non-unital subalgebra `s` is the same as the subalgebra generated by the algebraic adjunction of `s` over `R`. In simple terms, unitizing a non-unital subalgebra and then taking its range gives us the same result as simply adjoining the elements of the subalgebra to `R`.
More concisely: For any commutative semiring `R`, semiring and algebra `A` over `R`, non-unital subsemiring `S` of `A` with scalar multiplication behavior, and `s` in `S`, the range of the algebra homomorphism obtained by unitizing `s` equals the subalgebra generated by `s` and `R`.
|
AlgHomClass.unitization_injective'
theorem AlgHomClass.unitization_injective' :
∀ {F : Type u_1} {R : Type u_2} {S : Type u_3} {A : Type u_4} [inst : CommRing R] [inst_1 : Ring A]
[inst_2 : Algebra R A] [inst_3 : SetLike S A] [hSA : NonUnitalSubringClass S A] [hSRA : SMulMemClass S R A]
(s : S),
(∀ (r : R), r ≠ 0 → (algebraMap R A) r ∉ s) →
∀ [inst_4 : FunLike F (Unitization R ↥s) A] [inst_5 : AlgHomClass F R (Unitization R ↥s) A] (f : F),
(∀ (x : ↥s), f ↑x = ↑x) → Function.Injective ⇑f
This theorem, `AlgHomClass.unitization_injective'`, states that under certain conditions, a map `f` is injective. These conditions are:
1. `F`, `R`, `S`, and `A` are types with `R` being a commutative ring, `A` a ring, and `A` an `R`-algebra. `S` is a subset of `A` in the sense of `SetLike`, and `S` is a non-unital subring of `A`. Furthermore, scalar multiplication of `R` and `A` is well-defined on `S`.
2. For all non-zero scalars `r` in `R`, the image of `r` under the algebra map `R → A` does not belong to `S`.
3. `f` is a function-like object from `Unitization R ↥s` to `A` and also an algebra homomorphism from `R` to `Unitization R ↥s` to `A`.
Under these conditions, if `f` satisfies the condition that for all `x` in `s`, `f` of the representative of `x` equals `x` itself, then `f` is injective. This theorem provides a sufficient condition for injectivity of non-unital subalgebra unitization when the scalars are a commutative ring. When the scalars form a field, a more natural theorem `NonUnitalStarSubalgebra.unitization_injective` should be used, as its hypothesis is easier to verify.
More concisely: Given a commutative ring `R`, an `R`-algebra `A`, a non-unital subring `S` of `A` with scalar multiplication well-defined, and an algebra homomorphism `f` from `Unitization R ↥s` to `A` such that `f` maps each representative of an element in `s` to itself and no non-zero scalar in `R` maps to an element in `S`, then `f` is injective.
|
AlgHomClass.unitization_injective
theorem AlgHomClass.unitization_injective :
∀ {F : Type u_1} {R : Type u_2} {S : Type u_3} {A : Type u_4} [inst : Field R] [inst_1 : Ring A]
[inst_2 : Algebra R A] [inst_3 : SetLike S A] [hSA : NonUnitalSubringClass S A] [hSRA : SMulMemClass S R A]
(s : S),
1 ∉ s →
∀ [inst_4 : FunLike F (Unitization R ↥s) A] [inst_5 : AlgHomClass F R (Unitization R ↥s) A] (f : F),
(∀ (x : ↥s), f ↑x = ↑x) → Function.Injective ⇑f
The theorem `AlgHomClass.unitization_injective` states that for any fields `F` and `R`, ring `A`, set `S` and element `s` of `S` where `1` is not in `s`, if `F` behaves function-like from the unitization of `R` and `s` to `A` and `F` also behaves like an algebra homomorphism from `R` and the unitization of `R` and `s` to `A`, then any function `f` of type `F` which maps each element `x` in `s` to itself is injective. In other words, if `f x = f y` for any `x` and `y` in `s`, then `x = y`.
This theorem is a generic version that allows to prove both `NonUnitalSubalgebra.unitization_injective` and `NonUnitalStarSubalgebra.unitization_injective` which means it holds for both non-unital subalgebra and non-unital star subalgebra where the algebra does not necessarily have a unit element (or the number `1`).
More concisely: If `F` is a function-like and algebra homomorphism from a ring `R` and its unitization with an element `s` not in `1` to a ring `A`, then `F` restricts to a injective function on `s`.
|