Unitization.algHom_ext'
theorem Unitization.algHom_ext' :
∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
[inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A] {C : Type u_5} [inst_5 : Semiring C]
[inst_6 : Algebra R C] {φ ψ : Unitization R A →ₐ[R] C},
(↑φ).comp (Unitization.inrNonUnitalAlgHom R A) = (↑ψ).comp (Unitization.inrNonUnitalAlgHom R A) → φ = ψ
The theorem `Unitization.algHom_ext'` states that for any commutative semiring `R`, any non-unital semiring `A` that is also an `R`-module, any semiring `C` that is also an `R`-algebra, and any two `R`-algebra homomorphisms `φ` and `ψ` from the unitization of `A` over `R` to `C`, if the composition of `φ` and the non-unital algebra homomorphism from `A` to its unitization is equal to the composition of `ψ` and the same non-unital algebra homomorphism, then `φ` is equal to `ψ`. In simpler terms, this theorem provides a condition for the equality of two `R`-algebra homomorphisms from the unitization of a non-unital `R`-algebra to another `R`-algebra.
More concisely: Given commutative semirings `R`, non-unital `R`-semirings `A`, `R`-algebras `C`, and `R-`algebra homomorphisms `φ` and `ψ` from the unitization of `A` to `C`, if `φ ∘ i_A` equals `ψ ∘ i_A` where `i_A` is the inclusion of `A` into its unitization, then `φ` equals `ψ`.
|
Unitization.starAlgHom_ext
theorem Unitization.starAlgHom_ext :
∀ {R : Type u_1} {A : Type u_2} {C : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R]
[inst_2 : NonUnitalSemiring A] [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : SMulCommClass R A A]
[inst_6 : IsScalarTower R A A] [inst_7 : Semiring C] [inst_8 : Algebra R C] [inst_9 : StarRing C]
{φ ψ : Unitization R A →⋆ₐ[R] C},
(↑φ).comp (Unitization.inrNonUnitalStarAlgHom R A) = (↑ψ).comp (Unitization.inrNonUnitalStarAlgHom R A) → φ = ψ
This theorem, `Unitization.starAlgHom_ext`, states that for any types `R`, `A`, and `C`, where `R` is a commutative semiring with a star operation, `A` is a non-unital semiring with a star operation and `R`-module structure with certain commutativity and scalar tower properties, and `C` is a semiring with `R`-algebra and star-ring structures. If we have two star-algebra homomorphisms `φ` and `ψ` from the unitization of `A` with `R` to `C`, then if these two homomorphisms agree when composed with the coercion from `A` to its unitization, they were equal in the first place. Essentially, it's a uniqueness property for star-algebra homomorphisms under a certain equality condition.
More concisely: Given commutative semirings `R` with star operations, non-unital semirings `A` with star operations and `R`-module structures satisfying certain conditions, and semirings `C` with `R`-algebra and star-ring structures: if two star-algebra homomorphisms from the unitization of `A` to `C` agree when composed with the coercion from `A` to its unitization, then they are equal.
|
Unitization.ind
theorem Unitization.ind :
∀ {R : Type u_5} {A : Type u_6} [inst : AddZeroClass R] [inst_1 : AddZeroClass A] {P : Unitization R A → Prop},
(∀ (r : R) (a : A), P (Unitization.inl r + ↑a)) → ∀ (x : Unitization R A), P x
This theorem states that, given any types `R` and `A` and a property `P` concerning the unitization of a non-unital `R`-algebra `A`, if it is shown that the property `P` holds for all elements of the form `Unitization.inl r + a` (where `r` is from `R` and `a` is from `A`), then the property `P` holds for all elements of the unitization of `A`. This can be instrumental in performing induction on elements of the unitization using `Unitization.ind`.
More concisely: If a property `P` holds for all `r + a` in the unitization of a non-unital `R`-algebra `A` with `r` from `R` and `a` from `A`, then `P` holds for all elements of the unitization of `A`.
|
Unitization.ext
theorem Unitization.ext :
∀ {R : Type u_1} {A : Type u_2} {x y : Unitization R A}, x.fst = y.fst → x.snd = y.snd → x = y
The theorem `Unitization.ext` states that for any types `R` and `A`, and for any elements `x` and `y` of the minimal unitization of a non-unital `R`-algebra `A` (which is a pair consisting of an element from `R` and an element from `A`), if the `R` component (obtained using the `Unitization.fst` function) of `x` equals the `R` component of `y`, and the `A` component (obtained using the `Unitization.snd` function) of `x` equals the `A` component of `y`, then `x` equals `y`. In other words, two elements of the minimal unitization are equal if and only if their corresponding components are equal.
More concisely: For any non-unital `R`-algebra `A` and its minimal unitization, two elements with equal `R` and `A` components are equal.
|
Unitization.linearMap_ext
theorem Unitization.linearMap_ext :
∀ {S : Type u_2} {R : Type u_3} {A : Type u_4} {N : Type u_5} [inst : Semiring S] [inst_1 : AddCommMonoid R]
[inst_2 : AddCommMonoid A] [inst_3 : AddCommMonoid N] [inst_4 : Module S R] [inst_5 : Module S A]
[inst_6 : Module S N] ⦃f g : Unitization R A →ₗ[S] N⦄,
(∀ (r : R), f (Unitization.inl r) = g (Unitization.inl r)) → (∀ (a : A), f ↑a = g ↑a) → f = g
The theorem `Unitization.linearMap_ext` states that, given two linear maps `f` and `g` from the unitization of a non-unital `R`-algebra `A` to another module `N`, both over a semiring `S`, if `f` and `g` agree on the elements of the form `(r, 0)` (where `r` is an element of `R`) and on elements of `A`, then the two maps `f` and `g` must be the same. The caution about not marking the theorem as `@[ext]` is due to the fact that it can interfere with the usage of another extensionality theorem `LinearMap.prod_ext` when working with product types `R × A`.
More concisely: If two linear maps from the unitization of an `R`-algebra `A` to a module `N` over a semiring `S` agree on elements of the form `(r, 0)` and on elements of `A`, then they are equal.
|