Topological (sub)algebras #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
A topological algebra over a topological semiring R is a topological semiring with a compatible
continuous scalar multiplication by elements of R. We reuse typeclass has_continuous_smul for
topological algebras.
Results #
This is just a minimal stub for now!
The topological closure of a subalgebra is still a subalgebra, which as an algebra is a topological algebra.
theorem
continuous_algebra_map_iff_smul
(R : Type u_1)
(A : Type u)
[comm_semiring R]
[semiring A]
[algebra R A]
[topological_space R]
[topological_space A]
[topological_semiring A] :
continuous ⇑(algebra_map R A) ↔ continuous (λ (p : R × A), p.fst • p.snd)
@[continuity]
theorem
continuous_algebra_map
(R : Type u_1)
(A : Type u)
[comm_semiring R]
[semiring A]
[algebra R A]
[topological_space R]
[topological_space A]
[topological_semiring A]
[has_continuous_smul R A] :
continuous ⇑(algebra_map R A)
theorem
has_continuous_smul_of_algebra_map
(R : Type u_1)
(A : Type u)
[comm_semiring R]
[semiring A]
[algebra R A]
[topological_space R]
[topological_space A]
[topological_semiring A]
(h : continuous ⇑(algebra_map R A)) :
@[simp]
theorem
algebra_map_clm_coe_apply
(R : Type u_1)
(A : Type u)
[comm_semiring R]
[semiring A]
[algebra R A]
[topological_space R]
[topological_space A]
[topological_semiring A]
[has_continuous_smul R A]
(ᾰ : R) :
⇑↑(algebra_map_clm R A) ᾰ = ⇑(algebra_map R A) ᾰ
def
algebra_map_clm
(R : Type u_1)
(A : Type u)
[comm_semiring R]
[semiring A]
[algebra R A]
[topological_space R]
[topological_space A]
[topological_semiring A]
[has_continuous_smul R A] :
The inclusion of the base ring in a topological algebra as a continuous linear map.
Equations
- algebra_map_clm R A = {to_linear_map := {to_fun := ⇑(algebra_map R A), map_add' := _, map_smul' := _}, cont := _}
@[simp]
theorem
algebra_map_clm_apply
(R : Type u_1)
(A : Type u)
[comm_semiring R]
[semiring A]
[algebra R A]
[topological_space R]
[topological_space A]
[topological_semiring A]
[has_continuous_smul R A]
(ᾰ : R) :
⇑(algebra_map_clm R A) ᾰ = ⇑(algebra_map R A) ᾰ
theorem
algebra_map_clm_coe
(R : Type u_1)
(A : Type u)
[comm_semiring R]
[semiring A]
[algebra R A]
[topological_space R]
[topological_space A]
[topological_semiring A]
[has_continuous_smul R A] :
⇑(algebra_map_clm R A) = ⇑(algebra_map R A)
theorem
algebra_map_clm_to_linear_map
(R : Type u_1)
(A : Type u)
[comm_semiring R]
[semiring A]
[algebra R A]
[topological_space R]
[topological_space A]
[topological_semiring A]
[has_continuous_smul R A] :
(algebra_map_clm R A).to_linear_map = algebra.linear_map R A
@[protected, instance]
def
subalgebra.has_continuous_smul
{R : Type u_1}
[comm_semiring R]
{A : Type u}
[topological_space A]
[semiring A]
[algebra R A]
[topological_space R]
[has_continuous_smul R A]
(s : subalgebra R A) :
def
subalgebra.topological_closure
{R : Type u_1}
[comm_semiring R]
{A : Type u}
[topological_space A]
[semiring A]
[algebra R A]
[topological_semiring A]
(s : subalgebra R A) :
subalgebra R A
The closure of a subalgebra in a topological algebra as a subalgebra.
@[simp]
theorem
subalgebra.topological_closure_coe
{R : Type u_1}
[comm_semiring R]
{A : Type u}
[topological_space A]
[semiring A]
[algebra R A]
[topological_semiring A]
(s : subalgebra R A) :
↑(s.topological_closure) = closure ↑s
@[protected, instance]
def
subalgebra.topological_semiring
{R : Type u_1}
[comm_semiring R]
{A : Type u}
[topological_space A]
[semiring A]
[algebra R A]
[topological_semiring A]
(s : subalgebra R A) :
theorem
subalgebra.le_topological_closure
{R : Type u_1}
[comm_semiring R]
{A : Type u}
[topological_space A]
[semiring A]
[algebra R A]
[topological_semiring A]
(s : subalgebra R A) :
s ≤ s.topological_closure
theorem
subalgebra.is_closed_topological_closure
{R : Type u_1}
[comm_semiring R]
{A : Type u}
[topological_space A]
[semiring A]
[algebra R A]
[topological_semiring A]
(s : subalgebra R A) :
theorem
subalgebra.topological_closure_minimal
{R : Type u_1}
[comm_semiring R]
{A : Type u}
[topological_space A]
[semiring A]
[algebra R A]
[topological_semiring A]
(s : subalgebra R A)
{t : subalgebra R A}
(h : s ≤ t)
(ht : is_closed ↑t) :
s.topological_closure ≤ t
def
subalgebra.comm_semiring_topological_closure
{R : Type u_1}
[comm_semiring R]
{A : Type u}
[topological_space A]
[semiring A]
[algebra R A]
[topological_semiring A]
[t2_space A]
(s : subalgebra R A)
(hs : ∀ (x y : ↥s), x * y = y * x) :
If a subalgebra of a topological algebra is commutative, then so is its topological closure.
Equations
- s.comm_semiring_topological_closure hs = {add := semiring.add s.topological_closure.to_semiring, add_assoc := _, zero := semiring.zero s.topological_closure.to_semiring, zero_add := _, add_zero := _, nsmul := semiring.nsmul s.topological_closure.to_semiring, nsmul_zero' := _, nsmul_succ' := _, add_comm := _, mul := semiring.mul s.topological_closure.to_semiring, left_distrib := _, right_distrib := _, zero_mul := _, mul_zero := _, mul_assoc := _, one := semiring.one s.topological_closure.to_semiring, one_mul := _, mul_one := _, nat_cast := semiring.nat_cast s.topological_closure.to_semiring, nat_cast_zero := _, nat_cast_succ := _, npow := semiring.npow s.topological_closure.to_semiring, npow_zero' := _, npow_succ' := _, mul_comm := _}
theorem
subalgebra.topological_closure_comap_homeomorph
{R : Type u_1}
[comm_semiring R]
{A : Type u}
[topological_space A]
[semiring A]
[algebra R A]
[topological_semiring A]
(s : subalgebra R A)
{B : Type u_2}
[topological_space B]
[ring B]
[topological_ring B]
[algebra R B]
(f : B →ₐ[R] A)
(f' : B ≃ₜ A)
(w : ⇑f = ⇑f') :
This is really a statement about topological algebra isomorphisms, but we don't have those, so we use the clunky approach of talking about an algebra homomorphism, and a separate homeomorphism, along with a witness that as functions they are the same.
@[reducible]
def
subalgebra.comm_ring_topological_closure
{R : Type u_1}
[comm_ring R]
{A : Type u}
[topological_space A]
[ring A]
[algebra R A]
[topological_ring A]
[t2_space A]
(s : subalgebra R A)
(hs : ∀ (x y : ↥s), x * y = y * x) :
If a subalgebra of a topological algebra is commutative, then so is its topological closure. See note [reducible non-instances].
Equations
- s.comm_ring_topological_closure hs = {add := ring.add s.topological_closure.to_ring, add_assoc := _, zero := ring.zero s.topological_closure.to_ring, zero_add := _, add_zero := _, nsmul := ring.nsmul s.topological_closure.to_ring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg s.topological_closure.to_ring, sub := ring.sub s.topological_closure.to_ring, sub_eq_add_neg := _, zsmul := ring.zsmul s.topological_closure.to_ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast s.topological_closure.to_ring, nat_cast := ring.nat_cast s.topological_closure.to_ring, one := ring.one s.topological_closure.to_ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul s.topological_closure.to_ring, mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow s.topological_closure.to_ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _}
def
algebra.elemental_algebra
(R : Type u_1)
[comm_ring R]
{A : Type u}
[topological_space A]
[ring A]
[algebra R A]
[topological_ring A]
(x : A) :
subalgebra R A
The topological closure of the subalgebra generated by a single element.
Equations
- algebra.elemental_algebra R x = (algebra.adjoin R {x}).topological_closure
Instances for ↥algebra.elemental_algebra
theorem
algebra.self_mem_elemental_algebra
(R : Type u_1)
[comm_ring R]
{A : Type u}
[topological_space A]
[ring A]
[algebra R A]
[topological_ring A]
(x : A) :
x ∈ algebra.elemental_algebra R x
@[protected, instance]
def
algebra.elemental_algebra.comm_ring
{R : Type u_1}
[comm_ring R]
{A : Type u}
[topological_space A]
[ring A]
[algebra R A]
[topological_ring A]
[t2_space A]
{x : A} :
Equations
- algebra.elemental_algebra.comm_ring = (algebra.adjoin R {x}).comm_ring_topological_closure algebra.elemental_algebra.comm_ring._proof_1
@[protected, instance]
def
division_ring.has_continuous_const_smul_rat
{A : Type u_1}
[division_ring A]
[topological_space A]
[has_continuous_mul A]
[char_zero A] :
The action induced by algebra_rat is continuous.