continuous_algebraMap
theorem continuous_algebraMap :
∀ (R : Type u_1) (A : Type u) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
[inst_3 : TopologicalSpace R] [inst_4 : TopologicalSpace A] [inst_5 : TopologicalSemiring A]
[inst_6 : ContinuousSMul R A], Continuous ⇑(algebraMap R A)
The theorem states that for any two types `R` and `A`, where `R` is a commutative semiring, `A` is a semiring and `A` is an algebra over `R`, if the operations of `R` and `A` are continuous (meaning `R` and `A` are topological spaces where the semiring operations on `A` are continuous, and the scalar multiplication from `R` to `A` is also continuous), then the function `algebraMap`, which maps elements from `R` to `A` according to the algebra structure, is a continuous function.
More concisely: If `R` is a commutative semiring, `A` is a semiring and an algebra over `R`, `R` and `A` are topological spaces with continuous semiring operations and scalar multiplication, then the algebra map from `R` to `A` is a continuous function.
|
Subalgebra.le_topologicalClosure
theorem Subalgebra.le_topologicalClosure :
∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u} [inst_1 : TopologicalSpace A] [inst_2 : Semiring A]
[inst_3 : Algebra R A] [inst_4 : TopologicalSemiring A] (s : Subalgebra R A), s ≤ s.topologicalClosure
This theorem states that for any subalgebra `s` of a topological semiring `A` over a commutative semiring `R`, `s` is subset of its topological closure. In other words, every element in the subalgebra `s` is also an element in its topological closure. This theorem holds in the context of a topological space `A` that also has a semiring structure where `R` is the ring of scalars and `A` is the ring of elements, and the semiring `A` is also a topological semiring.
More concisely: Given a topological semiring `A` over a commutative semiring `R`, any subalgebra `s` of `A` is contained in its topological closure.
|
Subalgebra.topologicalClosure_comap_homeomorph
theorem Subalgebra.topologicalClosure_comap_homeomorph :
∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u} [inst_1 : TopologicalSpace A] [inst_2 : Semiring A]
[inst_3 : Algebra R A] [inst_4 : TopologicalSemiring A] (s : Subalgebra R A) {B : Type u_2}
[inst_5 : TopologicalSpace B] [inst_6 : Ring B] [inst_7 : TopologicalRing B] [inst_8 : Algebra R B]
(f : B →ₐ[R] A) (f' : B ≃ₜ A),
⇑f = ⇑f' → Subalgebra.comap f s.topologicalClosure = (Subalgebra.comap f s).topologicalClosure
This theorem states that for any commutative semiring `R`, given two types `A` and `B` which have the structures of a topological space, semiring, algebra over `R`, and a topological semiring (or a ring and a topological ring for `B`), a subalgebra `s` of `A`, an algebra homomorphism `f` from `B` to `A`, and a homeomorphism `f'` from `B` to `A`, if the two maps `f` and `f'` are the same as functions, then the topological closure of the preimage of `s` under `f` is the same as the topological closure of the preimage of `s` under `f`.
In other words, in the context of topological algebra, this theorem stipulates that the operation of taking the topological closure commutes with taking the preimage under an algebra homomorphism that is also a homeomorphism.
More concisely: Given a commutative semiring `R`, two topological spaces `A` and `B` with semiring, algebra over `R`, and topological semiring structures, a subalgebra `s` of `A`, an algebra homomorphism and homeomorphism `f` from `B` to `A`, if `f` is the identity function, then the topological closure of `f''-1(s)` equals `f''-1(Cl(s))`, where `Cl(s)` is the topological closure of `s` in `A`.
|