Mathlib.Topology.Algebra.Algebra

continuous_algebraMap theorem

[ContinuousSMul R A] : Continuous (algebraMap R A)

Full source

@[continuity, fun_prop]
theorem continuous_algebraMap [ContinuousSMul R A] : Continuous (algebraMap R A) := by
  rw [algebraMap_eq_smul_one']
  exact continuous_id.smul continuous_const

Continuity of the Algebra Map in Topological Algebras

Informal description

If $A$ is a topological algebra over a topological semiring $R$ with continuous scalar multiplication, then the algebra map $\text{algebraMap}_R \colon R \to A$ is continuous.

continuous_algebraMap_iff_smul theorem

[ContinuousMul A] : Continuous (algebraMap R A) ↔ Continuous fun p : R × A => p.1 • p.2

Full source

theorem continuous_algebraMap_iff_smul [ContinuousMul A] :
    ContinuousContinuous (algebraMap R A) ↔ Continuous fun p : R × A => p.1 • p.2 := by
  refine ⟨fun h => ?_, fun h => have : ContinuousSMul R A := ⟨h⟩; continuous_algebraMap _ _⟩
  simp only [Algebra.smul_def]
  exact (h.comp continuous_fst).mul continuous_snd

Equivalence of Continuity of Algebra Map and Scalar Multiplication in Topological Algebras

Informal description

For a topological algebra $A$ over a topological semiring $R$ with continuous multiplication, the algebra map $\text{algebraMap}_R \colon R \to A$ is continuous if and only if the scalar multiplication operation $(r, a) \mapsto r \cdot a$ is continuous as a function from $R \times A$ to $A$.

continuousSMul_of_algebraMap theorem

[ContinuousMul A] (h : Continuous (algebraMap R A)) : ContinuousSMul R A

Full source

theorem continuousSMul_of_algebraMap [ContinuousMul A] (h : Continuous (algebraMap R A)) :
    ContinuousSMul R A :=
  ⟨(continuous_algebraMap_iff_smul R A).1 h⟩

Continuity of Scalar Multiplication from Continuity of Algebra Map

Informal description

Let $A$ be a topological algebra over a topological semiring $R$ with continuous multiplication. If the algebra map $\text{algebraMap}_R \colon R \to A$ is continuous, then the scalar multiplication operation $R \times A \to A$ is jointly continuous.

Subalgebra.continuousSMul instance

(S : Subalgebra R A) (X) [TopologicalSpace X] [MulAction A X] [ContinuousSMul A X] : ContinuousSMul S X

Full source

instance Subalgebra.continuousSMul (S : Subalgebra R A) (X) [TopologicalSpace X] [MulAction A X]
    [ContinuousSMul A X] : ContinuousSMul S X :=
  Subsemiring.continuousSMul S.toSubsemiring X

Continuous Scalar Multiplication on Subalgebras

Informal description

For any topological algebra $A$ over a topological semiring $R$, and any subalgebra $S$ of $A$, the scalar multiplication operation $S \times X \to X$ is continuous for any topological space $X$ with a continuous multiplicative action of $A$.

algebraMapCLM definition

: R →L[R] A

Full source

/-- The inclusion of the base ring in a topological algebra as a continuous linear map. -/
@[simps]
def algebraMapCLM : R →L[R] A :=
  { Algebra.linearMap R A with
    toFun := algebraMap R A
    cont := continuous_algebraMap R A }

Continuous linear algebra map

Informal description

The canonical inclusion map from a topological semiring $R$ to a topological algebra $A$ over $R$, viewed as a continuous linear map. This map sends each element $r \in R$ to its image under the algebra map $\text{algebraMap}_R \colon R \to A$, and is continuous when $A$ has continuous scalar multiplication over $R$.

algebraMapCLM_coe theorem

: ⇑(algebraMapCLM R A) = algebraMap R A

Full source

theorem algebraMapCLM_coe : ⇑(algebraMapCLM R A) = algebraMap R A :=
  rfl

Equality of Continuous Linear Algebra Map and Algebra Map

Informal description

The underlying function of the continuous linear algebra map from $R$ to $A$ coincides with the algebra map from $R$ to $A$, i.e., $\text{algebraMapCLM}_{R,A}(r) = \text{algebraMap}_R(r)$ for all $r \in R$.

algebraMapCLM_toLinearMap theorem

: (algebraMapCLM R A).toLinearMap = Algebra.linearMap R A

Full source

theorem algebraMapCLM_toLinearMap : (algebraMapCLM R A).toLinearMap = Algebra.linearMap R A :=
  rfl

Equality of Underlying Linear Maps: $\text{algebraMapCLM}_{R,A}.toLinearMap = \text{Algebra.linearMap}_{R,A}$

Informal description

The underlying linear map of the continuous linear algebra map from $R$ to $A$ is equal to the algebra linear map from $R$ to $A$. In other words, if we forget the topology and consider only the linear structure, the continuous linear algebra map $\text{algebraMapCLM}_{R,A}$ coincides with the algebraic linear map $\text{Algebra.linearMap}_{R,A}$.

DiscreteTopology.instContinuousSMul theorem

[IsTopologicalSemiring A] [DiscreteTopology R] : ContinuousSMul R A

Full source

/-- If `R` is a discrete topological ring, then any topological ring `S` which is an `R`-algebra
is also a topological `R`-algebra.

NB: This could be an instance but the signature makes it very expensive in search.
See https://github.com/leanprover-community/mathlib4/pull/15339
for the regressions caused by making this an instance. -/
theorem DiscreteTopology.instContinuousSMul [IsTopologicalSemiring A] [DiscreteTopology R] :
    ContinuousSMul R A := continuousSMul_of_algebraMap _ _ continuous_of_discreteTopology

Continuity of Scalar Multiplication for Discrete Topological Semiring $R$

Informal description

Let $R$ be a topological semiring with the discrete topology and $A$ be a topological semiring. Then the scalar multiplication operation $R \times A \to A$ is jointly continuous, making $A$ a topological $R$-algebra.

ContinuousAlgHom structure

(R : Type*) [CommSemiring R] (A : Type*) [Semiring A]
    [TopologicalSpace A] (B : Type*) [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B]
    extends A →ₐ[R] B

Full source

/-- Continuous algebra homomorphisms between algebras. We only put the type classes that are
necessary for the definition, although in applications `M` and `B` will be topological algebras
over the topological ring `R`. -/
structure ContinuousAlgHom (R : Type*) [CommSemiring R] (A : Type*) [Semiring A]
    [TopologicalSpace A] (B : Type*) [Semiring B] [TopologicalSpace B] [Algebra R A] [Algebra R B]
    extends A →ₐ[R] B where
-- TODO: replace with `fun_prop` when that is stable
  cont : Continuous toFun := by continuity

Continuous Algebra Homomorphism

Informal description

The structure representing continuous algebra homomorphisms between topological algebras over a commutative semiring $ R $. A continuous algebra homomorphism from $ A $ to $ B $ is an algebra homomorphism (i.e., a map preserving both the ring and module structures) that is also continuous. Here, $ A $ and $ B $ are topological semirings equipped with an algebra structure over $ R $.

term_→A[_]_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
notation:25 A " →A[" R "] " B => ContinuousAlgHom R A B

Continuous algebra homomorphisms

Informal description

The notation $ A \to_A[R] B $ denotes the type of continuous algebra homomorphisms from the topological $ R $-algebra $ A $ to the topological $ R $-algebra $ B $. These are algebra homomorphisms that are also continuous maps between the underlying topological spaces.

ContinuousAlgHom.instFunLike instance

: FunLike (A →A[R] B) A B

Full source

instance : FunLike (A →A[R] B) A B where
  coe f := f.toAlgHom
  coe_injective'  f g h  := by
    cases f; cases g
    simp only [mk.injEq]
    exact AlgHom.ext (congrFun h)

Function-like Structure of Continuous Algebra Homomorphisms

Informal description

For topological algebras $A$ and $B$ over a commutative semiring $R$, the set of continuous algebra homomorphisms $A \to_{A[R]} B$ forms a function-like structure, meaning it can be treated as a collection of functions from $A$ to $B$.

ContinuousAlgHom.instAlgHomClass instance

: AlgHomClass (A →A[R] B) R A B

Full source

instance : AlgHomClass (A →A[R] B) R A B where
  map_mul f x y    := map_mul f.toAlgHom x y
  map_one f        := map_one f.toAlgHom
  map_add f        := map_add f.toAlgHom
  map_zero f       := map_zero f.toAlgHom
  commutes f r     := f.toAlgHom.commutes r

Algebra Homomorphism Class Structure on Continuous Algebra Homomorphisms

Informal description

The set of continuous algebra homomorphisms $A \to_{A[R]} B$ between topological $R$-algebras $A$ and $B$ forms an algebra homomorphism class, meaning it inherits all the algebraic structure-preserving properties of algebra homomorphisms while also being continuous.

ContinuousAlgHom.toAlgHom_eq_coe theorem

(f : A →A[R] B) : f.toAlgHom = f

Full source

@[simp]
theorem toAlgHom_eq_coe (f : A →A[R] B) : f.toAlgHom = f := rfl

Underlying Algebra Homomorphism of Continuous Algebra Homomorphism

Informal description

For any continuous algebra homomorphism $f \colon A \to_{A[R]} B$ between topological $R$-algebras, the underlying algebra homomorphism of $f$ is equal to $f$ itself when viewed as a function.

ContinuousAlgHom.coe_inj theorem

{f g : A →A[R] B} : (f : A →ₐ[R] B) = g ↔ f = g

Full source

@[simp, norm_cast]
theorem coe_inj {f g : A →A[R] B} : (f : A →ₐ[R] B) = g ↔ f = g :=   by
  cases f; cases g; simp only [mk.injEq]; exact Eq.congr_right rfl

Injective Correspondence Between Continuous Algebra Homomorphisms and Their Underlying Algebra Homomorphisms

Informal description

For any two continuous algebra homomorphisms $f, g \colon A \to_{A[R]} B$ between topological $R$-algebras $A$ and $B$, the underlying algebra homomorphisms of $f$ and $g$ are equal if and only if $f$ and $g$ are equal as continuous algebra homomorphisms.

ContinuousAlgHom.coe_mk theorem

(f : A →ₐ[R] B) (h) : (mk f h : A →ₐ[R] B) = f

Full source

@[simp]
theorem coe_mk (f : A →ₐ[R] B) (h) : (mk f h : A →ₐ[R] B) = f := rfl

Underlying Algebra Homomorphism of Continuous Algebra Homomorphism Construction

Informal description

Given an algebra homomorphism $f \colon A \to_{A[R]} B$ and a proof $h$ that $f$ is continuous, the underlying algebra homomorphism of the continuous algebra homomorphism constructed from $f$ and $h$ is equal to $f$ itself.

ContinuousAlgHom.coe_mk' theorem

(f : A →ₐ[R] B) (h) : (mk f h : A → B) = f

Full source

@[simp]
theorem coe_mk' (f : A →ₐ[R] B) (h) : (mk f h : A → B) = f := rfl

Underlying Function of Continuous Algebra Homomorphism Construction

Informal description

For any continuous algebra homomorphism $f \colon A \to_{A[R]} B$ constructed from an algebra homomorphism $f \colon A \toₐ[R] B$ and a continuity proof $h$, the underlying function of the continuous algebra homomorphism equals $f$.

ContinuousAlgHom.coe_coe theorem

(f : A →A[R] B) : ⇑(f : A →ₐ[R] B) = f

Full source

@[simp, norm_cast]
theorem coe_coe (f : A →A[R] B) : ⇑(f : A →ₐ[R] B) = f := rfl

Underlying Function Equality for Continuous Algebra Homomorphisms

Informal description

For any continuous algebra homomorphism $f \colon A \to_{A[R]} B$ between topological $R$-algebras $A$ and $B$, the underlying function of $f$ (when viewed as an algebra homomorphism) is equal to $f$ itself.

ContinuousAlgHom.instContinuousMapClass instance

: ContinuousMapClass (A →A[R] B) A B

Full source

instance : ContinuousMapClass (A →A[R] B) A B where
  map_continuous f := f.2

Continuous Algebra Homomorphisms as Continuous Maps

Informal description

The set of continuous algebra homomorphisms $A \to_{A[R]} B$ between topological algebras $A$ and $B$ over a commutative semiring $R$ forms a continuous map class, meaning each homomorphism is continuous as a function from $A$ to $B$.

ContinuousAlgHom.continuous theorem

(f : A →A[R] B) : Continuous f

Full source

@[fun_prop]
protected theorem continuous (f : A →A[R] B) : Continuous f := f.2

Continuity of Continuous Algebra Homomorphisms

Informal description

For any continuous algebra homomorphism $f \colon A \to_{A[R]} B$ between topological algebras $A$ and $B$ over a commutative semiring $R$, the function $f$ is continuous.

ContinuousAlgHom.uniformContinuous theorem

 {E₁ E₂ : Type*} [UniformSpace E₁] [UniformSpace E₂] [Ring E₁] [Ring E₂] [Algebra R E₁] [Algebra R E₂]
  [IsUniformAddGroup E₁] [IsUniformAddGroup E₂] (f : E₁ →A[R] E₂) : UniformContinuous f

Full source

protected theorem uniformContinuous {E₁ E₂ : Type*} [UniformSpace E₁] [UniformSpace E₂]
    [Ring E₁] [Ring E₂] [Algebra R E₁] [Algebra R E₂] [IsUniformAddGroup E₁]
    [IsUniformAddGroup E₂] (f : E₁ →A[R] E₂) : UniformContinuous f :=
  uniformContinuous_addMonoidHom_of_continuous f.continuous

Uniform Continuity of Continuous Algebra Homomorphisms on Uniform Additive Groups

Informal description

Let $E₁$ and $E₂$ be uniform spaces equipped with ring structures and algebra structures over a commutative semiring $R$, such that both $E₁$ and $E₂$ are uniform additive groups. For any continuous algebra homomorphism $f \colon E₁ \to_{A[R]} E₂$, the function $f$ is uniformly continuous.

ContinuousAlgHom.Simps.apply definition

(h : A →A[R] B) : A → B

Full source

/-- See Note [custom simps projection]. We need to specify this projection explicitly in this case,
because it is a composition of multiple projections. -/
def Simps.apply (h : A →A[R] B) : A → B := h

Underlying function of a continuous algebra homomorphism

Informal description

The function that extracts the underlying function from a continuous algebra homomorphism $ h : A \to_{A[R]} B $, mapping elements of $ A $ to elements of $ B $.

ContinuousAlgHom.Simps.coe definition

(h : A →A[R] B) : A →ₐ[R] B

Full source

/-- See Note [custom simps projection]. -/
def Simps.coe (h : A →A[R] B) : A →ₐ[R] B := h

Underlying algebra homomorphism of a continuous algebra homomorphism

Informal description

The function that extracts the underlying algebra homomorphism from a continuous algebra homomorphism $ h : A \to_{A[R]} B $, mapping elements of $ A $ to elements of $ B $ while preserving the algebraic structure over $ R $.

ContinuousAlgHom.ext theorem

{f g : A →A[R] B} (h : ∀ x, f x = g x) : f = g

Full source

@[ext]
theorem ext {f g : A →A[R] B} (h : ∀ x, f x = g x) : f = g := DFunLike.ext f g h

Extensionality of Continuous Algebra Homomorphisms

Informal description

For any two continuous algebra homomorphisms $f, g : A \to_{A[R]} B$ between topological algebras over a commutative semiring $R$, if $f(x) = g(x)$ for all $x \in A$, then $f = g$.

ContinuousAlgHom.copy definition

(f : A →A[R] B) (f' : A → B) (h : f' = ⇑f) : A →A[R] B

Full source

/-- Copy of a `ContinuousAlgHom` with a new `toFun` equal to the old one. Useful to fix
definitional equalities. -/
def copy (f : A →A[R] B) (f' : A → B) (h : f' = ⇑f) : A →A[R] B where
  toAlgHom := {
    toRingHom := (f : A →A[R] B).toRingHom.copy f' h
    commutes' := fun r => by
      simp only [AlgHom.toRingHom_eq_coe, h, RingHom.toMonoidHom_eq_coe, OneHom.toFun_eq_coe,
        MonoidHom.toOneHom_coe, MonoidHom.coe_coe, RingHom.coe_copy, AlgHomClass.commutes f r] }
  cont := show Continuous f' from h.symm ▸ f.continuous

Copy of a continuous algebra homomorphism with a new function

Informal description

Given a continuous algebra homomorphism $ f : A \to_{A[R]} B $ between topological algebras over a commutative semiring $ R $, and a function $ f' : A \to B $ that is definitionally equal to $ f $, the function `ContinuousAlgHom.copy` constructs a new continuous algebra homomorphism with the underlying function $ f' $. This preserves all the algebraic and topological properties of $ f $.

ContinuousAlgHom.coe_copy theorem

(f : A →A[R] B) (f' : A → B) (h : f' = ⇑f) : ⇑(f.copy f' h) = f'

Full source

@[simp]
theorem coe_copy (f : A →A[R] B) (f' : A → B) (h : f' = ⇑f) : ⇑(f.copy f' h) = f' := rfl

Underlying Function of Copied Continuous Algebra Homomorphism

Informal description

For any continuous algebra homomorphism $f \colon A \to_{A[R]} B$ between topological algebras over a commutative semiring $R$, and any function $f' \colon A \to B$ such that $f' = f$, the underlying function of the copied homomorphism $f.copy\ f'\ h$ is equal to $f'$.

ContinuousAlgHom.copy_eq theorem

(f : A →A[R] B) (f' : A → B) (h : f' = ⇑f) : f.copy f' h = f

Full source

theorem copy_eq (f : A →A[R] B) (f' : A → B) (h : f' = ⇑f) : f.copy f' h = f := DFunLike.ext' h

Equality of Copied Continuous Algebra Homomorphism

Informal description

Let $A$ and $B$ be topological algebras over a commutative semiring $R$, and let $f : A \to_{A[R]} B$ be a continuous algebra homomorphism. For any function $f' : A \to B$ such that $f' = f$, the copied homomorphism $f.copy\ f'\ h$ is equal to $f$.

ContinuousAlgHom.map_zero theorem

(f : A →A[R] B) : f (0 : A) = 0

Full source

protected theorem map_zero (f : A →A[R] B) : f (0 : A) = 0 := map_zero f

Preservation of Zero by Continuous Algebra Homomorphisms

Informal description

For any continuous algebra homomorphism $f \colon A \to_{A[R]} B$ between topological $R$-algebras $A$ and $B$, the image of the zero element $0 \in A$ under $f$ is the zero element $0 \in B$, i.e., $f(0) = 0$.

ContinuousAlgHom.map_add theorem

(f : A →A[R] B) (x y : A) : f (x + y) = f x + f y

Full source

protected theorem map_add (f : A →A[R] B) (x y : A) : f (x + y) = f x + f y := map_add f x y

Additivity of Continuous Algebra Homomorphisms

Informal description

For any continuous algebra homomorphism $f \colon A \to_{A[R]} B$ between topological $R$-algebras $A$ and $B$, and for any elements $x, y \in A$, we have $f(x + y) = f(x) + f(y)$.

ContinuousAlgHom.map_smul theorem

(f : A →A[R] B) (c : R) (x : A) : f (c • x) = c • f x

Full source

protected theorem map_smul (f : A →A[R] B) (c : R) (x : A) :
    f (c • x) = c • f x :=
  map_smul ..

Scalar Multiplication Preservation by Continuous Algebra Homomorphisms

Informal description

For any continuous algebra homomorphism $f \colon A \to_{A[R]} B$ between topological $R$-algebras $A$ and $B$, any scalar $c \in R$, and any element $x \in A$, we have $f(c \cdot x) = c \cdot f(x)$.

ContinuousAlgHom.map_smul_of_tower theorem

 {R S : Type*} [CommSemiring S] [SMul R A] [Algebra S A] [SMul R B] [Algebra S B] [MulActionHomClass (A →A[S] B) R A B]
  (f : A →A[S] B) (c : R) (x : A) : f (c • x) = c • f x

Full source

theorem map_smul_of_tower {R S : Type*} [CommSemiring S] [SMul R A] [Algebra S A] [SMul R B]
    [Algebra S B] [MulActionHomClass (A →A[S] B) R A B] (f : A →A[S] B) (c : R) (x : A) :
    f (c • x) = c • f x :=
  map_smul f c x

Scalar Multiplication Preservation by Continuous Algebra Homomorphisms

Informal description

Let $R$ and $S$ be types with $S$ a commutative semiring. Suppose $A$ and $B$ are topological algebras over $S$ with scalar multiplication by $R$ on both $A$ and $B$. For any continuous $S$-algebra homomorphism $f : A \to_{A[S]} B$, scalar $c \in R$, and element $x \in A$, we have $f(c \cdot x) = c \cdot f(x)$.

ContinuousAlgHom.map_sum theorem

{ι : Type*} (f : A →A[R] B) (s : Finset ι) (g : ι → A) : f (∑ i ∈ s, g i) = ∑ i ∈ s, f (g i)

Full source

protected theorem map_sum {ι : Type*} (f : A →A[R] B) (s : Finset ι) (g : ι → A) :
    f (∑ i ∈ s, g i) = ∑ i ∈ s, f (g i) :=
  map_sum ..

Continuous Algebra Homomorphism Preserves Finite Sums

Informal description

Let $A$ and $B$ be topological algebras over a commutative semiring $R$, and let $f : A \to_{A[R]} B$ be a continuous algebra homomorphism. For any finite index set $\iota$, finite subset $s \subseteq \iota$, and function $g : \iota \to A$, we have: \[ f\left(\sum_{i \in s} g(i)\right) = \sum_{i \in s} f(g(i)). \]

ContinuousAlgHom.ext_ring theorem

[TopologicalSpace R] {f g : R →A[R] A} : f = g

Full source

/-- Any two continuous `R`-algebra morphisms from `R` are equal -/
@[ext (iff := false)]
theorem ext_ring [TopologicalSpace R] {f g : R →A[R] A} : f = g :=
  coe_inj.mp (ext_id _ _ _)

Uniqueness of Continuous Algebra Homomorphisms from $R$ to $A$

Informal description

Let $R$ be a topological space equipped with a commutative semiring structure, and let $A$ be a topological algebra over $R$. For any two continuous $R$-algebra homomorphisms $f, g \colon R \to_{A[R]} A$, we have $f = g$.

ContinuousAlgHom.ext_ring_iff theorem

[TopologicalSpace R] {f g : R →A[R] A} : f = g ↔ f 1 = g 1

Full source

theorem ext_ring_iff [TopologicalSpace R] {f g : R →A[R] A} : f = g ↔ f 1 = g 1 :=
  ⟨fun h => h ▸ rfl, fun _ => ext_ring ⟩

Uniqueness of Continuous Algebra Homomorphisms via Unit Condition

Informal description

Let $R$ be a topological space equipped with a commutative semiring structure, and let $A$ be a topological algebra over $R$. For any two continuous $R$-algebra homomorphisms $f, g \colon R \to_{A[R]} A$, we have $f = g$ if and only if $f(1) = g(1)$.

ContinuousAlgHom.eqOn_closure_adjoin theorem

[T2Space B] {s : Set A} {f g : A →A[R] B} (h : Set.EqOn f g s) : Set.EqOn f g (closure (Algebra.adjoin R s : Set A))

Full source

/-- If two continuous algebra maps are equal on a set `s`, then they are equal on the closure
of the `Algebra.adjoin` of this set. -/
theorem eqOn_closure_adjoin [T2Space B] {s : Set A} {f g : A →A[R] B} (h : Set.EqOn f g s) :
    Set.EqOn f g (closure (Algebra.adjoin R s : Set A)) :=
  Set.EqOn.closure (AlgHom.eqOn_adjoin_iff.mpr h) f.continuous g.continuous

Agreement of Continuous Algebra Homomorphisms on Closure of Generated Subalgebra

Informal description

Let $A$ and $B$ be topological algebras over a commutative semiring $R$, with $B$ being a Hausdorff space. Given two continuous algebra homomorphisms $f, g \colon A \to_{A[R]} B$ that agree on a subset $s \subseteq A$, then $f$ and $g$ also agree on the topological closure of the algebra generated by $s$ in $A$.

ContinuousAlgHom.ext_on theorem

[T2Space B] {s : Set A} (hs : Dense (Algebra.adjoin R s : Set A)) {f g : A →A[R] B} (h : Set.EqOn f g s) : f = g

Full source

/-- If the subalgebra generated by a set `s` is dense in the ambient module, then two continuous
algebra maps equal on `s` are equal. -/
theorem ext_on [T2Space B] {s : Set A} (hs : Dense (Algebra.adjoin R s : Set A))
    {f g : A →A[R] B} (h : Set.EqOn f g s) : f = g :=
  ext fun x => eqOn_closure_adjoin h (hs x)

Uniqueness of Continuous Algebra Homomorphisms via Dense Generator

Informal description

Let $A$ and $B$ be topological algebras over a commutative semiring $R$, with $B$ being a Hausdorff space. If the subalgebra generated by a subset $s \subseteq A$ is dense in $A$, then any two continuous algebra homomorphisms $f, g \colon A \to_{A[R]} B$ that agree on $s$ must be equal.

Subalgebra.topologicalClosure definition

(s : Subalgebra R A) : Subalgebra R A

Full source

/-- The topological closure of a subalgebra -/
def _root_.Subalgebra.topologicalClosure (s : Subalgebra R A) : Subalgebra R A where
  toSubsemiring := s.toSubsemiring.topologicalClosure
  algebraMap_mem' r := by
    simp only [Subsemiring.coe_carrier_toSubmonoid, Subsemiring.topologicalClosure_coe,
      Subalgebra.coe_toSubsemiring]
    apply subset_closure
    exact algebraMap_mem s r

Topological closure of a subalgebra

Informal description

Given a topological algebra $A$ over a topological semiring $R$ and a subalgebra $s$ of $A$, the topological closure of $s$ is the smallest subalgebra of $A$ containing $s$ that is closed in the topology of $A$. It is constructed by taking the topological closure of the underlying subsemiring of $s$ and ensuring it remains closed under the algebra map from $R$.

Subalgebra.topologicalClosure_map theorem

 [IsTopologicalSemiring B] (f : A →A[R] B) (s : Subalgebra R A) :
  s.topologicalClosure.map f ≤ (s.map f.toAlgHom).topologicalClosure

Full source

/-- Under a continuous algebra map, the image of the `TopologicalClosure` of a subalgebra is
contained in the `TopologicalClosure` of its image. -/
theorem _root_.Subalgebra.topologicalClosure_map
    [IsTopologicalSemiring B] (f : A →A[R] B) (s : Subalgebra R A) :
    s.topologicalClosure.map f ≤ (s.map f.toAlgHom).topologicalClosure :=
  image_closure_subset_closure_image f.continuous

Image of Subalgebra Closure under Continuous Algebra Homomorphism is Contained in Closure of Image

Informal description

Let $A$ and $B$ be topological algebras over a commutative semiring $R$, with $B$ being a topological semiring. For any continuous algebra homomorphism $f \colon A \to_{A[R]} B$ and any subalgebra $s$ of $A$, the image of the topological closure of $s$ under $f$ is contained in the topological closure of the image of $s$ under $f$. In other words, $f(\overline{s}) \subseteq \overline{f(s)}$.

Subalgebra.topologicalClosure_coe theorem

(s : Subalgebra R A) : (s.topologicalClosure : Set A) = closure ↑s

Full source

@[simp]
theorem _root_.Subalgebra.topologicalClosure_coe
    (s : Subalgebra R A) :
  (s.topologicalClosure : Set A) = closure ↑s := rfl

Topological Closure of Subalgebra as Set Closure

Informal description

For any subalgebra $s$ of a topological algebra $A$ over a topological semiring $R$, the underlying set of the topological closure of $s$ is equal to the topological closure of the underlying set of $s$ in $A$. That is, $\overline{s} = \overline{s}$ as sets, where the left-hand side is the topological closure as a subalgebra and the right-hand side is the topological closure in the ambient space $A$.

DenseRange.topologicalClosure_map_subalgebra theorem

 [IsTopologicalSemiring B] {f : A →A[R] B} (hf' : DenseRange f) {s : Subalgebra R A} (hs : s.topologicalClosure = ⊤) :
  (s.map (f : A →ₐ[R] B)).topologicalClosure = ⊤

Full source

/-- Under a dense continuous algebra map, a subalgebra
whose `TopologicalClosure` is `⊤` is sent to another such submodule.
That is, the image of a dense subalgebra under a map with dense range is dense.
-/
theorem _root_.DenseRange.topologicalClosure_map_subalgebra
    [IsTopologicalSemiring B] {f : A →A[R] B} (hf' : DenseRange f) {s : Subalgebra R A}
    (hs : s.topologicalClosure = ⊤) : (s.map (f : A →ₐ[R] B)).topologicalClosure = ⊤ := by
  rw [SetLike.ext'_iff] at hs ⊢
  simp only [Subalgebra.topologicalClosure_coe, coe_top, ← dense_iff_closure_eq, Subalgebra.coe_map,
    AlgHom.coe_coe] at hs ⊢
  exact hf'.dense_image f.continuous hs

Density Preservation under Continuous Algebra Homomorphisms with Dense Range

Informal description

Let $A$ and $B$ be topological algebras over a commutative semiring $R$, with $B$ being a topological semiring. Given a continuous algebra homomorphism $f \colon A \to_{A[R]} B$ with dense range, and a subalgebra $s$ of $A$ whose topological closure is the entire algebra $A$, then the topological closure of the image subalgebra $f(s)$ is the entire algebra $B$. In other words, if $\overline{s} = A$ and $f$ has dense range, then $\overline{f(s)} = B$.

ContinuousAlgHom.id definition

: A →A[R] A

Full source

/-- The identity map as a continuous algebra homomorphism. -/
protected def id : A →A[R] A := ⟨AlgHom.id R A, continuous_id⟩

Identity continuous algebra homomorphism

Informal description

The identity map from a topological algebra $ A $ over a commutative semiring $ R $ to itself, viewed as a continuous algebra homomorphism.

ContinuousAlgHom.instOne instance

: One (A →A[R] A)

Full source

instance : One (A →A[R] A) := ⟨ContinuousAlgHom.id R A⟩

Identity Continuous Algebra Homomorphism as One

Informal description

For any topological algebra $A$ over a commutative semiring $R$, the set of continuous algebra homomorphisms from $A$ to itself has a distinguished element, the identity map, which serves as the multiplicative identity.

ContinuousAlgHom.one_def theorem

: (1 : A →A[R] A) = ContinuousAlgHom.id R A

Full source

theorem one_def : (1 : A →A[R] A) = ContinuousAlgHom.id R A := rfl

Identity as One in Continuous Algebra Homomorphisms

Informal description

The multiplicative identity element in the set of continuous algebra homomorphisms from a topological algebra $A$ over a commutative semiring $R$ to itself is equal to the identity continuous algebra homomorphism on $A$, i.e., $1 = \text{id}_A$.

ContinuousAlgHom.id_apply theorem

(x : A) : ContinuousAlgHom.id R A x = x

Full source

theorem id_apply (x : A) : ContinuousAlgHom.id R A x = x := rfl

Identity Continuous Algebra Homomorphism Acts as Identity

Informal description

For any element $x$ in a topological algebra $A$ over a commutative semiring $R$, the identity continuous algebra homomorphism evaluated at $x$ equals $x$, i.e., $\text{id}(x) = x$.

ContinuousAlgHom.coe_id theorem

: ((ContinuousAlgHom.id R A) : A →ₐ[R] A) = AlgHom.id R A

Full source

@[simp, norm_cast]
theorem coe_id : ((ContinuousAlgHom.id R A) : A →ₐ[R] A) = AlgHom.id R A:= rfl

Identity Continuous Algebra Homomorphism as Algebra Homomorphism

Informal description

The underlying algebra homomorphism of the identity continuous algebra homomorphism from a topological algebra $A$ over a commutative semiring $R$ to itself is equal to the identity algebra homomorphism on $A$.

ContinuousAlgHom.coe_id' theorem

: ⇑(ContinuousAlgHom.id R A) = _root_.id

Full source

@[simp, norm_cast]
theorem coe_id' : ⇑(ContinuousAlgHom.id R A ) = _root_.id := rfl

Identity Continuous Algebra Homomorphism Equals Identity Function

Informal description

The underlying function of the identity continuous algebra homomorphism from a topological algebra $A$ over a commutative semiring $R$ to itself is equal to the identity function on $A$, i.e., $\text{id}_{A \to_{A[R]} A} = \text{id}_A$.

ContinuousAlgHom.coe_eq_id theorem

{f : A →A[R] A} : (f : A →ₐ[R] A) = AlgHom.id R A ↔ f = ContinuousAlgHom.id R A

Full source

@[simp, norm_cast]
theorem coe_eq_id {f : A →A[R] A} :
    (f : A →ₐ[R] A) = AlgHom.id R A ↔ f = ContinuousAlgHom.id R A:= by
  rw [← coe_id, coe_inj]

Identity Characterization for Continuous Algebra Homomorphisms

Informal description

For any continuous algebra homomorphism $f \colon A \to_{A[R]} A$ between topological $R$-algebras, the underlying algebra homomorphism of $f$ is equal to the identity algebra homomorphism if and only if $f$ is equal to the identity continuous algebra homomorphism.

ContinuousAlgHom.one_apply theorem

(x : A) : (1 : A →A[R] A) x = x

Full source

@[simp]
theorem one_apply (x : A) : (1 : A →A[R] A) x = x := rfl

Identity Continuous Algebra Homomorphism Acts as Identity Function

Informal description

For any element $x$ in a topological algebra $A$ over a commutative semiring $R$, the identity continuous algebra homomorphism evaluated at $x$ equals $x$, i.e., $1(x) = x$.

ContinuousAlgHom.comp definition

(g : B →A[R] C) (f : A →A[R] B) : A →A[R] C

Full source

/-- Composition of continuous algebra homomorphisms. -/
def comp (g : B →A[R] C) (f : A →A[R] B) : A →A[R] C :=
  ⟨(g : B →ₐ[R] C).comp (f : A →ₐ[R] B), g.2.comp f.2⟩

Composition of continuous algebra homomorphisms

Informal description

Given continuous algebra homomorphisms $ f \colon A \to_{A[R]} B $ and $ g \colon B \to_{A[R]} C $, the composition $ g \circ f $ is a continuous algebra homomorphism from $ A $ to $ C $. Here, $ A $, $ B $, and $ C $ are topological algebras over a commutative semiring $ R $, and the composition preserves both the algebraic structure and continuity.

ContinuousAlgHom.coe_comp theorem

(h : B →A[R] C) (f : A →A[R] B) : (h.comp f : A →ₐ[R] C) = (h : B →ₐ[R] C).comp (f : A →ₐ[R] B)

Full source

@[simp, norm_cast]
theorem coe_comp (h : B →A[R] C) (f : A →A[R] B) :
    (h.comp f : A →ₐ[R] C) = (h : B →ₐ[R] C).comp (f : A →ₐ[R] B) := rfl

Compatibility of Composition with Underlying Algebra Homomorphisms

Informal description

For continuous algebra homomorphisms $f \colon A \to_{A[R]} B$ and $h \colon B \to_{A[R]} C$ between topological $R$-algebras, the underlying algebra homomorphism of the composition $h \circ f$ is equal to the composition of the underlying algebra homomorphisms of $h$ and $f$. That is, $(h \circ f : A \toₐ[R] C) = (h : B \toₐ[R] C) \circ (f : A \toₐ[R] B)$.

ContinuousAlgHom.coe_comp' theorem

(h : B →A[R] C) (f : A →A[R] B) : ⇑(h.comp f) = h ∘ f

Full source

@[simp, norm_cast]
theorem coe_comp' (h : B →A[R] C) (f : A →A[R] B) : ⇑(h.comp f) = h ∘ f := rfl

Composition of Underlying Functions in Continuous Algebra Homomorphisms

Informal description

For any continuous algebra homomorphisms $ f \colon A \to_{A[R]} B $ and $ h \colon B \to_{A[R]} C $, the underlying function of the composition $ h \circ f $ is equal to the composition of the underlying functions $ h \circ f $.

ContinuousAlgHom.comp_apply theorem

(g : B →A[R] C) (f : A →A[R] B) (x : A) : (g.comp f) x = g (f x)

Full source

theorem comp_apply (g : B →A[R] C) (f : A →A[R] B) (x : A) : (g.comp f) x = g (f x) := rfl

Composition of Continuous Algebra Homomorphisms Evaluates Pointwise as $ (g \circ f)(x) = g(f(x)) $

Informal description

For any continuous algebra homomorphisms $ f \colon A \to_{A[R]} B $ and $ g \colon B \to_{A[R]} C $, and any element $ x \in A $, the composition $ g \circ f $ evaluated at $ x $ equals $ g $ evaluated at $ f(x) $, i.e., $(g \circ f)(x) = g(f(x))$.

ContinuousAlgHom.comp_id theorem

(f : A →A[R] B) : f.comp (ContinuousAlgHom.id R A) = f

Full source

@[simp]
theorem comp_id (f : A →A[R] B) : f.comp (ContinuousAlgHom.id R A) = f :=
  ext fun _x => rfl

Right identity law for composition of continuous algebra homomorphisms

Informal description

For any continuous algebra homomorphism $f \colon A \to_{A[R]} B$ between topological algebras over a commutative semiring $R$, the composition of $f$ with the identity continuous algebra homomorphism on $A$ is equal to $f$, i.e., $f \circ \mathrm{id}_A = f$.

ContinuousAlgHom.id_comp theorem

(f : A →A[R] B) : (ContinuousAlgHom.id R B).comp f = f

Full source

@[simp]
theorem id_comp (f : A →A[R] B) : (ContinuousAlgHom.id R B).comp f = f :=
  ext fun _x => rfl

Identity Continuous Algebra Homomorphism Left Composition Law

Informal description

For any continuous algebra homomorphism $f \colon A \to_{A[R]} B$ between topological algebras over a commutative semiring $R$, the composition of the identity homomorphism on $B$ with $f$ equals $f$, i.e., $\mathrm{id}_B \circ f = f$.

ContinuousAlgHom.comp_assoc theorem

 {D : Type*} [Semiring D] [Algebra R D] [TopologicalSpace D] (h : C →A[R] D) (g : B →A[R] C) (f : A →A[R] B) :
  (h.comp g).comp f = h.comp (g.comp f)

Full source

theorem comp_assoc {D : Type*} [Semiring D] [Algebra R D] [TopologicalSpace D] (h : C →A[R] D)
    (g : B →A[R] C) (f : A →A[R] B) : (h.comp g).comp f = h.comp (g.comp f) :=
  rfl

Associativity of Composition of Continuous Algebra Homomorphisms

Informal description

For any continuous algebra homomorphisms $f \colon A \to_{A[R]} B$, $g \colon B \to_{A[R]} C$, and $h \colon C \to_{A[R]} D$ between topological algebras over a commutative semiring $R$, the composition operation is associative, i.e., $(h \circ g) \circ f = h \circ (g \circ f)$.

ContinuousAlgHom.instMul instance

: Mul (A →A[R] A)

Full source

instance : Mul (A →A[R] A) := ⟨comp⟩

Multiplication on Continuous Algebra Endomorphisms by Composition

Informal description

For any topological algebra $A$ over a commutative semiring $R$, the set of continuous algebra homomorphisms from $A$ to itself is equipped with a multiplication operation given by composition of maps.

ContinuousAlgHom.mul_def theorem

(f g : A →A[R] A) : f * g = f.comp g

Full source

theorem mul_def (f g : A →A[R] A) : f * g = f.comp g := rfl

Product of Continuous Algebra Endomorphisms is Composition

Informal description

For any continuous algebra homomorphisms $f, g \colon A \to_{A[R]} A$ on a topological algebra $A$ over a commutative semiring $R$, the product $f * g$ is equal to the composition $f \circ g$.

ContinuousAlgHom.coe_mul theorem

(f g : A →A[R] A) : ⇑(f * g) = f ∘ g

Full source

@[simp]
theorem coe_mul (f g : A →A[R] A) : ⇑(f * g) = f ∘ g := rfl

Composition of Continuous Algebra Endomorphisms via Multiplication

Informal description

For any continuous algebra homomorphisms $f, g : A \to_{A[R]} A$ between topological algebras over a commutative semiring $R$, the underlying function of the product $f * g$ is equal to the composition $f \circ g$.

ContinuousAlgHom.mul_apply theorem

(f g : A →A[R] A) (x : A) : (f * g) x = f (g x)

Full source

theorem mul_apply (f g : A →A[R] A) (x : A) : (f * g) x = f (g x) := rfl

Evaluation of Composition of Continuous Algebra Homomorphisms: $(f * g)(x) = f(g(x))$

Informal description

For any continuous algebra homomorphisms $f, g \colon A \to_{A[R]} A$ and any element $x \in A$, the evaluation of the product $f * g$ at $x$ is equal to the composition $f(g(x))$.

ContinuousAlgHom.instMonoid instance

: Monoid (A →A[R] A)

Full source

instance : Monoid (A →A[R] A) where
  mul_one _ := ext fun _ => rfl
  one_mul _ := ext fun _ => rfl
  mul_assoc _ _ _ := ext fun _ => rfl

Monoid Structure on Continuous Algebra Endomorphisms

Informal description

For any topological algebra $A$ over a commutative semiring $R$, the set of continuous algebra homomorphisms from $A$ to itself forms a monoid under composition, with the identity map as the neutral element.

ContinuousAlgHom.coe_pow theorem

(f : A →A[R] A) (n : ℕ) : ⇑(f ^ n) = f^[n]

Full source

theorem coe_pow (f : A →A[R] A) (n : ℕ) : ⇑(f ^ n) = f^[n] :=
  hom_coe_pow _ rfl (fun _ _ ↦ rfl) _ _

Iteration of Continuous Algebra Homomorphism: $(f^n)(x) = f^{(n)}(x)$

Informal description

For any continuous algebra homomorphism $f \colon A \to_{A[R]} A$ and any natural number $n$, the underlying function of $f^n$ is equal to the $n$-th iterate of $f$, i.e., $(f^n)(x) = f^{(n)}(x)$ for all $x \in A$.

ContinuousAlgHom.toAlgHomMonoidHom definition

: (A →A[R] A) →* A →ₐ[R] A

Full source

/-- coercion from `ContinuousAlgHom` to `AlgHom` as a `RingHom`. -/
@[simps]
def toAlgHomMonoidHom : (A →A[R] A) →* A →ₐ[R] A where
  toFun        := (↑)
  map_one'     := rfl
  map_mul' _ _ := rfl

Monoid homomorphism from continuous algebra endomorphisms to algebra endomorphisms

Informal description

The function that coerces a continuous algebra endomorphism $ f : A \to_{A[R]} A $ to its underlying algebra homomorphism $ A \toₐ[R] A $, which is a monoid homomorphism with respect to composition of algebra homomorphisms.

ContinuousAlgHom.prod definition

(f₁ : A →A[R] B) (f₂ : A →A[R] C) : A →A[R] B × C

Full source

/-- The cartesian product of two continuous algebra morphisms as a continuous algebra morphism. -/
protected def prod (f₁ : A →A[R] B) (f₂ : A →A[R] C) :
    A →A[R] B × C :=
  ⟨(f₁ : A →ₐ[R] B).prod f₂, f₁.2.prodMk f₂.2⟩

Cartesian product of continuous algebra homomorphisms

Informal description

Given two continuous algebra homomorphisms $ f_1 : A \to_{A[R]} B $ and $ f_2 : A \to_{A[R]} C $, their cartesian product is a continuous algebra homomorphism $ A \to_{A[R]} B \times C $ defined by mapping each element $ x \in A $ to the pair $ (f_1(x), f_2(x)) $.

ContinuousAlgHom.coe_prod theorem

(f₁ : A →A[R] B) (f₂ : A →A[R] C) : (f₁.prod f₂ : A →ₐ[R] B × C) = AlgHom.prod f₁ f₂

Full source

@[simp, norm_cast]
theorem coe_prod (f₁ : A →A[R] B) (f₂ : A →A[R] C) :
    (f₁.prod f₂ : A →ₐ[R] B × C) = AlgHom.prod f₁ f₂ :=
  rfl

Underlying Algebra Homomorphism of Product of Continuous Algebra Homomorphisms

Informal description

For any continuous algebra homomorphisms $f_1 \colon A \to_{A[R]} B$ and $f_2 \colon A \to_{A[R]} C$, the underlying algebra homomorphism of their product $f_1.\mathrm{prod}\, f_2$ is equal to the product of the underlying algebra homomorphisms $\mathrm{AlgHom.prod}\, f_1\, f_2$.

ContinuousAlgHom.prod_apply theorem

(f₁ : A →A[R] B) (f₂ : A →A[R] C) (x : A) : f₁.prod f₂ x = (f₁ x, f₂ x)

Full source

@[simp, norm_cast]
theorem prod_apply (f₁ : A →A[R] B) (f₂ : A →A[R] C) (x : A) :
    f₁.prod f₂ x = (f₁ x, f₂ x) :=
  rfl

Evaluation of Product of Continuous Algebra Homomorphisms

Informal description

For any continuous algebra homomorphisms $f_1 \colon A \to_{A[R]} B$ and $f_2 \colon A \to_{A[R]} C$, and for any element $x \in A$, the product homomorphism $f_1.\text{prod}\, f_2$ evaluated at $x$ is equal to the pair $(f_1(x), f_2(x))$.

ContinuousAlgHom.instCompleteSpaceSubtypeMemSubalgebraEqualizerOfT2SpaceOfContinuousMapClass instance

 {D : Type*} [UniformSpace D] [CompleteSpace D] [Semiring D] [Algebra R D] [T2Space B] [FunLike F D B]
  [AlgHomClass F R D B] [ContinuousMapClass F D B] (f g : F) : CompleteSpace (AlgHom.equalizer f g)

Full source

instance {D : Type*} [UniformSpace D] [CompleteSpace D]
    [Semiring D] [Algebra R D] [T2Space B]
    [FunLike F D B] [AlgHomClass F R D B] [ContinuousMapClass F D B]
    (f g : F) : CompleteSpace (AlgHom.equalizer f g) :=
  isClosed_eq (map_continuous f) (map_continuous g) |>.completeSpace_coe

Completeness of the Equalizer of Continuous Algebra Homomorphisms

Informal description

For any uniform space $D$ that is complete, a semiring $D$ with an algebra structure over $R$, a Hausdorff space $B$, and continuous algebra homomorphisms $f, g : D \to B$, the subspace of $D$ where $f$ and $g$ coincide is complete.

ContinuousAlgHom.fst definition

: A × B →A[R] A

Full source

/-- `Prod.fst` as a `ContinuousAlgHom`. -/
def fst : A × BA × B →A[R] A where
  cont     := continuous_fst
  toAlgHom := AlgHom.fst R A B

First projection as a continuous algebra homomorphism

Informal description

The projection map $\text{fst} : A \times B \to A$ is a continuous algebra homomorphism between the product topological algebra $A \times B$ and $A$, where $A$ and $B$ are topological algebras over a commutative semiring $R$. This map sends a pair $(a, b)$ to its first component $a$ and is continuous with respect to the product topology on $A \times B$ and the given topology on $A$.

ContinuousAlgHom.snd definition

: A × B →A[R] B

Full source

/-- `Prod.snd` as a `ContinuousAlgHom`. -/
def snd : A × BA × B →A[R] B where
  cont := continuous_snd
  toAlgHom := AlgHom.snd R A B

Second projection as a continuous algebra homomorphism

Informal description

The projection map $\text{snd} : A \times B \to B$ is a continuous algebra homomorphism between the product topological algebra $A \times B$ and $B$, where $A$ and $B$ are topological algebras over a commutative semiring $R$. This map sends a pair $(a, b)$ to its second component $b$ and is continuous with respect to the product topology on $A \times B$ and the given topology on $B$.

ContinuousAlgHom.coe_fst theorem

: ↑(fst R A B) = AlgHom.fst R A B

Full source

@[simp, norm_cast]
theorem coe_fst : ↑(fst R A B) = AlgHom.fst R A B :=
  rfl

Underlying Algebra Homomorphism of First Projection Continuous Algebra Homomorphism

Informal description

The underlying algebra homomorphism of the continuous algebra homomorphism $\text{fst} : A \times B \to A$ is equal to the first projection algebra homomorphism $\text{AlgHom.fst} : A \times B \to A$.

ContinuousAlgHom.coe_fst' theorem

: ⇑(fst R A B) = Prod.fst

Full source

@[simp, norm_cast]
theorem coe_fst' : ⇑(fst R A B) = Prod.fst :=
  rfl

First Projection as Continuous Algebra Homomorphism

Informal description

The underlying function of the continuous algebra homomorphism $\text{fst} : A \times B \to A$ is equal to the first projection map $\text{Prod.fst} : A \times B \to A$, which sends a pair $(a, b)$ to $a$.

ContinuousAlgHom.coe_snd theorem

: ↑(snd R A B) = AlgHom.snd R A B

Full source

@[simp, norm_cast]
theorem coe_snd : ↑(snd R A B) = AlgHom.snd R A B :=
  rfl

Underlying Algebra Homomorphism of Second Projection Continuous Algebra Homomorphism

Informal description

The underlying algebra homomorphism of the continuous algebra homomorphism $\text{snd} : A \times B \to B$ is equal to the second projection algebra homomorphism $\text{AlgHom.snd} : A \times B \to B$.

ContinuousAlgHom.coe_snd' theorem

: ⇑(snd R A B) = Prod.snd

Full source

@[simp, norm_cast]
theorem coe_snd' : ⇑(snd R A B) = Prod.snd :=
  rfl

Second Projection as Continuous Algebra Homomorphism

Informal description

The underlying function of the continuous algebra homomorphism $\text{snd} : A \times B \to B$ is equal to the second projection map $\text{Prod.snd} : A \times B \to B$, which sends a pair $(a, b)$ to $b$.

ContinuousAlgHom.fst_prod_snd theorem

: (fst R A B).prod (snd R A B) = ContinuousAlgHom.id R (A × B)

Full source

@[simp]
theorem fst_prod_snd : (fst R A B).prod (snd R A B) = ContinuousAlgHom.id R (A × B) :=
  ext fun ⟨_x, _y⟩ => rfl

Product of Projections Equals Identity: $(fst, snd) = id_{A \times B}$

Informal description

The product of the first projection continuous algebra homomorphism $\text{fst} : A \times B \to A$ and the second projection continuous algebra homomorphism $\text{snd} : A \times B \to B$ is equal to the identity continuous algebra homomorphism on the product topological algebra $A \times B$.

ContinuousAlgHom.fst_comp_prod theorem

(f : A →A[R] B) (g : A →A[R] C) : (fst R B C).comp (f.prod g) = f

Full source

@[simp]
theorem fst_comp_prod (f : A →A[R] B) (g : A →A[R] C) :
    (fst R B C).comp (f.prod g) = f :=
  ext fun _x => rfl

First projection of product homomorphism equals first factor

Informal description

Let $A$, $B$, and $C$ be topological algebras over a commutative semiring $R$. For any continuous algebra homomorphisms $f \colon A \to_{A[R]} B$ and $g \colon A \to_{A[R]} C$, the composition of the first projection $\text{fst} \colon B \times C \to B$ with the product homomorphism $(f, g) \colon A \to B \times C$ equals $f$, i.e., $\text{fst} \circ (f, g) = f$.

ContinuousAlgHom.snd_comp_prod theorem

(f : A →A[R] B) (g : A →A[R] C) : (snd R B C).comp (f.prod g) = g

Full source

@[simp]
theorem snd_comp_prod (f : A →A[R] B) (g : A →A[R] C) :
    (snd R B C).comp (f.prod g) = g :=
  ext fun _x => rfl

Second Projection of Product Homomorphism Equals Second Component: $ \text{snd} \circ (f, g) = g $

Informal description

For any continuous algebra homomorphisms $ f \colon A \to_{A[R]} B $ and $ g \colon A \to_{A[R]} C $ between topological algebras over a commutative semiring $ R $, the composition of the second projection $ \text{snd} \colon B \times C \to C $ with the product homomorphism $ (f, g) \colon A \to_{A[R]} B \times C $ equals $ g $. In other words, $ \text{snd} \circ (f, g) = g $.

ContinuousAlgHom.prodMap definition

 {D : Type*} [Semiring D] [TopologicalSpace D] [Algebra R D] (f₁ : A →A[R] B) (f₂ : C →A[R] D) : A × C →A[R] B × D

Full source

/-- `Prod.map` of two continuous algebra homomorphisms. -/
def prodMap {D : Type*} [Semiring D] [TopologicalSpace D] [Algebra R D] (f₁ : A →A[R] B)
    (f₂ : C →A[R] D) : A × CA × C →A[R] B × D :=
  (f₁.comp (fst R A C)).prod (f₂.comp (snd R A C))

Product of continuous algebra homomorphisms

Informal description

Given continuous algebra homomorphisms $ f_1 \colon A \to_{A[R]} B $ and $ f_2 \colon C \to_{A[R]} D $, the product map $ f_1 \times f_2 \colon A \times C \to_{A[R]} B \times D $ is defined as the continuous algebra homomorphism obtained by composing $ f_1 $ with the first projection $ \text{fst} \colon A \times C \to A $ and $ f_2 $ with the second projection $ \text{snd} \colon A \times C \to C $, then taking their product. Here, $ A, B, C, D $ are topological algebras over a commutative semiring $ R $.

ContinuousAlgHom.coe_prodMap theorem

 {D : Type*} [Semiring D] [TopologicalSpace D] [Algebra R D] (f₁ : A →A[R] B) (f₂ : C →A[R] D) :
  (f₁.prodMap f₂ : A × C →ₐ[R] B × D) = (f₁ : A →ₐ[R] B).prodMap (f₂ : C →ₐ[R] D)

Full source

@[simp, norm_cast]
theorem coe_prodMap {D : Type*} [Semiring D] [TopologicalSpace D] [Algebra R D] (f₁ : A →A[R] B)
    (f₂ : C →A[R] D) :
    (f₁.prodMap f₂ : A × CA × C →ₐ[R] B × D) = (f₁ : A →ₐ[R] B).prodMap (f₂ : C →ₐ[R] D) :=
  rfl

Product of Continuous Algebra Homomorphisms as Algebra Homomorphism

Informal description

For continuous algebra homomorphisms $f_1 \colon A \to_{A[R]} B$ and $f_2 \colon C \to_{A[R]} D$ between topological algebras over a commutative semiring $R$, the underlying algebra homomorphism of their product map $f_1 \times f_2 \colon A \times C \to_{A[R]} B \times D$ equals the product map of the underlying algebra homomorphisms of $f_1$ and $f_2$.

ContinuousAlgHom.coe_prodMap' theorem

 {D : Type*} [Semiring D] [TopologicalSpace D] [Algebra R D] (f₁ : A →A[R] B) (f₂ : C →A[R] D) :
  ⇑(f₁.prodMap f₂) = Prod.map f₁ f₂

Full source

@[simp, norm_cast]
theorem coe_prodMap' {D : Type*} [Semiring D] [TopologicalSpace D] [Algebra R D] (f₁ : A →A[R] B)
    (f₂ : C →A[R] D) : ⇑(f₁.prodMap f₂) = Prod.map f₁ f₂ :=
  rfl

Underlying Function of Product of Continuous Algebra Homomorphisms is the Product Map

Informal description

For continuous algebra homomorphisms $ f_1 \colon A \to_{A[R]} B $ and $ f_2 \colon C \to_{A[R]} D $ between topological algebras over a commutative semiring $ R $, the underlying function of the product map $ f_1 \times f_2 $ is equal to the product of the underlying functions $ f_1 $ and $ f_2 $, i.e., $ (f_1 \times f_2)(x, y) = (f_1(x), f_2(y)) $ for all $ x \in A $ and $ y \in C $.

ContinuousAlgHom.prodEquiv definition

: (A →A[R] B) × (A →A[R] C) ≃ (A →A[R] B × C)

Full source

/-- `ContinuousAlgHom.prod` as an `Equiv`. -/
@[simps apply]
def prodEquiv : (A →A[R] B) × (A →A[R] C)(A →A[R] B) × (A →A[R] C) ≃ (A →A[R] B × C) where
  toFun f     := f.1.prod f.2
  invFun f    := ⟨(fst _ _ _).comp f, (snd _ _ _).comp f⟩
  left_inv f  := by ext <;> rfl
  right_inv f := by ext <;> rfl

Equivalence between product of continuous algebra homomorphisms and homomorphisms into product algebra

Informal description

The equivalence between the product of continuous algebra homomorphisms $(A \to_{A[R]} B) \times (A \to_{A[R]} C)$ and the space of continuous algebra homomorphisms $A \to_{A[R]} B \times C$. Specifically, the forward map takes a pair $(f_1, f_2)$ of continuous algebra homomorphisms and constructs the homomorphism $x \mapsto (f_1(x), f_2(x))$. The inverse map decomposes a homomorphism $f : A \to_{A[R]} B \times C$ into its component homomorphisms by composing with the projections $\text{fst} : B \times C \to B$ and $\text{snd} : B \times C \to C$.

ContinuousAlgHom.codRestrict definition

(f : A →A[R] B) (p : Subalgebra R B) (h : ∀ x, f x ∈ p) : A →A[R] p

Full source

/-- Restrict codomain of a continuous algebra morphism. -/
def codRestrict (f : A →A[R] B) (p : Subalgebra R B) (h : ∀ x, f x ∈ p) : A →A[R] p where
  cont     := f.continuous.subtype_mk _
  toAlgHom := (f : A →ₐ[R] B).codRestrict p h

Codomain restriction of a continuous algebra homomorphism

Informal description

Given a continuous algebra homomorphism $ f : A \to_{A[R]} B $ between topological $ R $-algebras $ A $ and $ B $, and a subalgebra $ p $ of $ B $ such that $ f(x) \in p $ for all $ x \in A $, the function restricts the codomain of $ f $ to $ p $, yielding a continuous algebra homomorphism $ A \to_{A[R]} p $.

ContinuousAlgHom.coe_codRestrict theorem

 (f : A →A[R] B) (p : Subalgebra R B) (h : ∀ x, f x ∈ p) :
  (f.codRestrict p h : A →ₐ[R] p) = (f : A →ₐ[R] B).codRestrict p h

Full source

@[norm_cast]
theorem coe_codRestrict (f : A →A[R] B) (p : Subalgebra R B) (h : ∀ x, f x ∈ p) :
    (f.codRestrict p h : A →ₐ[R] p) = (f : A →ₐ[R] B).codRestrict p h :=
  rfl

Equality of Underlying Algebra Homomorphisms After Codomain Restriction

Informal description

For a continuous algebra homomorphism $f \colon A \to_{A[R]} B$ between topological $R$-algebras $A$ and $B$, and a subalgebra $p$ of $B$ such that $f(x) \in p$ for all $x \in A$, the underlying algebra homomorphism of the codomain-restricted map $f.\mathrm{codRestrict}\, p\, h$ is equal to the codomain restriction of the underlying algebra homomorphism of $f$. In symbols: $$(f.\mathrm{codRestrict}\, p\, h \colon A \to_{\alg[R]} p) = (f \colon A \to_{\alg[R]} B).\mathrm{codRestrict}\, p\, h$$

ContinuousAlgHom.coe_codRestrict_apply theorem

(f : A →A[R] B) (p : Subalgebra R B) (h : ∀ x, f x ∈ p) (x) : (f.codRestrict p h x : B) = f x

Full source

@[simp]
theorem coe_codRestrict_apply (f : A →A[R] B) (p : Subalgebra R B) (h : ∀ x, f x ∈ p) (x) :
    (f.codRestrict p h x : B) = f x :=
  rfl

Codomain restriction preserves function values for continuous algebra homomorphisms

Informal description

Let $f : A \to_{A[R]} B$ be a continuous algebra homomorphism between topological $R$-algebras $A$ and $B$, and let $p$ be a subalgebra of $B$ such that $f(x) \in p$ for all $x \in A$. Then for any $x \in A$, the image of $x$ under the codomain-restricted homomorphism $f.\text{codRestrict}\, p\, h$ (viewed as an element of $B$) equals $f(x)$.

ContinuousAlgHom.rangeRestrict definition

(f : A →A[R] B)

Full source

/-- Restrict the codomain of a continuous algebra homomorphism `f` to `f.range`. -/
@[reducible]
def rangeRestrict (f : A →A[R] B) :=
  f.codRestrict (@AlgHom.range R A B  _ _ _ _ _ f) (@AlgHom.mem_range_self R A B  _ _ _ _ _ f)

Range restriction of a continuous algebra homomorphism

Informal description

Given a continuous algebra homomorphism $ f : A \to_{A[R]} B $ between topological $ R $-algebras $ A $ and $ B $, the function restricts the codomain of $ f $ to the range of $ f $, yielding a continuous algebra homomorphism $ A \to_{A[R]} \text{range}(f) $.

ContinuousAlgHom.coe_rangeRestrict theorem

 (f : A →A[R] B) : (f.rangeRestrict : A →ₐ[R] (@AlgHom.range R A B _ _ _ _ _ f)) = (f : A →ₐ[R] B).rangeRestrict

Full source

@[simp]
theorem coe_rangeRestrict (f : A →A[R] B) :
    (f.rangeRestrict : A →ₐ[R] (@AlgHom.range R A B  _ _ _ _ _ f)) =
      (f : A →ₐ[R] B).rangeRestrict :=
  rfl

Range Restriction Commutes with Underlying Algebra Homomorphism

Informal description

For any continuous algebra homomorphism $f \colon A \to_{A[R]} B$ between topological $R$-algebras $A$ and $B$, the underlying algebra homomorphism of the range-restricted map $f.\text{rangeRestrict}$ is equal to the range restriction of the underlying algebra homomorphism of $f$.

Subalgebra.valA definition

(p : Subalgebra R A) : p →A[R] A

Full source

/-- `Subalgebra.val` as a `ContinuousAlgHom`. -/
def _root_.Subalgebra.valA (p : Subalgebra R A) : p →A[R] A where
  cont := continuous_subtype_val
  toAlgHom := p.val

Inclusion map of a subalgebra as a continuous algebra homomorphism

Informal description

The inclusion map from a subalgebra $ p $ of a topological algebra $ A $ over a commutative semiring $ R $ to $ A $ itself, viewed as a continuous algebra homomorphism. This map is continuous and preserves both the ring and module structures.

Subalgebra.coe_valA theorem

(p : Subalgebra R A) : (p.valA : p →ₐ[R] A) = p.subtype

Full source

@[simp, norm_cast]
theorem _root_.Subalgebra.coe_valA (p : Subalgebra R A) :
    (p.valA : p →ₐ[R] A) = p.subtype :=
  rfl

Equality of Underlying Algebra Homomorphism and Subalgebra Inclusion Map

Informal description

For any subalgebra $p$ of a topological algebra $A$ over a commutative semiring $R$, the underlying algebra homomorphism of the continuous algebra homomorphism $p.\text{valA}$ is equal to the subalgebra inclusion map $p.\text{subtype}$.

Subalgebra.coe_valA' theorem

(p : Subalgebra R A) : ⇑p.valA = p.subtype

Full source

@[simp]
theorem _root_.Subalgebra.coe_valA' (p : Subalgebra R A) : ⇑p.valA = p.subtype :=
  rfl

Equality of Underlying Function and Subalgebra Inclusion Map

Informal description

For any subalgebra $p$ of a topological algebra $A$ over a commutative semiring $R$, the underlying function of the continuous algebra homomorphism $p.\text{valA}$ is equal to the subalgebra inclusion map $p.\text{subtype}$.

Subalgebra.valA_apply theorem

(p : Subalgebra R A) (x : p) : p.valA x = x

Full source

@[simp]
theorem _root_.Subalgebra.valA_apply (p : Subalgebra R A) (x : p) : p.valA x = x :=
  rfl

Inclusion Map Evaluation on Subalgebra Elements

Informal description

For any subalgebra $p$ of a topological algebra $A$ over a commutative semiring $R$, and for any element $x \in p$, the evaluation of the inclusion map $p.\text{valA}$ at $x$ equals $x$ itself, i.e., $p.\text{valA}(x) = x$.

Submodule.range_valA theorem

(p : Subalgebra R A) : @AlgHom.range R p A _ _ _ _ _ p.valA = p

Full source

@[simp]
theorem _root_.Submodule.range_valA (p : Subalgebra R A) :
    @AlgHom.range R p A _ _ _ _ _ p.valA = p :=
  Subalgebra.range_val p

Range of Subalgebra Inclusion Map Equals Subalgebra

Informal description

For any subalgebra $p$ of a topological algebra $A$ over a commutative semiring $R$, the range of the inclusion map $p.\text{valA}$ (viewed as an algebra homomorphism) is equal to $p$ itself.

ContinuousAlgHom.map_neg theorem

(f : S →A[R] B) (x : S) : f (-x) = -f x

Full source

protected theorem map_neg (f : S →A[R] B) (x : S) : f (-x) = -f x := map_neg f x

Negation Preservation under Continuous Algebra Homomorphisms

Informal description

For any continuous algebra homomorphism $f \colon S \to_{A[R]} B$ between topological $R$-algebras and any element $x \in S$, the image of $-x$ under $f$ is equal to the negation of the image of $x$, i.e., $f(-x) = -f(x)$.

ContinuousAlgHom.map_sub theorem

(f : S →A[R] B) (x y : S) : f (x - y) = f x - f y

Full source

protected theorem map_sub (f : S →A[R] B) (x y : S) : f (x - y) = f x - f y := map_sub f x y

Subtraction Preservation under Continuous Algebra Homomorphisms

Informal description

For any continuous algebra homomorphism $f \colon S \to_{A[R]} B$ between topological $R$-algebras and any elements $x, y \in S$, the image of $x - y$ under $f$ equals the difference of the images, i.e., $f(x - y) = f(x) - f(y)$.

ContinuousAlgHom.restrictScalars definition

(f : B →A[S] C) : B →A[R] C

Full source

/-- If `A` is an `R`-algebra, then a continuous `A`-algebra morphism can be interpreted as a
continuous `R`-algebra morphism. -/
def restrictScalars (f : B →A[S] C) : B →A[R] C :=
  ⟨(f : B →ₐ[S] C).restrictScalars R, f.continuous⟩

Restriction of scalars for continuous algebra homomorphisms

Informal description

Given a continuous algebra homomorphism $ f : B \to_{A[S]} C $ between topological algebras over a commutative semiring $ S $, the function `restrictScalars` restricts the scalar multiplication of $ f $ to a smaller commutative semiring $ R $, producing a continuous algebra homomorphism $ B \to_{A[R]} C $. This operation preserves the underlying function and continuity of $ f $.

ContinuousAlgHom.coe_restrictScalars theorem

(f : B →A[S] C) : (f.restrictScalars R : B →ₐ[R] C) = (f : B →ₐ[S] C).restrictScalars R

Full source

@[simp]
theorem coe_restrictScalars (f : B →A[S] C) :
    (f.restrictScalars R : B →ₐ[R] C) = (f : B →ₐ[S] C).restrictScalars R :=
  rfl

Restriction of Scalars Preserves Underlying Algebra Homomorphism

Informal description

For any continuous algebra homomorphism $f \colon B \to_{A[S]} C$ between topological algebras over a commutative semiring $S$, the underlying algebra homomorphism of the restriction of scalars of $f$ to a smaller commutative semiring $R$ is equal to the restriction of scalars of the underlying algebra homomorphism of $f$.

ContinuousAlgHom.coe_restrictScalars' theorem

(f : B →A[S] C) : ⇑(f.restrictScalars R) = f

Full source

@[simp]
theorem coe_restrictScalars' (f : B →A[S] C) : ⇑(f.restrictScalars R) = f :=
  rfl

Restriction of Scalars Preserves Underlying Function

Informal description

For any continuous algebra homomorphism $f \colon B \to_{A[S]} C$ between topological algebras over a commutative semiring $S$, the underlying function of the restriction of scalars of $f$ to a smaller commutative semiring $R$ is equal to $f$ itself.

instIsTopologicalSemiringSubtypeMemSubalgebra instance

(s : Subalgebra R A) : IsTopologicalSemiring s

Full source

instance (s : Subalgebra R A) : IsTopologicalSemiring s :=
  s.toSubsemiring.topologicalSemiring

Subalgebras as Topological Semirings

Informal description

For any subalgebra $s$ of a topological algebra $A$ over a topological semiring $R$, the subalgebra $s$ inherits a topological semiring structure from $A$.

Subalgebra.le_topologicalClosure theorem

(s : Subalgebra R A) : s ≤ s.topologicalClosure

Full source

theorem Subalgebra.le_topologicalClosure (s : Subalgebra R A) : s ≤ s.topologicalClosure :=
  subset_closure

Subalgebra is Contained in its Topological Closure

Informal description

For any subalgebra $s$ of a topological algebra $A$ over a topological semiring $R$, the subalgebra $s$ is contained in its topological closure.

Subalgebra.isClosed_topologicalClosure theorem

(s : Subalgebra R A) : IsClosed (s.topologicalClosure : Set A)

Full source

theorem Subalgebra.isClosed_topologicalClosure (s : Subalgebra R A) :
    IsClosed (s.topologicalClosure : Set A) := by convert @isClosed_closure A _ s

Topological Closure of a Subalgebra is Closed

Informal description

For any subalgebra $s$ of a topological algebra $A$ over a topological semiring $R$, the topological closure of $s$ is a closed subset of $A$.

Subalgebra.topologicalClosure_minimal theorem

(s : Subalgebra R A) {t : Subalgebra R A} (h : s ≤ t) (ht : IsClosed (t : Set A)) : s.topologicalClosure ≤ t

Full source

theorem Subalgebra.topologicalClosure_minimal (s : Subalgebra R A) {t : Subalgebra R A} (h : s ≤ t)
    (ht : IsClosed (t : Set A)) : s.topologicalClosure ≤ t :=
  closure_minimal h ht

Minimality of Topological Closure for Subalgebras

Informal description

Let $A$ be a topological algebra over a topological semiring $R$, and let $s$ be a subalgebra of $A$. For any subalgebra $t$ of $A$ such that $s \subseteq t$ and $t$ is closed in the topology of $A$, the topological closure of $s$ is contained in $t$.

Subalgebra.commSemiringTopologicalClosure abbrev

[T2Space A] (s : Subalgebra R A) (hs : ∀ x y : s, x * y = y * x) : CommSemiring s.topologicalClosure

Full source

/-- If a subalgebra of a topological algebra is commutative, then so is its topological closure.

See note [reducible non-instances]. -/
abbrev Subalgebra.commSemiringTopologicalClosure [T2Space A] (s : Subalgebra R A)
    (hs : ∀ x y : s, x * y = y * x) : CommSemiring s.topologicalClosure :=
  { s.topologicalClosure.toSemiring, s.toSubmonoid.commMonoidTopologicalClosure hs with }

Commutativity of Topological Closure of a Subalgebra

Informal description

Let $A$ be a topological algebra over a topological semiring $R$ that is Hausdorff, and let $s$ be a subalgebra of $A$. If $s$ is commutative (i.e., $x \cdot y = y \cdot x$ for all $x, y \in s$), then the topological closure of $s$ is also a commutative semiring.

Subalgebra.topologicalClosure_comap_homeomorph theorem

 (s : Subalgebra R A) {B : Type*} [TopologicalSpace B] [Ring B] [IsTopologicalRing B] [Algebra R B] (f : B →ₐ[R] A)
  (f' : B ≃ₜ A) (w : (f : B → A) = f') : s.topologicalClosure.comap f = (s.comap f).topologicalClosure

Full source

/-- 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.
-/
theorem Subalgebra.topologicalClosure_comap_homeomorph (s : Subalgebra R A) {B : Type*}
    [TopologicalSpace B] [Ring B] [IsTopologicalRing B] [Algebra R B] (f : B →ₐ[R] A) (f' : B ≃ₜ A)
    (w : (f : B → A) = f') : s.topologicalClosure.comap f = (s.comap f).topologicalClosure := by
  apply SetLike.ext'
  simp only [Subalgebra.topologicalClosure_coe]
  simp only [Subalgebra.coe_comap, Subsemiring.coe_comap, AlgHom.coe_toRingHom]
  rw [w]
  exact f'.preimage_closure _

Equality of Pullbacks of Topological Closures under Algebra Homeomorphism

Informal description

Let $A$ be a topological algebra over a topological semiring $R$, and let $s$ be a subalgebra of $A$. Suppose $B$ is another topological ring with an algebra structure over $R$, and let $f: B \to A$ be an algebra homomorphism that is also a homeomorphism (with inverse $f'$). If $f$ and $f'$ agree as functions, then the topological closure of $s$ pulled back along $f$ is equal to the topological closure of the pullback of $s$ along $f$.

Algebra.elemental definition

(x : A) : Subalgebra R A

Full source

/-- The topological closure of the subalgebra generated by a single element. -/
def Algebra.elemental (x : A) : Subalgebra R A :=
  (Algebra.adjoin R ({x} : Set A)).topologicalClosure

Topological closure of the subalgebra generated by an element

Informal description

Given a topological algebra $A$ over a topological semiring $R$ and an element $x \in A$, the *topological closure of the subalgebra generated by $x$* is the smallest closed subalgebra of $A$ containing $x$. It is constructed by taking the topological closure of the subalgebra generated by the singleton set $\{x\}$.

Algebra.elemental.self_mem theorem

(x : A) : x ∈ elemental R x

Full source

@[aesop safe apply (rule_sets := [SetLike])]
theorem self_mem (x : A) : x ∈ elemental R x :=
  le_topologicalClosure _ <| self_mem_adjoin_singleton R x

Element is in its own generated subalgebra closure

Informal description

For any element $x$ in a topological algebra $A$ over a topological semiring $R$, the element $x$ belongs to the topological closure of the subalgebra generated by $x$.

Algebra.elemental.le_of_mem theorem

{x : A} {s : Subalgebra R A} (hs : IsClosed (s : Set A)) (hx : x ∈ s) : elemental R x ≤ s

Full source

theorem le_of_mem {x : A} {s : Subalgebra R A} (hs : IsClosed (s : Set A)) (hx : x ∈ s) :
    elemental R x ≤ s :=
  topologicalClosure_minimal _ (adjoin_le <| by simpa using hx) hs

Inclusion of Topological Closure of Cyclic Subalgebra in Closed Subalgebra

Informal description

Let $A$ be a topological algebra over a topological semiring $R$, and let $x \in A$ and $s$ be a closed subalgebra of $A$. If $x \in s$, then the topological closure of the subalgebra generated by $x$ is contained in $s$.

Algebra.elemental.le_iff_mem theorem

{x : A} {s : Subalgebra R A} (hs : IsClosed (s : Set A)) : elemental R x ≤ s ↔ x ∈ s

Full source

theorem le_iff_mem {x : A} {s : Subalgebra R A} (hs : IsClosed (s : Set A)) :
    elementalelemental R x ≤ s ↔ x ∈ s :=
  ⟨fun h ↦ h (self_mem R x), fun h ↦ le_of_mem hs h⟩

Characterization of Inclusion of Cyclic Subalgebra Closure in Closed Subalgebra

Informal description

Let $A$ be a topological algebra over a topological semiring $R$, let $x \in A$, and let $s$ be a closed subalgebra of $A$. Then the topological closure of the subalgebra generated by $x$ is contained in $s$ if and only if $x$ belongs to $s$.

Algebra.elemental.isClosed instance

(x : A) : IsClosed (elemental R x : Set A)

Full source

instance isClosed (x : A) : IsClosed (elemental R x : Set A) :=
  isClosed_topologicalClosure _

Closedness of the Topological Closure of a Cyclic Subalgebra

Informal description

For any element $x$ in a topological algebra $A$ over a topological semiring $R$, the topological closure of the subalgebra generated by $x$ is a closed subset of $A$.

Algebra.elemental.instCommSemiringSubtypeMemSubalgebraOfT2Space instance

[T2Space A] {x : A} : CommSemiring (elemental R x)

Full source

instance [T2Space A] {x : A} : CommSemiring (elemental R x) :=
  commSemiringTopologicalClosure _
    letI : CommSemiring (adjoin R {x}) :=
      adjoinCommSemiringOfComm R fun y hy z hz => by
        rw [mem_singleton_iff] at hy hz
        rw [hy, hz]
    fun _ _ => mul_comm _ _

Commutative Semiring Structure on Topological Closure of Cyclic Subalgebra

Informal description

For any Hausdorff topological algebra $A$ over a topological semiring $R$ and any element $x \in A$, the topological closure of the subalgebra generated by $x$ is a commutative semiring.

Algebra.elemental.instCompleteSpaceSubtypeMemSubalgebra instance

 {A : Type*} [UniformSpace A] [CompleteSpace A] [Semiring A] [IsTopologicalSemiring A] [Algebra R A] (x : A) :
  CompleteSpace (elemental R x)

Full source

instance {A : Type*} [UniformSpace A] [CompleteSpace A] [Semiring A]
    [IsTopologicalSemiring A] [Algebra R A] (x : A) :
    CompleteSpace (elemental R x) :=
  isClosed_closure.completeSpace_coe

Completeness of the Topological Closure of a Cyclic Subalgebra

Informal description

For a uniform topological algebra $A$ over a topological semiring $R$ that is complete, and for any element $x \in A$, the topological closure of the subalgebra generated by $x$ is also complete.

Algebra.elemental.isClosedEmbedding_coe theorem

(x : A) : IsClosedEmbedding ((↑) : elemental R x → A)

Full source

/-- The coercion from an elemental algebra to the full algebra is a `IsClosedEmbedding`. -/
theorem isClosedEmbedding_coe (x : A) : IsClosedEmbedding ((↑) : elemental R x → A) where
  eq_induced := rfl
  injective := Subtype.coe_injective
  isClosed_range := by simpa using isClosed R x

Closed Embedding Property of the Inclusion from the Topological Closure of a Cyclic Subalgebra

Informal description

For any element $x$ in a topological algebra $A$ over a topological semiring $R$, the canonical inclusion map from the topological closure of the subalgebra generated by $x$ to $A$ is a closed embedding. That is, the map is injective, continuous, maps closed sets to closed sets, and has a continuous left inverse.

Subalgebra.commRingTopologicalClosure abbrev

[T2Space A] (s : Subalgebra R A) (hs : ∀ x y : s, x * y = y * x) : CommRing s.topologicalClosure

Full source

/-- If a subalgebra of a topological algebra is commutative, then so is its topological closure.
See note [reducible non-instances]. -/
abbrev Subalgebra.commRingTopologicalClosure [T2Space A] (s : Subalgebra R A)
    (hs : ∀ x y : s, x * y = y * x) : CommRing s.topologicalClosure :=
  { s.topologicalClosure.toRing, s.toSubmonoid.commMonoidTopologicalClosure hs with }

Commutativity of Topological Closure of a Subalgebra

Informal description

Let $A$ be a topological algebra over a topological semiring $R$, and let $s$ be a subalgebra of $A$. If $s$ is commutative (i.e., $x \cdot y = y \cdot x$ for all $x, y \in s$), then the topological closure of $s$ in $A$ is also a commutative ring.

instCommRingSubtypeMemSubalgebraElementalOfT2Space instance

[T2Space A] {x : A} : CommRing (elemental R x)

Full source

instance [T2Space A] {x : A} : CommRing (elemental R x) where
  mul_comm := mul_comm

Commutative Ring Structure on Topological Closure of Cyclic Subalgebra in T₂ Space

Informal description

For any topological algebra $A$ over a topological semiring $R$ that is a T₂ space, and for any element $x \in A$, the topological closure of the subalgebra generated by $x$ forms a commutative ring.

Results