elementalStarAlgebra.closedEmbedding_coe
theorem elementalStarAlgebra.closedEmbedding_coe :
∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : TopologicalSpace A]
[inst_3 : Semiring A] [inst_4 : StarRing A] [inst_5 : TopologicalSemiring A] [inst_6 : ContinuousStar A]
[inst_7 : Algebra R A] [inst_8 : StarModule R A] (x : A), ClosedEmbedding Subtype.val
This theorem states that for any type `R` and type `A` with certain conditions, the coercion from an elemental algebra to the full algebra is a `ClosedEmbedding`. More specifically, if `R` is a `CommSemiring` and a `StarRing`, and `A` is a structure with a `Semiring`, `StarRing`, and `TopologicalSemiring` structures, as well as a `ContinuousStar`, an `Algebra` over `R`, and is a `StarModule` over `R`, then the function `Subtype.val` is a closed embedding. This function `Subtype.val` takes an element of a subtype (of type `A`) satisfying a certain property and returns it as an element of the base type `A`.
More concisely: For any CommSemiring and StarRing `R`, and a Type `A` with a Semiring, StarRing, TopologicalSemiring, ContinuousStar, Algebra structure over `R`, and a StarModule structure, the coercion from an element of the subtype satisfying a certain property to `A` via `Subtype.val` is a closed embedding.
|
StarSubalgebra.embedding_inclusion
theorem StarSubalgebra.embedding_inclusion :
∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : TopologicalSpace A]
[inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : StarRing A] [inst_6 : StarModule R A]
{S₁ S₂ : StarSubalgebra R A} (h : S₁ ≤ S₂), Embedding ⇑(StarSubalgebra.inclusion h)
This theorem states that for any two star subalgebras S₁ and S₂ of a star ring A over a commutative semiring R, if S₁ is a subset of (or equal to) S₂, then the function that includes each element of S₁ into S₂ (known as the `StarSubalgebra.inclusion` function) is an `Embedding`. This means that the inclusion function is both injective (unique images for unique inputs) and its image under the function topology is a homeomorphism of the original set.
More concisely: If S₁ is a star subalgebra of a star ring A over a commutative semiring R, and S₁ is a subset or equal to S₂, then the inclusion function from S₁ to S₂ is a homeomorphic embedding.
|
StarSubalgebra.closedEmbedding_inclusion
theorem StarSubalgebra.closedEmbedding_inclusion :
∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : TopologicalSpace A]
[inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : StarRing A] [inst_6 : StarModule R A]
{S₁ S₂ : StarSubalgebra R A} (h : S₁ ≤ S₂), IsClosed ↑S₁ → ClosedEmbedding ⇑(StarSubalgebra.inclusion h)
This theorem states that for any two star subalgebras `S₁` and `S₂` of a star module over a star ring and a commutative semiring `R` with a topological space `A`, if `S₁` is a subset of or equal to `S₂` and `S₁` is closed, then the `StarSubalgebra.inclusion` function, which represents the inclusion of `S₁` into `S₂`, is a `ClosedEmbedding`. A `ClosedEmbedding` is a function that is both a homeomorphism onto its image (a function preserving the topological properties) and a closed map (a function that maps closed sets to closed sets).
More concisely: If `S₁` is a closed star subalgebra of `S₂`, which is a star subalgebra of a star module over a star ring and a commutative semiring with a topological space, then the inclusion function from `S₁` to `S₂` is a closed embedding.
|
elementalStarAlgebra.self_mem
theorem elementalStarAlgebra.self_mem :
∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : TopologicalSpace A]
[inst_3 : Semiring A] [inst_4 : StarRing A] [inst_5 : TopologicalSemiring A] [inst_6 : ContinuousStar A]
[inst_7 : Algebra R A] [inst_8 : StarModule R A] (x : A), x ∈ elementalStarAlgebra R x
This theorem states that for any given type `R` and another type `A`, under several conditions - `R` is a commutative semiring and a star ring, `A` is a topological space, a semiring, a star ring, a topological semiring, a continuous star, an algebra over `R`, and a star module over `R` - any element `x` from `A` is contained in the elemental star algebra of `R` and `x`.
More concisely: For any commutative semiring and star ring `R`, and any topological space, semiring, star ring, topological semiring, continuous star, algebra, and star module `A` over `R`, every element `x` in `A` is contained in the elemental star algebra of `R` and `x`.
|