Mathlib.Topology.Algebra.Module.LinearMap

ContinuousLinearMap structure

{R : Type*} {S : Type*} [Semiring R] [Semiring S] (σ : R →+* S)
    (M : Type*) [TopologicalSpace M] [AddCommMonoid M] (M₂ : Type*) [TopologicalSpace M₂]
    [AddCommMonoid M₂] [Module R M] [Module S M₂] extends M →ₛₗ[σ] M₂

Full source

/-- Continuous linear maps between modules. We only put the type classes that are necessary for the
definition, although in applications `M` and `M₂` will be topological modules over the topological
ring `R`. -/
structure ContinuousLinearMap {R : Type*} {S : Type*} [Semiring R] [Semiring S] (σ : R →+* S)
    (M : Type*) [TopologicalSpace M] [AddCommMonoid M] (M₂ : Type*) [TopologicalSpace M₂]
    [AddCommMonoid M₂] [Module R M] [Module S M₂] extends M →ₛₗ[σ] M₂ where
  cont : Continuous toFun := by continuity

Continuous semilinear map

Informal description

The structure representing continuous semilinear maps between topological modules $M$ and $M₂$ over semirings $R$ and $S$ respectively, with respect to a ring homomorphism $\sigma: R \to S$. A continuous semilinear map is a semilinear map that is also continuous with respect to the given topologies on $M$ and $M₂$.

term_→SL[_]_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
notation:25 M " →SL[" σ "] " M₂ => ContinuousLinearMap σ M M₂

Continuous semilinear maps

Informal description

The notation `M →SL[σ] M₂` denotes the type of continuous semilinear maps between the topological modules `M` and `M₂` with respect to the ring homomorphism `σ`.

term_→L[_]_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
notation:25 M " →L[" R "] " M₂ => ContinuousLinearMap (RingHom.id R) M M₂

Continuous linear maps

Informal description

The notation `M →L[R] M₂` represents the type of continuous linear maps from the topological module `M` over the ring `R` to the topological module `M₂` over the same ring `R`. These are linear maps that are also continuous with respect to the given topologies.

ContinuousSemilinearMapClass structure

(F : Type*) {R S : outParam Type*} [Semiring R] [Semiring S]
    (σ : outParam <| R →+* S) (M : outParam Type*) [TopologicalSpace M] [AddCommMonoid M]
    (M₂ : outParam Type*) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M]
    [Module S M₂] [FunLike F M M₂] : Prop
    extends SemilinearMapClass F σ M M₂, ContinuousMapClass F M M₂

Full source

/-- `ContinuousSemilinearMapClass F σ M M₂` asserts `F` is a type of bundled continuous
`σ`-semilinear maps `M → M₂`.  See also `ContinuousLinearMapClass F R M M₂` for the case where
`σ` is the identity map on `R`.  A map `f` between an `R`-module and an `S`-module over a ring
homomorphism `σ : R →+* S` is semilinear if it satisfies the two properties `f (x + y) = f x + f y`
and `f (c • x) = (σ c) • f x`. -/
class ContinuousSemilinearMapClass (F : Type*) {R S : outParam Type*} [Semiring R] [Semiring S]
    (σ : outParam <| R →+* S) (M : outParam Type*) [TopologicalSpace M] [AddCommMonoid M]
    (M₂ : outParam Type*) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M]
    [Module S M₂] [FunLike F M M₂] : Prop
    extends SemilinearMapClass F σ M M₂, ContinuousMapClass F M M₂

Class of Continuous Semilinear Maps

Informal description

The class `ContinuousSemilinearMapClass F σ M M₂` asserts that `F` is a type of bundled continuous `σ`-semilinear maps from `M` to `M₂`, where `σ : R →+* S` is a ring homomorphism. A map `f : M → M₂` is `σ`-semilinear if it satisfies: 1. Additivity: $f(x + y) = f(x) + f(y)$ for all $x, y \in M$. 2. Semilinearity: $f(c \cdot x) = \sigma(c) \cdot f(x)$ for all $c \in R$ and $x \in M$. Additionally, all maps in `F` are continuous with respect to the given topologies on `M` and `M₂`.

ContinuousLinearMapClass abbrev

 (F : Type*) (R : outParam Type*) [Semiring R] (M : outParam Type*) [TopologicalSpace M] [AddCommMonoid M]
  (M₂ : outParam Type*) [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M] [Module R M₂] [FunLike F M M₂]

Full source

/-- `ContinuousLinearMapClass F R M M₂` asserts `F` is a type of bundled continuous
`R`-linear maps `M → M₂`.  This is an abbreviation for
`ContinuousSemilinearMapClass F (RingHom.id R) M M₂`. -/
abbrev ContinuousLinearMapClass (F : Type*) (R : outParam Type*) [Semiring R]
    (M : outParam Type*) [TopologicalSpace M] [AddCommMonoid M] (M₂ : outParam Type*)
    [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R M] [Module R M₂] [FunLike F M M₂] :=
  ContinuousSemilinearMapClass F (RingHom.id R) M M₂

Class of Continuous Linear Maps

Informal description

The class `ContinuousLinearMapClass F R M M₂` asserts that `F` is a type of bundled continuous `R`-linear maps from `M` to `M₂`. A map `f : M → M₂` is `R`-linear if it satisfies: 1. Additivity: $f(x + y) = f(x) + f(y)$ for all $x, y \in M$. 2. Linearity: $f(c \cdot x) = c \cdot f(x)$ for all $c \in R$ and $x \in M$. Additionally, all maps in `F` are continuous with respect to the given topologies on `M` and `M₂$.

ContinuousLinearMap.LinearMap.coe instance

: Coe (M₁ →SL[σ₁₂] M₂) (M₁ →ₛₗ[σ₁₂] M₂)

Full source

/-- Coerce continuous linear maps to linear maps. -/
instance LinearMap.coe : Coe (M₁ →SL[σ₁₂] M₂) (M₁ →ₛₗ[σ₁₂] M₂) := ⟨toLinearMap⟩

Continuous Semilinear Maps as Semilinear Maps

Informal description

Every continuous semilinear map $f: M_1 \to_{SL[\sigma_{12}]} M_2$ can be viewed as a semilinear map $M_1 \to_{SL[\sigma_{12}]} M_2$ by forgetting the continuity condition.

ContinuousLinearMap.coe_injective theorem

: Function.Injective ((↑) : (M₁ →SL[σ₁₂] M₂) → M₁ →ₛₗ[σ₁₂] M₂)

Full source

theorem coe_injective : Function.Injective ((↑) : (M₁ →SL[σ₁₂] M₂) → M₁ →ₛₗ[σ₁₂] M₂) := by
  intro f g H
  cases f
  cases g
  congr

Injectivity of the Continuous Semilinear Map Canonical Embedding

Informal description

The canonical map from the space of continuous semilinear maps $ M_1 \to_{SL[\sigma_{12}]} M_2 $ to the space of semilinear maps $ M_1 \to_{SL[\sigma_{12}]} M_2 $ is injective. That is, if two continuous semilinear maps $ f, g \colon M_1 \to M_2 $ are equal as semilinear maps, then they are equal as continuous semilinear maps.

ContinuousLinearMap.funLike instance

: FunLike (M₁ →SL[σ₁₂] M₂) M₁ M₂

Full source

instance funLike : FunLike (M₁ →SL[σ₁₂] M₂) M₁ M₂ where
  coe f := f.toLinearMap
  coe_injective' _ _ h := coe_injective (DFunLike.coe_injective h)

Function-Like Structure on Continuous Semilinear Maps

Informal description

The type of continuous semilinear maps $ M_1 \to_{SL[\sigma_{12}]} M_2 $ is equipped with a function-like structure, meaning each continuous semilinear map can be treated as a function from $ M_1 $ to $ M_2 $.

ContinuousLinearMap.continuousSemilinearMapClass instance

: ContinuousSemilinearMapClass (M₁ →SL[σ₁₂] M₂) σ₁₂ M₁ M₂

Full source

instance continuousSemilinearMapClass :
    ContinuousSemilinearMapClass (M₁ →SL[σ₁₂] M₂) σ₁₂ M₁ M₂ where
  map_add f := map_add f.toLinearMap
  map_continuous f := f.2
  map_smulₛₗ f := f.toLinearMap.map_smul'

Continuous Semilinear Maps as a Class

Informal description

The type of continuous semilinear maps $ M_1 \to_{SL[\sigma_{12}]} M_2 $ forms a class of continuous semilinear maps, where each map is both semilinear with respect to the ring homomorphism $\sigma_{12}$ and continuous with respect to the given topologies on $ M_1 $ and $ M_2 $.

ContinuousLinearMap.coe_mk theorem

(f : M₁ →ₛₗ[σ₁₂] M₂) (h) : (mk f h : M₁ →ₛₗ[σ₁₂] M₂) = f

Full source

theorem coe_mk (f : M₁ →ₛₗ[σ₁₂] M₂) (h) : (mk f h : M₁ →ₛₗ[σ₁₂] M₂) = f :=
  rfl

Coercion of Constructed Continuous Semilinear Map Equals Original Map

Informal description

Let $M₁$ and $M₂$ be topological modules over rings $R₁$ and $R₂$ respectively, with $\sigma_{12} \colon R₁ \to R₂$ a ring homomorphism. For any continuous semilinear map $f \colon M₁ \to_{SL[\sigma_{12}]} M₂$ and continuity proof $h$, the coercion of the constructed continuous semilinear map $\text{mk}(f, h)$ to a semilinear map equals $f$ itself. In other words, $(\text{mk}(f, h) \colon M₁ \to_{SL[\sigma_{12}]} M₂) = f$.

ContinuousLinearMap.coe_mk' theorem

(f : M₁ →ₛₗ[σ₁₂] M₂) (h) : (mk f h : M₁ → M₂) = f

Full source

@[simp]
theorem coe_mk' (f : M₁ →ₛₗ[σ₁₂] M₂) (h) : (mk f h : M₁ → M₂) = f :=
  rfl

Underlying Function of Continuous Semilinear Map Construction

Informal description

For any semilinear map $f \colon M_1 \to_{SL[\sigma_{12}]} M_2$ and a proof $h$ that $f$ is continuous, the underlying function of the continuous semilinear map constructed from $f$ and $h$ is equal to $f$ itself. That is, if we construct a continuous semilinear map $\text{mk}(f, h) \colon M_1 \toSL[\sigma_{12}] M_2$, then the function $\text{mk}(f, h) \colon M_1 \to M_2$ is identical to $f$.

ContinuousLinearMap.continuous theorem

(f : M₁ →SL[σ₁₂] M₂) : Continuous f

Full source

@[continuity, fun_prop]
protected theorem continuous (f : M₁ →SL[σ₁₂] M₂) : Continuous f :=
  f.2

Continuity of Continuous Semilinear Maps

Informal description

Every continuous semilinear map $f \colon M_1 \to_{SL[\sigma_{12}]} M_2$ between topological modules is continuous as a function between topological spaces.

ContinuousLinearMap.uniformContinuous theorem

 {E₁ E₂ : Type*} [UniformSpace E₁] [UniformSpace E₂] [AddCommGroup E₁] [AddCommGroup E₂] [Module R₁ E₁] [Module R₂ E₂]
  [IsUniformAddGroup E₁] [IsUniformAddGroup E₂] (f : E₁ →SL[σ₁₂] E₂) : UniformContinuous f

Full source

protected theorem uniformContinuous {E₁ E₂ : Type*} [UniformSpace E₁] [UniformSpace E₂]
    [AddCommGroup E₁] [AddCommGroup E₂] [Module R₁ E₁] [Module R₂ E₂] [IsUniformAddGroup E₁]
    [IsUniformAddGroup E₂] (f : E₁ →SL[σ₁₂] E₂) : UniformContinuous f :=
  uniformContinuous_addMonoidHom_of_continuous f.continuous

Uniform Continuity of Continuous Semilinear Maps on Uniform Additive Groups

Informal description

Let $E_1$ and $E_2$ be uniform spaces equipped with additive commutative group structures and module structures over semirings $R_1$ and $R_2$ respectively, with respect to a ring homomorphism $\sigma_{12} \colon R_1 \to R_2$. Assume that both $E_1$ and $E_2$ are uniform additive groups (i.e., addition and negation are uniformly continuous). Then any continuous semilinear map $f \colon E_1 \to_{SL[\sigma_{12}]} E_2$ is uniformly continuous.

ContinuousLinearMap.coe_inj theorem

{f g : M₁ →SL[σ₁₂] M₂} : (f : M₁ →ₛₗ[σ₁₂] M₂) = g ↔ f = g

Full source

@[simp, norm_cast]
theorem coe_inj {f g : M₁ →SL[σ₁₂] M₂} : (f : M₁ →ₛₗ[σ₁₂] M₂) = g ↔ f = g :=
  coe_injective.eq_iff

Equality of Continuous Semilinear Maps via Underlying Semilinear Maps

Informal description

For any two continuous semilinear maps $ f, g \colon M_1 \to_{SL[\sigma_{12}]} M_2 $, the underlying semilinear maps $ f $ and $ g $ are equal if and only if $ f $ and $ g $ are equal as continuous semilinear maps. In other words, $ f = g $ as semilinear maps if and only if $ f = g $ as continuous semilinear maps.

ContinuousLinearMap.coeFn_injective theorem

: @Function.Injective (M₁ →SL[σ₁₂] M₂) (M₁ → M₂) (↑)

Full source

theorem coeFn_injective : @Function.Injective (M₁ →SL[σ₁₂] M₂) (M₁ → M₂) (↑) :=
  DFunLike.coe_injective

Injectivity of the Canonical Map from Continuous Semilinear Maps to Functions

Informal description

The canonical map from the space of continuous semilinear maps $M_1 \to_{SL[\sigma_{12}]} M_2$ to the space of functions $M_1 \to M_2$ is injective. That is, if two continuous semilinear maps $f, g : M_1 \to_{SL[\sigma_{12}]} M_2$ satisfy $f(x) = g(x)$ for all $x \in M_1$, then $f = g$.

ContinuousLinearMap.toContinuousAddMonoidHom_injective theorem

: Function.Injective ((↑) : (M₁ →SL[σ₁₂] M₂) → ContinuousAddMonoidHom M₁ M₂)

Full source

theorem toContinuousAddMonoidHom_injective :
    Function.Injective ((↑) : (M₁ →SL[σ₁₂] M₂) → ContinuousAddMonoidHom M₁ M₂) :=
  (DFunLike.coe_injective.of_comp_iff _).1 DFunLike.coe_injective

Injectivity of the Canonical Map from Continuous Semilinear Maps to Continuous Additive Monoid Homomorphisms

Informal description

The canonical map from the space of continuous semilinear maps $M_1 \to_{SL[\sigma_{12}]} M_2$ to the space of continuous additive monoid homomorphisms $M_1 \to M_2$ is injective. That is, if two continuous semilinear maps $f, g : M_1 \to_{SL[\sigma_{12}]} M_2$ induce the same continuous additive monoid homomorphism, then $f = g$.

ContinuousLinearMap.toContinuousAddMonoidHom_inj theorem

{f g : M₁ →SL[σ₁₂] M₂} : (f : ContinuousAddMonoidHom M₁ M₂) = g ↔ f = g

Full source

@[simp, norm_cast]
theorem toContinuousAddMonoidHom_inj {f g : M₁ →SL[σ₁₂] M₂} :
    (f : ContinuousAddMonoidHom M₁ M₂) = g ↔ f = g :=
  toContinuousAddMonoidHom_injective.eq_iff

Equality of Continuous Semilinear Maps via Induced Homomorphisms

Informal description

For any two continuous semilinear maps $ f, g : M_1 \to_{SL[\sigma_{12}]} M_2 $, the induced continuous additive monoid homomorphisms $ f $ and $ g $ are equal if and only if $ f = g $ as continuous semilinear maps.

ContinuousLinearMap.Simps.apply definition

(h : M₁ →SL[σ₁₂] M₂) : M₁ → M₂

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 : M₁ →SL[σ₁₂] M₂) : M₁ → M₂ :=
  h

Underlying function of a continuous semilinear map

Informal description

The function that extracts the underlying function from a continuous semilinear map $ h : M_1 \to_{SL}[\sigma_{12}] M_2 $, where $ h $ is a continuous semilinear map between topological modules $ M_1 $ and $ M_2 $ with respect to the ring homomorphism $ \sigma_{12} $.

ContinuousLinearMap.Simps.coe definition

(h : M₁ →SL[σ₁₂] M₂) : M₁ →ₛₗ[σ₁₂] M₂

Full source

/-- See Note [custom simps projection]. -/
def Simps.coe (h : M₁ →SL[σ₁₂] M₂) : M₁ →ₛₗ[σ₁₂] M₂ :=
  h

Underlying semilinear map of a continuous semilinear map

Informal description

The function that extracts the underlying semilinear map from a continuous semilinear map $ h : M_1 \to_{SL}[\sigma_{12}] M_2 $, where $ h $ is a continuous semilinear map between topological modules $ M_1 $ and $ M_2 $ with respect to the ring homomorphism $ \sigma_{12} $.

ContinuousLinearMap.ext theorem

{f g : M₁ →SL[σ₁₂] M₂} (h : ∀ x, f x = g x) : f = g

Full source

@[ext]
theorem ext {f g : M₁ →SL[σ₁₂] M₂} (h : ∀ x, f x = g x) : f = g :=
  DFunLike.ext f g h

Extensionality of Continuous Semilinear Maps

Informal description

For any two continuous semilinear maps $f, g \colon M_1 \to_{SL[\sigma_{12}]} M_2$, if $f(x) = g(x)$ for all $x \in M_1$, then $f = g$.

ContinuousLinearMap.copy definition

(f : M₁ →SL[σ₁₂] M₂) (f' : M₁ → M₂) (h : f' = ⇑f) : M₁ →SL[σ₁₂] M₂

Full source

/-- Copy of a `ContinuousLinearMap` with a new `toFun` equal to the old one. Useful to fix
definitional equalities. -/
protected def copy (f : M₁ →SL[σ₁₂] M₂) (f' : M₁ → M₂) (h : f' = ⇑f) : M₁ →SL[σ₁₂] M₂ where
  toLinearMap := f.toLinearMap.copy f' h
  cont := show Continuous f' from h.symm ▸ f.continuous

Copy of a continuous semilinear map with a new underlying function

Informal description

Given a continuous semilinear map $ f \colon M_1 \to_{SL[\sigma_{12}]} M_2 $ and a function $ f' \colon M_1 \to M_2 $ that is definitionally equal to $ f $, the function `ContinuousLinearMap.copy` constructs a new continuous semilinear map with the underlying function $ f' $, maintaining the same linear and continuity properties as $ f $.

ContinuousLinearMap.coe_copy theorem

(f : M₁ →SL[σ₁₂] M₂) (f' : M₁ → M₂) (h : f' = ⇑f) : ⇑(f.copy f' h) = f'

Full source

@[simp]
theorem coe_copy (f : M₁ →SL[σ₁₂] M₂) (f' : M₁ → M₂) (h : f' = ⇑f) : ⇑(f.copy f' h) = f' :=
  rfl

Underlying Function of Copied Continuous Semilinear Map Equals Given Function

Informal description

For any continuous semilinear map $f \colon M_1 \to_{SL[\sigma_{12}]} M_2$, function $f' \colon M_1 \to M_2$ satisfying $f' = f$, the underlying function of the copied map $f.copy\ f'\ h$ equals $f'$.

ContinuousLinearMap.copy_eq theorem

(f : M₁ →SL[σ₁₂] M₂) (f' : M₁ → M₂) (h : f' = ⇑f) : f.copy f' h = f

Full source

theorem copy_eq (f : M₁ →SL[σ₁₂] M₂) (f' : M₁ → M₂) (h : f' = ⇑f) : f.copy f' h = f :=
  DFunLike.ext' h

Copy of Continuous Semilinear Map with Identical Underlying Function is Itself

Informal description

Let $f \colon M_1 \to_{SL[\sigma_{12}]} M_2$ be a continuous semilinear map, and let $f' \colon M_1 \to M_2$ be a function such that $f' = f$. Then the copy of $f$ with underlying function $f'$ is equal to $f$ itself, i.e., $f.\text{copy}(f', h) = f$.

ContinuousLinearMap.range_coeFn_eq theorem

 : Set.range ((⇑) : (M₁ →SL[σ₁₂] M₂) → (M₁ → M₂)) = {f | Continuous f} ∩ Set.range ((⇑) : (M₁ →ₛₗ[σ₁₂] M₂) → (M₁ → M₂))

Full source

theorem range_coeFn_eq :
    Set.range ((⇑) : (M₁ →SL[σ₁₂] M₂) → (M₁ → M₂)) =
      {f | Continuous f}{f | Continuous f} ∩ Set.range ((⇑) : (M₁ →ₛₗ[σ₁₂] M₂) → (M₁ → M₂)) := by
  ext f
  constructor
  · rintro ⟨f, rfl⟩
    exact ⟨f.continuous, f, rfl⟩
  · rintro ⟨hfc, f, rfl⟩
    exact ⟨⟨f, hfc⟩, rfl⟩

Range of Continuous Semilinear Map Coercion Equals Intersection of Continuous Functions and Semilinear Map Coercion Range

Informal description

The range of the coercion function from continuous semilinear maps $M_1 \to_{SL[\sigma_{12}]} M_2$ to functions $M_1 \to M_2$ is equal to the intersection of the set of continuous functions $M_1 \to M_2$ and the range of the coercion function from semilinear maps $M_1 \to_{SL[\sigma_{12}]} M_2$ to functions $M_1 \to M_2$.

ContinuousLinearMap.map_zero theorem

(f : M₁ →SL[σ₁₂] M₂) : f (0 : M₁) = 0

Full source

protected theorem map_zero (f : M₁ →SL[σ₁₂] M₂) : f (0 : M₁) = 0 :=
  map_zero f

Continuous semilinear maps preserve zero

Informal description

For any continuous semilinear map $f \colon M_1 \to_{SL[\sigma_{12}]} M_2$ between topological modules, the image of the zero vector in $M_1$ is the zero vector in $M_2$, i.e., $f(0) = 0$.

ContinuousLinearMap.map_add theorem

(f : M₁ →SL[σ₁₂] M₂) (x y : M₁) : f (x + y) = f x + f y

Full source

protected theorem map_add (f : M₁ →SL[σ₁₂] M₂) (x y : M₁) : f (x + y) = f x + f y :=
  map_add f x y

Additivity of Continuous Semilinear Maps

Informal description

For any continuous semilinear map $f \colon M_1 \to_{SL[\sigma_{12}]} M_2$ between topological modules $M_1$ and $M_2$, and for any elements $x, y \in M_1$, the map $f$ satisfies the additive property: \[ f(x + y) = f(x) + f(y). \]

ContinuousLinearMap.map_smulₛₗ theorem

(f : M₁ →SL[σ₁₂] M₂) (c : R₁) (x : M₁) : f (c • x) = σ₁₂ c • f x

Full source

@[simp]
protected theorem map_smulₛₗ (f : M₁ →SL[σ₁₂] M₂) (c : R₁) (x : M₁) : f (c • x) = σ₁₂ c • f x :=
  (toLinearMap _).map_smulₛₗ _ _

Scalar Multiplication Property of Continuous Semilinear Maps

Informal description

Let $R_1$ and $R_2$ be semirings, $M_1$ be a topological module over $R_1$, and $M_2$ be a topological module over $R_2$. Given a ring homomorphism $\sigma: R_1 \to R_2$ and a continuous semilinear map $f: M_1 \to_{SL[\sigma]} M_2$, then for any scalar $c \in R_1$ and any vector $x \in M_1$, we have $f(c \cdot x) = \sigma(c) \cdot f(x)$.

ContinuousLinearMap.map_smul theorem

[Module R₁ M₂] (f : M₁ →L[R₁] M₂) (c : R₁) (x : M₁) : f (c • x) = c • f x

Full source

protected theorem map_smul [Module R₁ M₂] (f : M₁ →L[R₁] M₂) (c : R₁) (x : M₁) :
    f (c • x) = c • f x := by simp only [RingHom.id_apply, ContinuousLinearMap.map_smulₛₗ]

Scalar Multiplication Preservation for Continuous Linear Maps

Informal description

Let $R_1$ be a semiring, and let $M_1$ and $M_2$ be topological modules over $R_1$. For any continuous $R_1$-linear map $f \colon M_1 \to M_2$, scalar $c \in R_1$, and vector $x \in M_1$, we have $f(c \cdot x) = c \cdot f(x)$.

ContinuousLinearMap.map_smul_of_tower theorem

 {R S : Type*} [Semiring S] [SMul R M₁] [Module S M₁] [SMul R M₂] [Module S M₂] [LinearMap.CompatibleSMul M₁ M₂ R S]
  (f : M₁ →L[S] M₂) (c : R) (x : M₁) : f (c • x) = c • f x

Full source

@[simp]
theorem map_smul_of_tower {R S : Type*} [Semiring S] [SMul R M₁] [Module S M₁] [SMul R M₂]
    [Module S M₂] [LinearMap.CompatibleSMul M₁ M₂ R S] (f : M₁ →L[S] M₂) (c : R) (x : M₁) :
    f (c • x) = c • f x :=
  LinearMap.CompatibleSMul.map_smul (f : M₁ →ₗ[S] M₂) c x

Scalar Multiplication Preservation for Continuous Linear Maps with Compatible Actions

Informal description

Let $R$ and $S$ be semirings, with $M_1$ and $M_2$ being topological modules over $S$ that are also equipped with a scalar multiplication by $R$ compatible with the $S$-module structure. For any continuous $S$-linear map $f: M_1 \to M_2$, scalar $c \in R$, and vector $x \in M_1$, we have $f(c \cdot x) = c \cdot f(x)$.

ContinuousLinearMap.coe_coe theorem

(f : M₁ →SL[σ₁₂] M₂) : ⇑(f : M₁ →ₛₗ[σ₁₂] M₂) = f

Full source

@[simp, norm_cast]
theorem coe_coe (f : M₁ →SL[σ₁₂] M₂) : ⇑(f : M₁ →ₛₗ[σ₁₂] M₂) = f :=
  rfl

Underlying Semilinear Map of Continuous Semilinear Map Coincides with Itself

Informal description

For any continuous semilinear map $f \colon M_1 \to_{SL[\sigma_{12}]} M_2$, the underlying function of $f$ (when viewed as a semilinear map) coincides with $f$ itself. In other words, $\tilde{f} = f$ where $\tilde{f}$ is the semilinear map associated to $f$.

ContinuousLinearMap.ext_ring theorem

[TopologicalSpace R₁] {f g : R₁ →L[R₁] M₁} (h : f 1 = g 1) : f = g

Full source

@[ext]
theorem ext_ring [TopologicalSpace R₁] {f g : R₁ →L[R₁] M₁} (h : f 1 = g 1) : f = g :=
  coe_inj.1 <| LinearMap.ext_ring h

Equality of Continuous Linear Maps via Evaluation at One

Informal description

Let $R_1$ be a topological space and a semiring, and let $M_1$ be a topological module over $R_1$. For any two continuous $R_1$-linear maps $f, g \colon R_1 \to_{L[R_1]} M_1$, if $f(1) = g(1)$, then $f = g$.

ContinuousLinearMap.eqOn_closure_span theorem

 [T2Space M₂] {s : Set M₁} {f g : M₁ →SL[σ₁₂] M₂} (h : Set.EqOn f g s) :
  Set.EqOn f g (closure (Submodule.span R₁ s : Set M₁))

Full source

/-- If two continuous linear maps are equal on a set `s`, then they are equal on the closure
of the `Submodule.span` of this set. -/
theorem eqOn_closure_span [T2Space M₂] {s : Set M₁} {f g : M₁ →SL[σ₁₂] M₂} (h : Set.EqOn f g s) :
    Set.EqOn f g (closure (Submodule.span R₁ s : Set M₁)) :=
  (LinearMap.eqOn_span' h).closure f.continuous g.continuous

Continuous Semilinear Maps Equal on Span Closure in Hausdorff Space

Informal description

Let $M_1$ and $M_2$ be topological modules over semirings $R_1$ and $R_2$ respectively, with $M_2$ being Hausdorff. Let $\sigma_{12}: R_1 \to R_2$ be a ring homomorphism, and let $f, g: M_1 \to_{SL[\sigma_{12}]} M_2$ be continuous semilinear maps. If $f$ and $g$ agree on a subset $s \subseteq M_1$, then they also agree on the closure of the $R_1$-linear span of $s$.

ContinuousLinearMap.ext_on theorem

 [T2Space M₂] {s : Set M₁} (hs : Dense (Submodule.span R₁ s : Set M₁)) {f g : M₁ →SL[σ₁₂] M₂} (h : Set.EqOn f g s) :
  f = g

Full source

/-- If the submodule generated by a set `s` is dense in the ambient module, then two continuous
linear maps equal on `s` are equal. -/
theorem ext_on [T2Space M₂] {s : Set M₁} (hs : Dense (Submodule.span R₁ s : Set M₁))
    {f g : M₁ →SL[σ₁₂] M₂} (h : Set.EqOn f g s) : f = g :=
  ext fun x => eqOn_closure_span h (hs x)

Uniqueness of Continuous Semilinear Maps on Dense Span in Hausdorff Space

Informal description

Let $M_1$ and $M_2$ be topological modules over semirings $R_1$ and $R_2$ respectively, with $M_2$ being Hausdorff. Let $\sigma_{12} \colon R_1 \to R_2$ be a ring homomorphism, and let $f, g \colon M_1 \to_{SL[\sigma_{12}]} M_2$ be continuous semilinear maps. If $f$ and $g$ agree on a subset $s \subseteq M_1$ and the $R_1$-linear span of $s$ is dense in $M_1$, then $f = g$.

Submodule.topologicalClosure_map theorem

 [RingHomSurjective σ₁₂] [TopologicalSpace R₁] [TopologicalSpace R₂] [ContinuousSMul R₁ M₁] [ContinuousAdd M₁]
  [ContinuousSMul R₂ M₂] [ContinuousAdd M₂] (f : M₁ →SL[σ₁₂] M₂) (s : Submodule R₁ M₁) :
  s.topologicalClosure.map (f : M₁ →ₛₗ[σ₁₂] M₂) ≤ (s.map (f : M₁ →ₛₗ[σ₁₂] M₂)).topologicalClosure

Full source

/-- Under a continuous linear map, the image of the `TopologicalClosure` of a submodule is
contained in the `TopologicalClosure` of its image. -/
theorem _root_.Submodule.topologicalClosure_map [RingHomSurjective σ₁₂] [TopologicalSpace R₁]
    [TopologicalSpace R₂] [ContinuousSMul R₁ M₁] [ContinuousAdd M₁] [ContinuousSMul R₂ M₂]
    [ContinuousAdd M₂] (f : M₁ →SL[σ₁₂] M₂) (s : Submodule R₁ M₁) :
    s.topologicalClosure.map (f : M₁ →ₛₗ[σ₁₂] M₂) ≤
      (s.map (f : M₁ →ₛₗ[σ₁₂] M₂)).topologicalClosure :=
  image_closure_subset_closure_image f.continuous

Image of Submodule Closure under Continuous Semilinear Map is Contained in Closure of Image

Informal description

Let $R_1$ and $R_2$ be topological semirings, and let $M_1$ and $M_2$ be topological modules over $R_1$ and $R_2$ respectively, with continuous scalar multiplication and addition. Let $\sigma_{12} \colon R_1 \to R_2$ be a surjective ring homomorphism, and let $f \colon M_1 \to_{SL[\sigma_{12}]} M_2$ be a continuous semilinear map. For any submodule $s$ of $M_1$, the image under $f$ of the topological closure of $s$ is contained in the topological closure of the image of $s$ under $f$. In other words, $$ f(\overline{s}) \subseteq \overline{f(s)}. $$

DenseRange.topologicalClosure_map_submodule theorem

 [RingHomSurjective σ₁₂] [TopologicalSpace R₁] [TopologicalSpace R₂] [ContinuousSMul R₁ M₁] [ContinuousAdd M₁]
  [ContinuousSMul R₂ M₂] [ContinuousAdd M₂] {f : M₁ →SL[σ₁₂] M₂} (hf' : DenseRange f) {s : Submodule R₁ M₁}
  (hs : s.topologicalClosure = ⊤) : (s.map (f : M₁ →ₛₗ[σ₁₂] M₂)).topologicalClosure = ⊤

Full source

/-- Under a dense continuous linear map, a submodule whose `TopologicalClosure` is `⊤` is sent to
another such submodule.  That is, the image of a dense set under a map with dense range is dense.
-/
theorem _root_.DenseRange.topologicalClosure_map_submodule [RingHomSurjective σ₁₂]
    [TopologicalSpace R₁] [TopologicalSpace R₂] [ContinuousSMul R₁ M₁] [ContinuousAdd M₁]
    [ContinuousSMul R₂ M₂] [ContinuousAdd M₂] {f : M₁ →SL[σ₁₂] M₂} (hf' : DenseRange f)
    {s : Submodule R₁ M₁} (hs : s.topologicalClosure = ⊤) :
    (s.map (f : M₁ →ₛₗ[σ₁₂] M₂)).topologicalClosure = ⊤ := by
  rw [SetLike.ext'_iff] at hs ⊢
  simp only [Submodule.topologicalClosure_coe, Submodule.top_coe, ← dense_iff_closure_eq] at hs ⊢
  exact hf'.dense_image f.continuous hs

Density Preservation of Submodule Images under Continuous Semilinear Maps with Dense Range

Informal description

Let $R_1$ and $R_2$ be topological semirings, $M_1$ and $M_2$ be topological modules over $R_1$ and $R_2$ respectively with continuous scalar multiplication and addition, and $\sigma_{12} \colon R_1 \to R_2$ be a surjective ring homomorphism. Given a continuous semilinear map $f \colon M_1 \to_{SL[\sigma_{12}]} M_2$ with dense range, and a submodule $s$ of $M_1$ whose topological closure is the entire space $M_1$, the topological closure of the image submodule $f(s)$ is the entire space $M_2$.

ContinuousLinearMap.instSMul instance

: SMul S₂ (M₁ →SL[σ₁₂] M₂)

Full source

instance instSMul : SMul S₂ (M₁ →SL[σ₁₂] M₂) where
  smul c f := ⟨c • (f : M₁ →ₛₗ[σ₁₂] M₂), (f.2.const_smul _ : Continuous fun x => c • f x)⟩

Scalar Multiplication on Continuous Semilinear Maps

Informal description

For any semiring $S₂$, the set of continuous semilinear maps $M₁ \toSL[σ₁₂] M₂$ has a scalar multiplication structure by elements of $S₂$.

ContinuousLinearMap.mulAction instance

: MulAction S₂ (M₁ →SL[σ₁₂] M₂)

Full source

instance mulAction : MulAction S₂ (M₁ →SL[σ₁₂] M₂) where
  one_smul _f := ext fun _x => one_smul _ _
  mul_smul _a _b _f := ext fun _x => mul_smul _ _ _

Multiplicative Action on Continuous Semilinear Maps

Informal description

For any semiring $S₂$, the set of continuous semilinear maps $M₁ \toSL[σ₁₂] M₂$ forms a multiplicative action by elements of $S₂$. That is, there is a well-defined operation $(c, f) \mapsto c \cdot f$ for $c \in S₂$ and $f \in M₁ \toSL[σ₁₂] M₂$ that satisfies the multiplicative action axioms.

ContinuousLinearMap.smul_apply theorem

(c : S₂) (f : M₁ →SL[σ₁₂] M₂) (x : M₁) : (c • f) x = c • f x

Full source

theorem smul_apply (c : S₂) (f : M₁ →SL[σ₁₂] M₂) (x : M₁) : (c • f) x = c • f x :=
  rfl

Scalar Multiplication Commutes with Evaluation for Continuous Semilinear Maps

Informal description

For any scalar $c \in S₂$, any continuous semilinear map $f \colon M₁ \toSL[σ₁₂] M₂$, and any element $x \in M₁$, the evaluation of the scalar multiple $c \cdot f$ at $x$ is equal to the scalar multiple $c$ applied to the evaluation of $f$ at $x$, i.e., $(c \cdot f)(x) = c \cdot f(x)$.

ContinuousLinearMap.coe_smul theorem

(c : S₂) (f : M₁ →SL[σ₁₂] M₂) : ↑(c • f) = c • (f : M₁ →ₛₗ[σ₁₂] M₂)

Full source

@[simp, norm_cast]
theorem coe_smul (c : S₂) (f : M₁ →SL[σ₁₂] M₂) :
    ↑(c • f) = c • (f : M₁ →ₛₗ[σ₁₂] M₂) :=
  rfl

Scalar multiplication commutes with coercion to semilinear maps

Informal description

For any scalar $c \in S₂$ and any continuous semilinear map $f \colon M₁ \toSL[σ₁₂] M₂$, the underlying semilinear map of the scalar multiple $c \cdot f$ is equal to the scalar multiple $c \cdot (f \colon M₁ \toₛₗ[σ₁₂] M₂)$.

ContinuousLinearMap.coe_smul' theorem

(c : S₂) (f : M₁ →SL[σ₁₂] M₂) : ↑(c • f) = c • (f : M₁ → M₂)

Full source

@[simp, norm_cast]
theorem coe_smul' (c : S₂) (f : M₁ →SL[σ₁₂] M₂) :
    ↑(c • f) = c • (f : M₁ → M₂) :=
  rfl

Pointwise Scalar Multiplication of Continuous Semilinear Maps

Informal description

For any scalar $c \in S₂$ and any continuous semilinear map $f \colon M₁ \toSL[σ₁₂] M₂$, the underlying function of the scalar multiple $c \cdot f$ is equal to the pointwise scalar multiple of the underlying function of $f$, i.e., $(c \cdot f)(x) = c \cdot f(x)$ for all $x \in M₁$.

ContinuousLinearMap.isScalarTower instance

[SMul S₂ T₂] [IsScalarTower S₂ T₂ M₂] : IsScalarTower S₂ T₂ (M₁ →SL[σ₁₂] M₂)

Full source

instance isScalarTower [SMul S₂ T₂] [IsScalarTower S₂ T₂ M₂] :
    IsScalarTower S₂ T₂ (M₁ →SL[σ₁₂] M₂) :=
  ⟨fun a b f => ext fun x => smul_assoc a b (f x)⟩

Scalar Tower Property for Continuous Semilinear Maps

Informal description

For any semirings $S₂$ and $T₂$ with a scalar multiplication action on $M₂$ that forms a scalar tower (i.e., $(s \cdot t) \cdot m = s \cdot (t \cdot m)$ for all $s \in S₂$, $t \in T₂$, $m \in M₂$), the set of continuous semilinear maps $M₁ \toSL[σ₁₂] M₂$ also forms a scalar tower with respect to the same scalar multiplication actions.

ContinuousLinearMap.smulCommClass instance

[SMulCommClass S₂ T₂ M₂] : SMulCommClass S₂ T₂ (M₁ →SL[σ₁₂] M₂)

Full source

instance smulCommClass [SMulCommClass S₂ T₂ M₂] : SMulCommClass S₂ T₂ (M₁ →SL[σ₁₂] M₂) :=
  ⟨fun a b f => ext fun x => smul_comm a b (f x)⟩

Commuting Scalar Actions on Continuous Semilinear Maps

Informal description

For any semirings $S₂$ and $T₂$ acting on $M₂$ with commuting scalar multiplications, the scalar multiplications by $S₂$ and $T₂$ on the space of continuous semilinear maps $M₁ \toSL[σ₁₂] M₂$ also commute.

ContinuousLinearMap.zero instance

: Zero (M₁ →SL[σ₁₂] M₂)

Full source

/-- The continuous map that is constantly zero. -/
instance zero : Zero (M₁ →SL[σ₁₂] M₂) :=
  ⟨⟨0, continuous_zero⟩⟩

The Zero Continuous Linear Map

Informal description

The zero map between topological modules $M_1$ and $M_2$ is a continuous linear map. Specifically, the map that sends every element of $M_1$ to the zero element of $M_2$ is continuous and linear with respect to the ring homomorphism $\sigma_{12}$.

ContinuousLinearMap.inhabited instance

: Inhabited (M₁ →SL[σ₁₂] M₂)

Full source

instance inhabited : Inhabited (M₁ →SL[σ₁₂] M₂) :=
  ⟨0⟩

Inhabited Space of Continuous Semilinear Maps

Informal description

The space of continuous semilinear maps between topological modules $M_1$ and $M_2$ (with respect to a ring homomorphism $\sigma_{12}$) is always inhabited, with the zero map as a canonical element.

ContinuousLinearMap.default_def theorem

: (default : M₁ →SL[σ₁₂] M₂) = 0

Full source

@[simp]
theorem default_def : (default : M₁ →SL[σ₁₂] M₂) = 0 :=
  rfl

Default Continuous Semilinear Map is Zero Map

Informal description

The default continuous semilinear map from $M_1$ to $M_2$ (with respect to the ring homomorphism $\sigma_{12}$) is equal to the zero map.

ContinuousLinearMap.zero_apply theorem

(x : M₁) : (0 : M₁ →SL[σ₁₂] M₂) x = 0

Full source

@[simp]
theorem zero_apply (x : M₁) : (0 : M₁ →SL[σ₁₂] M₂) x = 0 :=
  rfl

Zero Continuous Semilinear Map Evaluates to Zero

Informal description

For any element $x$ in the topological module $M_1$, the zero continuous semilinear map evaluated at $x$ equals the zero element in $M_2$, i.e., $(0 : M_1 \to_{SL[\sigma_{12}]} M_2)(x) = 0$.

ContinuousLinearMap.coe_zero theorem

: ((0 : M₁ →SL[σ₁₂] M₂) : M₁ →ₛₗ[σ₁₂] M₂) = 0

Full source

@[simp, norm_cast]
theorem coe_zero : ((0 : M₁ →SL[σ₁₂] M₂) : M₁ →ₛₗ[σ₁₂] M₂) = 0 :=
  rfl

Zero Continuous Linear Map Coerces to Zero Semilinear Map

Informal description

The zero continuous linear map from $M_1$ to $M_2$ (with respect to the ring homomorphism $\sigma_{12}$), when viewed as a semilinear map, is equal to the zero semilinear map. In other words, the coercion of the zero continuous linear map to a semilinear map yields the zero semilinear map.

ContinuousLinearMap.coe_zero' theorem

: ⇑(0 : M₁ →SL[σ₁₂] M₂) = 0

Full source

@[norm_cast]
theorem coe_zero' : ⇑(0 : M₁ →SL[σ₁₂] M₂) = 0 :=
  rfl

Zero continuous semilinear map is the zero function

Informal description

The zero continuous semilinear map from $M_1$ to $M_2$ (with respect to the ring homomorphism $\sigma_{12}$) is equal to the zero function, i.e., $0(x) = 0$ for all $x \in M_1$.

ContinuousLinearMap.toContinuousAddMonoidHom_zero theorem

: ((0 : M₁ →SL[σ₁₂] M₂) : ContinuousAddMonoidHom M₁ M₂) = 0

Full source

@[simp, norm_cast]
theorem toContinuousAddMonoidHom_zero :
    ((0 : M₁ →SL[σ₁₂] M₂) : ContinuousAddMonoidHom M₁ M₂) = 0 := rfl

Zero Continuous Linear Map as Zero Continuous Additive Monoid Homomorphism

Informal description

The zero continuous linear map from $M_1$ to $M_2$ (with respect to the ring homomorphism $\sigma_{12}$), when viewed as a continuous additive monoid homomorphism, is equal to the zero continuous additive monoid homomorphism.

ContinuousLinearMap.uniqueOfLeft instance

[Subsingleton M₁] : Unique (M₁ →SL[σ₁₂] M₂)

Full source

instance uniqueOfLeft [Subsingleton M₁] : Unique (M₁ →SL[σ₁₂] M₂) :=
  coe_injective.unique

Uniqueness of Continuous Semilinear Maps from a Subsingleton

Informal description

If the topological module $M_1$ is a subsingleton (i.e., has at most one element), then the space of continuous semilinear maps from $M_1$ to $M_2$ (with respect to the ring homomorphism $\sigma_{12}$) has exactly one element.

ContinuousLinearMap.uniqueOfRight instance

[Subsingleton M₂] : Unique (M₁ →SL[σ₁₂] M₂)

Full source

instance uniqueOfRight [Subsingleton M₂] : Unique (M₁ →SL[σ₁₂] M₂) :=
  coe_injective.unique

Uniqueness of Continuous Semilinear Maps to a Subsingleton

Informal description

If the topological module $M_2$ is a subsingleton (i.e., has at most one element), then the space of continuous semilinear maps from $M_1$ to $M_2$ (with respect to a ring homomorphism $\sigma_{12}$) has exactly one element.

ContinuousLinearMap.exists_ne_zero theorem

{f : M₁ →SL[σ₁₂] M₂} (hf : f ≠ 0) : ∃ x, f x ≠ 0

Full source

theorem exists_ne_zero {f : M₁ →SL[σ₁₂] M₂} (hf : f ≠ 0) : ∃ x, f x ≠ 0 := by
  by_contra! h
  exact hf (ContinuousLinearMap.ext h)

Nonzero Continuous Semilinear Maps Have Nonzero Values

Informal description

For any nonzero continuous semilinear map $f \colon M_1 \to_{SL[\sigma_{12}]} M_2$, there exists an element $x \in M_1$ such that $f(x) \neq 0$.

ContinuousLinearMap.id definition

: M₁ →L[R₁] M₁

Full source

/-- the identity map as a continuous linear map. -/
def id : M₁ →L[R₁] M₁ :=
  ⟨LinearMap.id, continuous_id⟩

Identity continuous linear map

Informal description

The identity map on a topological module $M_1$ over a semiring $R_1$, viewed as a continuous linear map from $M_1$ to itself.

ContinuousLinearMap.one instance

: One (M₁ →L[R₁] M₁)

Full source

instance one : One (M₁ →L[R₁] M₁) :=
  ⟨id R₁ M₁⟩

Identity as the Multiplicative Unit for Continuous Linear Maps

Informal description

The space of continuous linear maps from a topological module $M_1$ to itself over a semiring $R_1$ has a multiplicative identity element, given by the identity map.

ContinuousLinearMap.one_def theorem

: (1 : M₁ →L[R₁] M₁) = id R₁ M₁

Full source

theorem one_def : (1 : M₁ →L[R₁] M₁) = id R₁ M₁ :=
  rfl

Identity Continuous Linear Map as Multiplicative Unit: $1 = \text{id}$

Informal description

The multiplicative identity element in the space of continuous linear maps from a topological module $M_1$ to itself over a semiring $R_1$ is equal to the identity continuous linear map, i.e., $1 = \text{id}_{R_1}$.

ContinuousLinearMap.id_apply theorem

(x : M₁) : id R₁ M₁ x = x

Full source

theorem id_apply (x : M₁) : id R₁ M₁ x = x :=
  rfl

Identity Continuous Linear Map Evaluation: $\text{id}(x) = x$

Informal description

For any element $x$ in the topological module $M_1$ over the semiring $R_1$, the identity continuous linear map evaluated at $x$ equals $x$, i.e., $\text{id}_{R_1}(x) = x$.

ContinuousLinearMap.coe_id theorem

: (id R₁ M₁ : M₁ →ₗ[R₁] M₁) = LinearMap.id

Full source

@[simp, norm_cast]
theorem coe_id : (id R₁ M₁ : M₁ →ₗ[R₁] M₁) = LinearMap.id :=
  rfl

Identity Continuous Linear Map as Identity Linear Map

Informal description

The underlying linear map of the identity continuous linear map on a topological module $M_1$ over a semiring $R_1$ is equal to the identity linear map on $M_1$.

ContinuousLinearMap.coe_id' theorem

: ⇑(id R₁ M₁) = _root_.id

Full source

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

Identity Continuous Linear Map as Identity Function

Informal description

The underlying function of the identity continuous linear map on a topological module $M_1$ over a semiring $R_1$ is equal to the identity function on $M_1$.

ContinuousLinearMap.toContinuousAddMonoidHom_id theorem

: (id R₁ M₁ : ContinuousAddMonoidHom M₁ M₁) = .id _

Full source

@[simp, norm_cast]
theorem toContinuousAddMonoidHom_id :
    (id R₁ M₁ : ContinuousAddMonoidHom M₁ M₁) = .id _ := rfl

Identity Continuous Linear Map as Identity Continuous Additive Monoid Homomorphism

Informal description

The identity continuous linear map on a topological module $M_1$ over a semiring $R_1$, when viewed as a continuous additive monoid homomorphism, is equal to the identity continuous additive monoid homomorphism on $M_1$.

ContinuousLinearMap.coe_eq_id theorem

{f : M₁ →L[R₁] M₁} : (f : M₁ →ₗ[R₁] M₁) = LinearMap.id ↔ f = id _ _

Full source

@[simp, norm_cast]
theorem coe_eq_id {f : M₁ →L[R₁] M₁} : (f : M₁ →ₗ[R₁] M₁) = LinearMap.id ↔ f = id _ _ := by
  rw [← coe_id, coe_inj]

Identity Criterion for Continuous Linear Maps via Underlying Linear Maps

Informal description

For any continuous linear map $f \colon M_1 \to_{L[R_1]} M_1$ on a topological module $M_1$ over a semiring $R_1$, the underlying linear map of $f$ is equal to the identity linear map if and only if $f$ is equal to the identity continuous linear map on $M_1$.

ContinuousLinearMap.one_apply theorem

(x : M₁) : (1 : M₁ →L[R₁] M₁) x = x

Full source

@[simp]
theorem one_apply (x : M₁) : (1 : M₁ →L[R₁] M₁) x = x :=
  rfl

Identity Continuous Linear Map Acts as Identity on Elements

Informal description

For any element $x$ in a topological module $M_1$ over a semiring $R_1$, the identity continuous linear map $1$ evaluated at $x$ equals $x$, i.e., $1(x) = x$.

ContinuousLinearMap.instNontrivialId instance

[Nontrivial M₁] : Nontrivial (M₁ →L[R₁] M₁)

Full source

instance [Nontrivial M₁] : Nontrivial (M₁ →L[R₁] M₁) :=
  ⟨0, 1, fun e ↦
    have ⟨x, hx⟩ := exists_ne (0 : M₁); hx (by simpa using DFunLike.congr_fun e.symm x)⟩

Nontriviality of Continuous Linear Maps on Nontrivial Modules

Informal description

For any nontrivial topological module $M_1$ over a semiring $R_1$, the space of continuous linear maps from $M_1$ to itself is also nontrivial.

ContinuousLinearMap.add instance

: Add (M₁ →SL[σ₁₂] M₂)

Full source

instance add : Add (M₁ →SL[σ₁₂] M₂) :=
  ⟨fun f g => ⟨f + g, f.2.add g.2⟩⟩

Additive Structure of Continuous Semilinear Maps

Informal description

The set of continuous semilinear maps between topological modules $M_1$ and $M_2$ (with respect to a ring homomorphism $\sigma_{12}: R_1 \to R_2$) forms an additive structure, where addition is defined pointwise.

ContinuousLinearMap.add_apply theorem

(f g : M₁ →SL[σ₁₂] M₂) (x : M₁) : (f + g) x = f x + g x

Full source

@[simp]
theorem add_apply (f g : M₁ →SL[σ₁₂] M₂) (x : M₁) : (f + g) x = f x + g x :=
  rfl

Pointwise Addition of Continuous Semilinear Maps

Informal description

For any two continuous semilinear maps $f, g: M_1 \to_{SL[\sigma_{12}]} M_2$ and any element $x \in M_1$, the evaluation of their sum at $x$ satisfies $(f + g)(x) = f(x) + g(x)$.

ContinuousLinearMap.coe_add theorem

(f g : M₁ →SL[σ₁₂] M₂) : (↑(f + g) : M₁ →ₛₗ[σ₁₂] M₂) = f + g

Full source

@[simp, norm_cast]
theorem coe_add (f g : M₁ →SL[σ₁₂] M₂) : (↑(f + g) : M₁ →ₛₗ[σ₁₂] M₂) = f + g :=
  rfl

Underlying Semilinear Map of Sum Equals Pointwise Sum

Informal description

For any two continuous semilinear maps $f, g: M_1 \to_{SL[\sigma_{12}]} M_2$ between topological modules, the underlying semilinear map of their sum $f + g$ is equal to the pointwise sum of the underlying semilinear maps of $f$ and $g$.

ContinuousLinearMap.coe_add' theorem

(f g : M₁ →SL[σ₁₂] M₂) : ⇑(f + g) = f + g

Full source

@[norm_cast]
theorem coe_add' (f g : M₁ →SL[σ₁₂] M₂) : ⇑(f + g) = f + g :=
  rfl

Pointwise Sum of Continuous Semilinear Maps

Informal description

For any two continuous semilinear maps $ f, g: M_1 \to_{SL[\sigma_{12}]} M_2 $, the underlying function of their sum $ f + g $ is equal to the pointwise sum of the underlying functions of $ f $ and $ g $. That is, $ (f + g)(x) = f(x) + g(x) $ for all $ x \in M_1 $.

ContinuousLinearMap.toContinuousAddMonoidHom_add theorem

(f g : M₁ →SL[σ₁₂] M₂) : ↑(f + g) = (f + g : ContinuousAddMonoidHom M₁ M₂)

Full source

@[simp, norm_cast]
theorem toContinuousAddMonoidHom_add (f g : M₁ →SL[σ₁₂] M₂) :
    ↑(f + g) = (f + g : ContinuousAddMonoidHom M₁ M₂) := rfl

Sum of Continuous Semilinear Maps Preserved Under Canonical Map to Continuous Additive Monoid Homomorphisms

Informal description

For any two continuous semilinear maps $ f, g: M_1 \to_{SL[\sigma_{12}]} M_2 $, the image of their sum under the canonical map to continuous additive monoid homomorphisms is equal to the sum of their images, i.e., $ \uparrow(f + g) = f + g $ as elements of the space of continuous additive monoid homomorphisms from $ M_1 $ to $ M_2 $.

ContinuousLinearMap.addCommMonoid instance

: AddCommMonoid (M₁ →SL[σ₁₂] M₂)

Full source

instance addCommMonoid : AddCommMonoid (M₁ →SL[σ₁₂] M₂) where
  zero_add := by
    intros
    ext
    apply_rules [zero_add, add_assoc, add_zero, neg_add_cancel, add_comm]
  add_zero := by
    intros
    ext
    apply_rules [zero_add, add_assoc, add_zero, neg_add_cancel, add_comm]
  add_comm := by
    intros
    ext
    apply_rules [zero_add, add_assoc, add_zero, neg_add_cancel, add_comm]
  add_assoc := by
    intros
    ext
    apply_rules [zero_add, add_assoc, add_zero, neg_add_cancel, add_comm]
  nsmul := (· • ·)
  nsmul_zero f := by
    ext
    simp
  nsmul_succ n f := by
    ext
    simp [add_smul]

Additive Commutative Monoid Structure on Continuous Semilinear Maps

Informal description

The set of continuous semilinear maps between topological modules $M_1$ and $M_2$ (with respect to a ring homomorphism $\sigma_{12}: R_1 \to R_2$) forms an additive commutative monoid under pointwise addition.

ContinuousLinearMap.coe_sum theorem

 {ι : Type*} (t : Finset ι) (f : ι → M₁ →SL[σ₁₂] M₂) : ↑(∑ d ∈ t, f d) = (∑ d ∈ t, f d : M₁ →ₛₗ[σ₁₂] M₂)

Full source

@[simp, norm_cast]
theorem coe_sum {ι : Type*} (t : Finset ι) (f : ι → M₁ →SL[σ₁₂] M₂) :
    ↑(∑ d ∈ t, f d) = (∑ d ∈ t, f d : M₁ →ₛₗ[σ₁₂] M₂) :=
  map_sum (AddMonoidHom.mk ⟨((↑) : (M₁ →SL[σ₁₂] M₂) → M₁ →ₛₗ[σ₁₂] M₂), rfl⟩ fun _ _ => rfl) _ _

Canonical Map Preserves Sum of Continuous Semilinear Maps

Informal description

For any finite set $\iota$ and any family of continuous semilinear maps $f : \iota \to M_1 \to_{SL[\sigma_{12}]} M_2$, the canonical map from the sum of the family $\sum_{d \in t} f_d$ to the space of semilinear maps $M_1 \to_{SL[\sigma_{12}]} M_2$ is equal to the sum of the canonical maps of each individual $f_d$.

ContinuousLinearMap.coe_sum' theorem

{ι : Type*} (t : Finset ι) (f : ι → M₁ →SL[σ₁₂] M₂) : ⇑(∑ d ∈ t, f d) = ∑ d ∈ t, ⇑(f d)

Full source

@[simp, norm_cast]
theorem coe_sum' {ι : Type*} (t : Finset ι) (f : ι → M₁ →SL[σ₁₂] M₂) :
    ⇑(∑ d ∈ t, f d) = ∑ d ∈ t, ⇑(f d) := by simp only [← coe_coe, coe_sum, LinearMap.coeFn_sum]

Sum of Continuous Semilinear Maps Acts Pointwise

Informal description

For any finite set $\iota$ and any family of continuous semilinear maps $f \colon \iota \to M_1 \to_{SL[\sigma_{12}]} M_2$, the function represented by the sum $\sum_{d \in t} f_d$ is equal to the sum of the functions represented by each $f_d$. That is, $\left(\sum_{d \in t} f_d\right)(x) = \sum_{d \in t} f_d(x)$ for all $x \in M_1$.

ContinuousLinearMap.sum_apply theorem

 {ι : Type*} (t : Finset ι) (f : ι → M₁ →SL[σ₁₂] M₂) (b : M₁) : (∑ d ∈ t, f d) b = ∑ d ∈ t, f d b

Full source

theorem sum_apply {ι : Type*} (t : Finset ι) (f : ι → M₁ →SL[σ₁₂] M₂) (b : M₁) :
    (∑ d ∈ t, f d) b = ∑ d ∈ t, f d b := by simp only [coe_sum', Finset.sum_apply]

Pointwise Summation of Continuous Semilinear Maps

Informal description

For any finite set $\iota$, any family of continuous semilinear maps $f \colon \iota \to M_1 \to_{SL[\sigma_{12}]} M_2$, and any element $b \in M_1$, the evaluation of the sum $\sum_{d \in t} f_d$ at $b$ equals the sum of the evaluations $\sum_{d \in t} f_d(b)$.

ContinuousLinearMap.comp definition

(g : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) : M₁ →SL[σ₁₃] M₃

Full source

/-- Composition of bounded linear maps. -/
def comp (g : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) : M₁ →SL[σ₁₃] M₃ :=
  ⟨(g : M₂ →ₛₗ[σ₂₃] M₃).comp (f : M₁ →ₛₗ[σ₁₂] M₂), g.2.comp f.2⟩

Composition of continuous semilinear maps

Informal description

Given continuous semilinear maps $ g : M_2 \to_{SL[\sigma_{23}]} M_3 $ and $ f : M_1 \to_{SL[\sigma_{12}]} M_2 $, their composition $ g \circ f $ is a continuous semilinear map from $ M_1 $ to $ M_3 $ with respect to the composite ring homomorphism $ \sigma_{13} = \sigma_{23} \circ \sigma_{12} $.

ContinuousLinearMap.term_∘L_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc comp]
infixr:80 " ∘L " =>
  @ContinuousLinearMap.comp _ _ _ _ _ _ (RingHom.id _) (RingHom.id _) (RingHom.id _) _ _ _ _ _ _ _ _
    _ _ _ _ RingHomCompTriple.ids

Composition notation for continuous linear maps

Informal description

The notation `∘L` represents the composition of continuous linear maps. For continuous linear maps `f` and `g`, `g ∘L f` denotes their composition as continuous linear maps.

ContinuousLinearMap.coe_comp theorem

 (h : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) :
  (h.comp f : M₁ →ₛₗ[σ₁₃] M₃) = (h : M₂ →ₛₗ[σ₂₃] M₃).comp (f : M₁ →ₛₗ[σ₁₂] M₂)

Full source

@[simp, norm_cast]
theorem coe_comp (h : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) :
    (h.comp f : M₁ →ₛₗ[σ₁₃] M₃) = (h : M₂ →ₛₗ[σ₂₃] M₃).comp (f : M₁ →ₛₗ[σ₁₂] M₂) :=
  rfl

Composition of Continuous Semilinear Maps Preserves Underlying Semilinear Maps

Informal description

For continuous semilinear maps $ h : M_2 \to_{SL[\sigma_{23}]} M_3 $ and $ f : M_1 \to_{SL[\sigma_{12}]} M_2 $, the underlying semilinear map of the composition $ h \circ f $ is equal to the composition of the underlying semilinear maps of $ h $ and $ f $. That is, \[ (h \circ f : M_1 \to_{SL[\sigma_{13}]} M_3) = (h : M_2 \to_{SL[\sigma_{23}]} M_3) \circ (f : M_1 \to_{SL[\sigma_{12}]} M_2). \]

ContinuousLinearMap.coe_comp' theorem

(h : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) : ⇑(h.comp f) = h ∘ f

Full source

@[simp, norm_cast]
theorem coe_comp' (h : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) : ⇑(h.comp f) = h ∘ f :=
  rfl

Composition of Continuous Semilinear Maps as Function Composition

Informal description

For any continuous semilinear maps $ h : M_2 \to_{SL[\sigma_{23}]} M_3 $ and $ f : M_1 \to_{SL[\sigma_{12}]} M_2 $, the underlying function of their composition $ h \circ f $ is equal to the composition of the underlying functions $ h $ and $ f $. That is, $ (h \circ f)(x) = h(f(x)) $ for all $ x \in M_1 $.

ContinuousLinearMap.toContinuousAddMonoidHom_comp theorem

 (h : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) :
  (↑(h.comp f) : ContinuousAddMonoidHom M₁ M₃) = (h : ContinuousAddMonoidHom M₂ M₃).comp f

Full source

@[simp, norm_cast]
theorem toContinuousAddMonoidHom_comp (h : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) :
    (↑(h.comp f) : ContinuousAddMonoidHom M₁ M₃) = (h : ContinuousAddMonoidHom M₂ M₃).comp f := rfl

Compatibility of Continuous Semilinear Map Composition with Continuous Additive Monoid Homomorphism Structure

Informal description

Let $h: M_2 \to_{SL[\sigma_{23}]} M_3$ and $f: M_1 \to_{SL[\sigma_{12}]} M_2$ be continuous semilinear maps between topological modules. Then the continuous additive monoid homomorphism associated with the composition $h \circ f$ equals the composition of the continuous additive monoid homomorphisms associated with $h$ and $f$. In other words, $\uparrow(h \circ f) = \uparrow h \circ \uparrow f$ as continuous additive monoid homomorphisms from $M_1$ to $M_3$.

ContinuousLinearMap.comp_apply theorem

(g : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) (x : M₁) : (g.comp f) x = g (f x)

Full source

theorem comp_apply (g : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) (x : M₁) : (g.comp f) x = g (f x) :=
  rfl

Composition of Continuous Semilinear Maps Evaluates Pointwise

Informal description

For any continuous semilinear maps $ g : M_2 \to_{SL[\sigma_{23}]} M_3 $ and $ f : M_1 \to_{SL[\sigma_{12}]} M_2 $, and any element $ x \in M_1 $, the composition $ g \circ f $ evaluated at $ x $ equals $ g $ evaluated at $ f(x) $, i.e., $(g \circ f)(x) = g(f(x))$.

ContinuousLinearMap.comp_id theorem

(f : M₁ →SL[σ₁₂] M₂) : f.comp (id R₁ M₁) = f

Full source

@[simp]
theorem comp_id (f : M₁ →SL[σ₁₂] M₂) : f.comp (id R₁ M₁) = f :=
  ext fun _x => rfl

Right Identity Property of Continuous Semilinear Map Composition

Informal description

For any continuous semilinear map $f \colon M_1 \to_{SL[\sigma_{12}]} M_2$, the composition of $f$ with the identity continuous linear map on $M_1$ is equal to $f$ itself, i.e., $f \circ \text{id}_{M_1} = f$.

ContinuousLinearMap.id_comp theorem

(f : M₁ →SL[σ₁₂] M₂) : (id R₂ M₂).comp f = f

Full source

@[simp]
theorem id_comp (f : M₁ →SL[σ₁₂] M₂) : (id R₂ M₂).comp f = f :=
  ext fun _x => rfl

Identity Map Composition Law for Continuous Semilinear Maps

Informal description

For any continuous semilinear map $f \colon M_1 \to_{SL[\sigma_{12}]} M_2$ between topological modules, the composition of the identity map on $M_2$ with $f$ equals $f$ itself. That is, $\mathrm{id}_{M_2} \circ f = f$.

ContinuousLinearMap.comp_zero theorem

(g : M₂ →SL[σ₂₃] M₃) : g.comp (0 : M₁ →SL[σ₁₂] M₂) = 0

Full source

@[simp]
theorem comp_zero (g : M₂ →SL[σ₂₃] M₃) : g.comp (0 : M₁ →SL[σ₁₂] M₂) = 0 := by
  ext
  simp

Composition with Zero Map Yields Zero Map

Informal description

Let $M_1$, $M_2$, and $M_3$ be topological modules over semirings $R_1$, $R_2$, and $R_3$ respectively, with ring homomorphisms $\sigma_{12} \colon R_1 \to R_2$ and $\sigma_{23} \colon R_2 \to R_3$. For any continuous semilinear map $g \colon M_2 \to_{SL[\sigma_{23}]} M_3$, the composition of $g$ with the zero map $0 \colon M_1 \to_{SL[\sigma_{12}]} M_2$ is the zero map $0 \colon M_1 \to_{SL[\sigma_{13}]} M_3$, where $\sigma_{13} = \sigma_{23} \circ \sigma_{12}$.

ContinuousLinearMap.zero_comp theorem

(f : M₁ →SL[σ₁₂] M₂) : (0 : M₂ →SL[σ₂₃] M₃).comp f = 0

Full source

@[simp]
theorem zero_comp (f : M₁ →SL[σ₁₂] M₂) : (0 : M₂ →SL[σ₂₃] M₃).comp f = 0 := by
  ext
  simp

Composition with Zero Map Yields Zero Map

Informal description

For any continuous semilinear map $f \colon M_1 \to_{SL[\sigma_{12}]} M_2$, the composition of the zero map $0 \colon M_2 \to_{SL[\sigma_{23}]} M_3$ with $f$ is equal to the zero map from $M_1$ to $M_3$.

ContinuousLinearMap.comp_add theorem

 [ContinuousAdd M₂] [ContinuousAdd M₃] (g : M₂ →SL[σ₂₃] M₃) (f₁ f₂ : M₁ →SL[σ₁₂] M₂) :
  g.comp (f₁ + f₂) = g.comp f₁ + g.comp f₂

Full source

@[simp]
theorem comp_add [ContinuousAdd M₂] [ContinuousAdd M₃] (g : M₂ →SL[σ₂₃] M₃)
    (f₁ f₂ : M₁ →SL[σ₁₂] M₂) : g.comp (f₁ + f₂) = g.comp f₁ + g.comp f₂ := by
  ext
  simp

Additivity of Composition for Continuous Semilinear Maps

Informal description

Let $M_1$, $M_2$, and $M_3$ be topological modules over semirings $R_1$, $R_2$, and $R_3$ respectively, with ring homomorphisms $\sigma_{12}: R_1 \to R_2$ and $\sigma_{23}: R_2 \to R_3$. Suppose $M_2$ and $M_3$ have continuous addition operations. For any continuous semilinear map $g: M_2 \to_{SL[\sigma_{23}]} M_3$ and any two continuous semilinear maps $f_1, f_2: M_1 \to_{SL[\sigma_{12}]} M_2$, the composition of $g$ with the sum $f_1 + f_2$ equals the sum of the compositions: \[ g \circ (f_1 + f_2) = g \circ f_1 + g \circ f_2. \]

ContinuousLinearMap.add_comp theorem

 [ContinuousAdd M₃] (g₁ g₂ : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) : (g₁ + g₂).comp f = g₁.comp f + g₂.comp f

Full source

@[simp]
theorem add_comp [ContinuousAdd M₃] (g₁ g₂ : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) :
    (g₁ + g₂).comp f = g₁.comp f + g₂.comp f := by
  ext
  simp

Distributivity of Composition over Addition for Continuous Semilinear Maps

Informal description

Let $M_1$, $M_2$, and $M_3$ be topological modules over semirings $R_1$, $R_2$, and $R_3$ respectively, with ring homomorphisms $\sigma_{12} \colon R_1 \to R_2$ and $\sigma_{23} \colon R_2 \to R_3$. Assume $M_3$ has a continuous addition operation. For any continuous semilinear maps $g_1, g_2 \colon M_2 \to_{SL[\sigma_{23}]} M_3$ and $f \colon M_1 \to_{SL[\sigma_{12}]} M_2$, the composition of the sum $g_1 + g_2$ with $f$ equals the sum of the compositions $g_1 \circ f + g_2 \circ f$. That is, $$(g_1 + g_2) \circ f = g_1 \circ f + g_2 \circ f.$$

ContinuousLinearMap.comp_finset_sum theorem

 {ι : Type*} {s : Finset ι} [ContinuousAdd M₂] [ContinuousAdd M₃] (g : M₂ →SL[σ₂₃] M₃) (f : ι → M₁ →SL[σ₁₂] M₂) :
  g.comp (∑ i ∈ s, f i) = ∑ i ∈ s, g.comp (f i)

Full source

theorem comp_finset_sum {ι : Type*} {s : Finset ι}
    [ContinuousAdd M₂] [ContinuousAdd M₃] (g : M₂ →SL[σ₂₃] M₃)
    (f : ι → M₁ →SL[σ₁₂] M₂) : g.comp (∑ i ∈ s, f i) = ∑ i ∈ s, g.comp (f i) := by
  ext
  simp

Composition Distributes over Finite Sum of Continuous Semilinear Maps

Informal description

Let $M_1$, $M_2$, and $M_3$ be topological modules over semirings $R_1$, $R_2$, and $R_3$ respectively, with ring homomorphisms $\sigma_{12}: R_1 \to R_2$ and $\sigma_{23}: R_2 \to R_3$. Assume $M_2$ and $M_3$ have continuous addition operations. For any finite set $\iota$, any subset $s \subseteq \iota$, any continuous semilinear map $g: M_2 \to_{SL[\sigma_{23}]} M_3$, and any family of continuous semilinear maps $f: \iota \to M_1 \to_{SL[\sigma_{12}]} M_2$, the composition of $g$ with the sum $\sum_{i \in s} f_i$ equals the sum of the compositions: \[ g \circ \left(\sum_{i \in s} f_i\right) = \sum_{i \in s} (g \circ f_i). \]

ContinuousLinearMap.finset_sum_comp theorem

 {ι : Type*} {s : Finset ι} [ContinuousAdd M₃] (g : ι → M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) :
  (∑ i ∈ s, g i).comp f = ∑ i ∈ s, (g i).comp f

Full source

theorem finset_sum_comp {ι : Type*} {s : Finset ι}
    [ContinuousAdd M₃] (g : ι → M₂ →SL[σ₂₃] M₃)
    (f : M₁ →SL[σ₁₂] M₂) : (∑ i ∈ s, g i).comp f = ∑ i ∈ s, (g i).comp f := by
  ext
  simp only [coe_comp', coe_sum', Function.comp_apply, Finset.sum_apply]

Distributivity of Composition over Finite Sums for Continuous Semilinear Maps

Informal description

Let $M_1$, $M_2$, and $M_3$ be topological modules over semirings $R_1$, $R_2$, and $R_3$ respectively, with ring homomorphisms $\sigma_{12} \colon R_1 \to R_2$ and $\sigma_{23} \colon R_2 \to R_3$. Assume $M_3$ has a continuous addition operation. For any finite set $\iota$, any family of continuous semilinear maps $g_i \colon M_2 \to_{SL[\sigma_{23}]} M_3$ indexed by $i \in \iota$, and any continuous semilinear map $f \colon M_1 \to_{SL[\sigma_{12}]} M_2$, the composition of the sum $\sum_{i \in \iota} g_i$ with $f$ equals the sum of the compositions $\sum_{i \in \iota} (g_i \circ f)$. That is, $$\left(\sum_{i \in \iota} g_i\right) \circ f = \sum_{i \in \iota} (g_i \circ f).$$

ContinuousLinearMap.comp_assoc theorem

 {R₄ : Type*} [Semiring R₄] [Module R₄ M₄] {σ₁₄ : R₁ →+* R₄} {σ₂₄ : R₂ →+* R₄} {σ₃₄ : R₃ →+* R₄}
  [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] (h : M₃ →SL[σ₃₄] M₄)
  (g : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) : (h.comp g).comp f = h.comp (g.comp f)

Full source

theorem comp_assoc {R₄ : Type*} [Semiring R₄] [Module R₄ M₄] {σ₁₄ : R₁ →+* R₄} {σ₂₄ : R₂ →+* R₄}
    {σ₃₄ : R₃ →+* R₄} [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄]
    [RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] (h : M₃ →SL[σ₃₄] M₄) (g : M₂ →SL[σ₂₃] M₃) (f : M₁ →SL[σ₁₂] M₂) :
    (h.comp g).comp f = h.comp (g.comp f) :=
  rfl

Associativity of Composition for Continuous Semilinear Maps

Informal description

Let $R_1, R_2, R_3, R_4$ be semirings and $M_1, M_2, M_3, M_4$ be topological modules over $R_1, R_2, R_3, R_4$ respectively, with continuous additive structures. Given ring homomorphisms $\sigma_{ij}: R_i \to R_j$ for $1 \leq i < j \leq 4$ satisfying the composition compatibility conditions $\sigma_{34} \circ \sigma_{13} = \sigma_{14}$, $\sigma_{34} \circ \sigma_{23} = \sigma_{24}$, and $\sigma_{24} \circ \sigma_{12} = \sigma_{14}$, and continuous semilinear maps $f: M_1 \to_{SL[\sigma_{12}]} M_2$, $g: M_2 \to_{SL[\sigma_{23}]} M_3$, and $h: M_3 \to_{SL[\sigma_{34}]} M_4$, the composition of continuous semilinear maps is associative: $(h \circ g) \circ f = h \circ (g \circ f)$.

ContinuousLinearMap.instMul instance

: Mul (M₁ →L[R₁] M₁)

Full source

instance instMul : Mul (M₁ →L[R₁] M₁) :=
  ⟨comp⟩

Multiplication Structure on Continuous Linear Endomorphisms

Informal description

The space of continuous linear maps from a topological module $M_1$ to itself over a semiring $R_1$ forms a multiplicative structure, where the multiplication operation is given by composition of maps.

ContinuousLinearMap.mul_def theorem

(f g : M₁ →L[R₁] M₁) : f * g = f.comp g

Full source

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

Product of Continuous Linear Endomorphisms is Composition

Informal description

For any two continuous linear endomorphisms $f$ and $g$ on a topological module $M_1$ over a semiring $R_1$, the product $f * g$ is equal to the composition $f \circ g$ of the two maps.

ContinuousLinearMap.coe_mul theorem

(f g : M₁ →L[R₁] M₁) : ⇑(f * g) = f ∘ g

Full source

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

Function Representation of Composition of Continuous Linear Endomorphisms

Informal description

For any two continuous linear endomorphisms $f$ and $g$ on a topological module $M_1$ over a semiring $R_1$, the underlying function of their composition $f * g$ is equal to the function composition $f \circ g$.

ContinuousLinearMap.mul_apply theorem

(f g : M₁ →L[R₁] M₁) (x : M₁) : (f * g) x = f (g x)

Full source

theorem mul_apply (f g : M₁ →L[R₁] M₁) (x : M₁) : (f * g) x = f (g x) :=
  rfl

Evaluation of Composition of Continuous Linear Maps: $ (f * g)(x) = f(g(x)) $

Informal description

For any continuous linear maps $ f, g $ from a topological module $ M_1 $ to itself over a semiring $ R_1 $, and for any element $ x \in M_1 $, the evaluation of the product $ f * g $ at $ x $ is equal to the composition $ f(g(x)) $.

ContinuousLinearMap.monoidWithZero instance

: MonoidWithZero (M₁ →L[R₁] M₁)

Full source

instance monoidWithZero : MonoidWithZero (M₁ →L[R₁] M₁) where
  mul_zero f := ext fun _ => map_zero f
  zero_mul _ := ext fun _ => rfl
  mul_one _ := ext fun _ => rfl
  one_mul _ := ext fun _ => rfl
  mul_assoc _ _ _ := ext fun _ => rfl

Monoid with Zero Structure on Continuous Linear Endomorphisms

Informal description

The space of continuous linear endomorphisms on a topological module $M_1$ over a semiring $R_1$ forms a monoid with zero, where the multiplication is given by composition of maps and the zero element is the zero map.

ContinuousLinearMap.coe_pow theorem

(f : M₁ →L[R₁] M₁) (n : ℕ) : ⇑(f ^ n) = f^[n]

Full source

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

Iteration-Power Correspondence for Continuous Linear Endomorphisms: $f^n = f^{[n]}$

Informal description

For any continuous linear endomorphism $f \colon M_1 \to M_1$ over a topological module $M_1$ with semiring $R_1$, and for any natural number $n$, the $n$-th power of $f$ as a continuous linear map is equal to the $n$-th iterate of $f$ as a function, i.e., $(f^n)(x) = f^{[n]}(x)$ for all $x \in M_1$.

ContinuousLinearMap.instNatCast instance

[ContinuousAdd M₁] : NatCast (M₁ →L[R₁] M₁)

Full source

instance instNatCast [ContinuousAdd M₁] : NatCast (M₁ →L[R₁] M₁) where
  natCast n := n • (1 : M₁ →L[R₁] M₁)

Natural Number Scalar Multiplication on Continuous Linear Maps

Informal description

For any topological module $M_1$ over a semiring $R_1$ with continuous addition, the space of continuous linear maps from $M_1$ to itself has a natural number scalar multiplication structure.

ContinuousLinearMap.semiring instance

[ContinuousAdd M₁] : Semiring (M₁ →L[R₁] M₁)

Full source

instance semiring [ContinuousAdd M₁] : Semiring (M₁ →L[R₁] M₁) where
  __ := ContinuousLinearMap.monoidWithZero
  __ := ContinuousLinearMap.addCommMonoid
  left_distrib f g h := ext fun x => map_add f (g x) (h x)
  right_distrib _ _ _ := ext fun _ => LinearMap.add_apply _ _ _
  toNatCast := instNatCast
  natCast_zero := zero_smul ℕ (1 : M₁ →L[R₁] M₁)
  natCast_succ n := AddMonoid.nsmul_succ n (1 : M₁ →L[R₁] M₁)

Semiring Structure on Continuous Linear Endomorphisms

Informal description

For any topological module $M_1$ over a semiring $R_1$ with continuous addition, the space of continuous linear endomorphisms $M_1 \toL[R_1] M_1$ forms a semiring under pointwise addition and composition of maps.

ContinuousLinearMap.toLinearMapRingHom definition

[ContinuousAdd M₁] : (M₁ →L[R₁] M₁) →+* M₁ →ₗ[R₁] M₁

Full source

/-- `ContinuousLinearMap.toLinearMap` as a `RingHom`. -/
@[simps]
def toLinearMapRingHom [ContinuousAdd M₁] : (M₁ →L[R₁] M₁) →+* M₁ →ₗ[R₁] M₁ where
  toFun := toLinearMap
  map_zero' := rfl
  map_one' := rfl
  map_add' _ _ := rfl
  map_mul' _ _ := rfl

Ring homomorphism from continuous linear endomorphisms to linear maps

Informal description

The function that maps a continuous linear endomorphism $f \colon M_1 \to_{L[R_1]} M_1$ to its underlying linear map $f \colon M_1 \to_{\ell[R_1]} M_1$ is a ring homomorphism. Here $M_1$ is a topological module over a semiring $R_1$ with continuous addition, and the ring structure on continuous linear endomorphisms is given by pointwise addition and composition of maps.

ContinuousLinearMap.natCast_apply theorem

[ContinuousAdd M₁] (n : ℕ) (m : M₁) : (↑n : M₁ →L[R₁] M₁) m = n • m

Full source

@[simp]
theorem natCast_apply [ContinuousAdd M₁] (n : ℕ) (m : M₁) : (↑n : M₁ →L[R₁] M₁) m = n • m :=
  rfl

Natural Number Scalar Application Identity for Continuous Linear Maps

Informal description

For any topological module $M_1$ over a semiring $R_1$ with continuous addition, the evaluation of the natural number scalar multiplication $n$ (viewed as a continuous linear map from $M_1$ to itself) at any element $m \in M_1$ equals the $n$-fold sum of $m$, i.e., $(n \cdot \text{id})(m) = n \cdot m$.

ContinuousLinearMap.ofNat_apply theorem

[ContinuousAdd M₁] (n : ℕ) [n.AtLeastTwo] (m : M₁) : (ofNat(n) : M₁ →L[R₁] M₁) m = OfNat.ofNat n • m

Full source

@[simp]
theorem ofNat_apply [ContinuousAdd M₁] (n : ℕ) [n.AtLeastTwo] (m : M₁) :
    (ofNat(n) : M₁ →L[R₁] M₁) m = OfNat.ofNat n • m :=
  rfl

Evaluation of Numeric Continuous Linear Map Equals Scalar Multiplication

Informal description

Let $M_1$ be a topological module over a semiring $R_1$ with continuous addition. For any natural number $n \geq 2$ and any element $m \in M_1$, the evaluation of the continuous linear map corresponding to $n$ (via the `OfNat` instance) at $m$ equals the scalar multiplication of $n$ on $m$, i.e., $$(\text{ofNat}(n) : M_1 \to_{L[R_1]} M_1)(m) = n \cdot m.$$

ContinuousLinearMap.applyModule instance

: Module (M₁ →L[R₁] M₁) M₁

Full source

/-- The tautological action by `M₁ →L[R₁] M₁` on `M`.

This generalizes `Function.End.applyMulAction`. -/
instance applyModule : Module (M₁ →L[R₁] M₁) M₁ :=
  Module.compHom _ toLinearMapRingHom

Module Structure on $M_1$ via Continuous Linear Endomorphisms

Informal description

For any topological module $M_1$ over a semiring $R_1$, the space of continuous linear endomorphisms $M_1 \to_{L[R_1]} M_1$ acts on $M_1$ by function application, making $M_1$ a module over this space of endomorphisms. Specifically, the scalar multiplication is defined by $(f \cdot a) = f(a)$ for any $f \in M_1 \to_{L[R_1]} M_1$ and $a \in M_1$.

ContinuousLinearMap.smul_def theorem

(f : M₁ →L[R₁] M₁) (a : M₁) : f • a = f a

Full source

@[simp]
protected theorem smul_def (f : M₁ →L[R₁] M₁) (a : M₁) : f • a = f a :=
  rfl

Scalar Multiplication Equals Evaluation for Continuous Linear Endomorphisms

Informal description

For any continuous linear endomorphism $f \colon M_1 \to_{L[R_1]} M_1$ and any element $a \in M_1$, the scalar multiplication of $f$ on $a$ is equal to the evaluation of $f$ at $a$, i.e., $f \cdot a = f(a)$.

ContinuousLinearMap.applyFaithfulSMul instance

: FaithfulSMul (M₁ →L[R₁] M₁) M₁

Full source

/-- `ContinuousLinearMap.applyModule` is faithful. -/
instance applyFaithfulSMul : FaithfulSMul (M₁ →L[R₁] M₁) M₁ :=
  ⟨fun {_ _} => ContinuousLinearMap.ext⟩

Faithfulness of the Action of Continuous Linear Endomorphisms

Informal description

The scalar multiplication action of continuous linear endomorphisms on a topological module $M_1$ over a semiring $R_1$ is faithful. That is, for any two continuous linear maps $f, g \colon M_1 \to_{L[R_1]} M_1$, if $f \cdot a = g \cdot a$ for all $a \in M_1$, then $f = g$.

ContinuousLinearMap.applySMulCommClass instance

: SMulCommClass R₁ (M₁ →L[R₁] M₁) M₁

Full source

instance applySMulCommClass : SMulCommClass R₁ (M₁ →L[R₁] M₁) M₁ where
  smul_comm r e m := (e.map_smul r m).symm

Commutation of Scalar Multiplication with Continuous Linear Endomorphisms

Informal description

For any topological module $M_1$ over a semiring $R_1$, the scalar multiplication actions of $R_1$ and the space of continuous linear endomorphisms $M_1 \to_{L[R_1]} M_1$ on $M_1$ commute. That is, for any $r \in R_1$, $f \in M_1 \to_{L[R_1]} M_1$, and $x \in M_1$, we have $r \cdot (f \cdot x) = f \cdot (r \cdot x)$.

ContinuousLinearMap.applySMulCommClass' instance

: SMulCommClass (M₁ →L[R₁] M₁) R₁ M₁

Full source

instance applySMulCommClass' : SMulCommClass (M₁ →L[R₁] M₁) R₁ M₁ where
  smul_comm := ContinuousLinearMap.map_smul

Commutation of Scalar Multiplication with Continuous Linear Endomorphisms

Informal description

For any topological module $M_1$ over a semiring $R_1$, the scalar multiplication actions of $R_1$ and the space of continuous linear endomorphisms $M_1 \to_{L[R_1]} M_1$ on $M_1$ commute. That is, for any $r \in R_1$, $f \in M_1 \to_{L[R_1]} M_1$, and $x \in M_1$, we have $r \cdot f(x) = f(r \cdot x)$.

ContinuousLinearMap.continuousConstSMul_apply instance

: ContinuousConstSMul (M₁ →L[R₁] M₁) M₁

Full source

instance continuousConstSMul_apply : ContinuousConstSMul (M₁ →L[R₁] M₁) M₁ :=
  ⟨ContinuousLinearMap.continuous⟩

Continuity of the Action of Continuous Linear Endomorphisms

Informal description

For any topological module $M_1$ over a semiring $R_1$, the action of continuous linear endomorphisms $M_1 \to_{L[R_1]} M_1$ on $M_1$ by function application is continuous in the second variable. That is, for each fixed $f \in M_1 \to_{L[R_1]} M_1$, the map $x \mapsto f(x)$ is continuous.

ContinuousLinearMap.isClosed_ker theorem

 [T1Space M₂] [FunLike F M₁ M₂] [ContinuousSemilinearMapClass F σ₁₂ M₁ M₂] (f : F) : IsClosed (ker f : Set M₁)

Full source

theorem isClosed_ker [T1Space M₂] [FunLike F M₁ M₂] [ContinuousSemilinearMapClass F σ₁₂ M₁ M₂]
    (f : F) :
    IsClosed (ker f : Set M₁) :=
  continuous_iff_isClosed.1 (map_continuous f) _ isClosed_singleton

Closedness of the Kernel of a Continuous Semilinear Map in a T₁ Space

Informal description

Let $M₁$ and $M₂$ be topological modules over semirings $R₁$ and $R₂$ respectively, with $M₂$ a T₁ space. Let $F$ be a type of continuous $\sigma$-semilinear maps from $M₁$ to $M₂$, where $\sigma \colon R₁ \to R₂$ is a ring homomorphism. Then for any $f \in F$, the kernel $\ker f$ is a closed subset of $M₁$.

ContinuousLinearMap.isComplete_ker theorem

 {M' : Type*} [UniformSpace M'] [CompleteSpace M'] [AddCommMonoid M'] [Module R₁ M'] [T1Space M₂] [FunLike F M' M₂]
  [ContinuousSemilinearMapClass F σ₁₂ M' M₂] (f : F) : IsComplete (ker f : Set M')

Full source

theorem isComplete_ker {M' : Type*} [UniformSpace M'] [CompleteSpace M'] [AddCommMonoid M']
    [Module R₁ M'] [T1Space M₂] [FunLike F M' M₂] [ContinuousSemilinearMapClass F σ₁₂ M' M₂]
    (f : F) :
    IsComplete (ker f : Set M') :=
  (isClosed_ker f).isComplete

Completeness of the Kernel of a Continuous Semilinear Map in a Complete Uniform Space

Informal description

Let $M'$ be a complete uniform space equipped with an additive commutative monoid structure and a module structure over a semiring $R₁$. Let $M₂$ be a T₁ space and $F$ be a type of continuous $\sigma$-semilinear maps from $M'$ to $M₂$, where $\sigma \colon R₁ \to R₂$ is a ring homomorphism. Then for any $f \in F$, the kernel $\ker f$ is a complete subset of $M'$.

ContinuousLinearMap.completeSpace_ker instance

 {M' : Type*} [UniformSpace M'] [CompleteSpace M'] [AddCommMonoid M'] [Module R₁ M'] [T1Space M₂] [FunLike F M' M₂]
  [ContinuousSemilinearMapClass F σ₁₂ M' M₂] (f : F) : CompleteSpace (ker f)

Full source

instance completeSpace_ker {M' : Type*} [UniformSpace M'] [CompleteSpace M']
    [AddCommMonoid M'] [Module R₁ M'] [T1Space M₂]
    [FunLike F M' M₂] [ContinuousSemilinearMapClass F σ₁₂ M' M₂]
    (f : F) : CompleteSpace (ker f) :=
  (isComplete_ker f).completeSpace_coe

Completeness of the Kernel of a Continuous Semilinear Map

Informal description

For any complete uniform space $M'$ equipped with an additive commutative monoid structure and a module structure over a semiring $R₁$, and any T₁ space $M₂$ with a type $F$ of continuous $\sigma$-semilinear maps from $M'$ to $M₂$ (where $\sigma \colon R₁ \to R₂$ is a ring homomorphism), the kernel $\ker f$ of any map $f \in F$ is a complete space.

ContinuousLinearMap.completeSpace_eqLocus instance

 {M' : Type*} [UniformSpace M'] [CompleteSpace M'] [AddCommMonoid M'] [Module R₁ M'] [T2Space M₂] [FunLike F M' M₂]
  [ContinuousSemilinearMapClass F σ₁₂ M' M₂] (f g : F) : CompleteSpace (LinearMap.eqLocus f g)

Full source

instance completeSpace_eqLocus {M' : Type*} [UniformSpace M'] [CompleteSpace M']
    [AddCommMonoid M'] [Module R₁ M'] [T2Space M₂]
    [FunLike F M' M₂] [ContinuousSemilinearMapClass F σ₁₂ M' M₂]
    (f g : F) : CompleteSpace (LinearMap.eqLocus f g) :=
  IsClosed.completeSpace_coe <| isClosed_eq (map_continuous f) (map_continuous g)

Completeness of the Equalizer Set for Continuous Semilinear Maps

Informal description

For any complete uniform space $M'$ equipped with an additive commutative monoid structure and a module structure over a semiring $R₁$, and any Hausdorff space $M₂$ with a type $F$ of continuous $\sigma$-semilinear maps from $M'$ to $M₂$ (where $\sigma \colon R₁ \to R₂$ is a ring homomorphism), the equalizer set $\{x \in M' \mid f(x) = g(x)\}$ of any two maps $f, g \in F$ is a complete space.

ContinuousLinearMap.codRestrict definition

(f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ x, f x ∈ p) : M₁ →SL[σ₁₂] p

Full source

/-- Restrict codomain of a continuous linear map. -/
def codRestrict (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ x, f x ∈ p) :
    M₁ →SL[σ₁₂] p where
  cont := f.continuous.subtype_mk _
  toLinearMap := (f : M₁ →ₛₗ[σ₁₂] M₂).codRestrict p h

Codomain restriction of a continuous semilinear map

Informal description

Given a continuous semilinear map $ f : M_1 \to_{SL[\sigma_{12}]} M_2 $ and a submodule $ p $ of $ M_2 $ such that $ f(x) \in p $ for all $ x \in M_1 $, the function restricts the codomain of $ f $ to $ p $, yielding a continuous semilinear map $ M_1 \to_{SL[\sigma_{12}]} p $.

ContinuousLinearMap.coe_codRestrict theorem

 (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ x, f x ∈ p) :
  (f.codRestrict p h : M₁ →ₛₗ[σ₁₂] p) = (f : M₁ →ₛₗ[σ₁₂] M₂).codRestrict p h

Full source

@[norm_cast]
theorem coe_codRestrict (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ x, f x ∈ p) :
    (f.codRestrict p h : M₁ →ₛₗ[σ₁₂] p) = (f : M₁ →ₛₗ[σ₁₂] M₂).codRestrict p h :=
  rfl

Semilinear equality for codomain restriction of continuous semilinear maps

Informal description

Let $M_1$ and $M_2$ be topological modules over semirings $R_1$ and $R_2$ respectively, with a ring homomorphism $\sigma_{12} : R_1 \to R_2$. Given a continuous semilinear map $f : M_1 \to_{SL[\sigma_{12}]} M_2$, a submodule $p$ of $M_2$ such that $f(x) \in p$ for all $x \in M_1$, the codomain-restricted map $f.\text{codRestrict}\, p\, h$ (as a semilinear map) equals the semilinear codomain restriction of $f$ to $p$.

ContinuousLinearMap.coe_codRestrict_apply theorem

 (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ x, f x ∈ p) (x) : (f.codRestrict p h x : M₂) = f x

Full source

@[simp]
theorem coe_codRestrict_apply (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ x, f x ∈ p) (x) :
    (f.codRestrict p h x : M₂) = f x :=
  rfl

Codomain restriction preserves evaluation: $(f|_{p})(x) = f(x)$

Informal description

Let $f : M_1 \to_{SL[\sigma_{12}]} M_2$ be a continuous semilinear map between topological modules, and let $p$ be a submodule of $M_2$ such that $f(x) \in p$ for all $x \in M_1$. Then for any $x \in M_1$, the value of the codomain-restricted map $f.\text{codRestrict}\, p\, h$ at $x$, when viewed as an element of $M_2$, equals $f(x)$. In other words, the following equality holds in $M_2$: $$(f.\text{codRestrict}\, p\, h)(x) = f(x).$$

ContinuousLinearMap.ker_codRestrict theorem

(f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ x, f x ∈ p) : ker (f.codRestrict p h) = ker f

Full source

@[simp]
theorem ker_codRestrict (f : M₁ →SL[σ₁₂] M₂) (p : Submodule R₂ M₂) (h : ∀ x, f x ∈ p) :
    ker (f.codRestrict p h) = ker f :=
  (f : M₁ →ₛₗ[σ₁₂] M₂).ker_codRestrict p h

Kernel Preservation under Codomain Restriction of Continuous Semilinear Maps

Informal description

Let $f \colon M_1 \to_{SL[\sigma_{12}]} M_2$ be a continuous semilinear map between topological modules, and let $p$ be a submodule of $M_2$ such that $f(x) \in p$ for all $x \in M_1$. Then the kernel of the codomain-restricted map $f \colon M_1 \to_{SL[\sigma_{12}]} p$ is equal to the kernel of the original map $f$.

ContinuousLinearMap.rangeRestrict abbrev

[RingHomSurjective σ₁₂] (f : M₁ →SL[σ₁₂] M₂)

Full source

/-- Restrict the codomain of a continuous linear map `f` to `f.range`. -/
abbrev rangeRestrict [RingHomSurjective σ₁₂] (f : M₁ →SL[σ₁₂] M₂) :=
  f.codRestrict (LinearMap.range f) (LinearMap.mem_range_self f)

Range restriction of a continuous semilinear map

Informal description

Given a continuous semilinear map $f \colon M_1 \to_{SL[\sigma_{12}]} M_2$ where $\sigma_{12} \colon R_1 \to R_2$ is a ring homomorphism, and assuming $\sigma_{12}$ is surjective, the map $f.\text{rangeRestrict}$ restricts the codomain of $f$ to its range $\text{range}(f) \subseteq M_2$, yielding a continuous semilinear map $M_1 \to_{SL[\sigma_{12}]} \text{range}(f)$.

ContinuousLinearMap.coe_rangeRestrict theorem

 [RingHomSurjective σ₁₂] (f : M₁ →SL[σ₁₂] M₂) :
  (f.rangeRestrict : M₁ →ₛₗ[σ₁₂] LinearMap.range f) = (f : M₁ →ₛₗ[σ₁₂] M₂).rangeRestrict

Full source

@[simp]
theorem coe_rangeRestrict [RingHomSurjective σ₁₂] (f : M₁ →SL[σ₁₂] M₂) :
    (f.rangeRestrict : M₁ →ₛₗ[σ₁₂] LinearMap.range f) = (f : M₁ →ₛₗ[σ₁₂] M₂).rangeRestrict :=
  rfl

Equality of Underlying Semilinear Maps for Range-Restricted Continuous Semilinear Maps

Informal description

Let $R_1$ and $R_2$ be semirings with a ring homomorphism $\sigma_{12} \colon R_1 \to R_2$, and let $M_1$ and $M_2$ be topological modules over $R_1$ and $R_2$ respectively. Given a continuous semilinear map $f \colon M_1 \to_{SL[\sigma_{12}]} M_2$ where $\sigma_{12}$ is surjective, the underlying semilinear map of the range-restricted continuous semilinear map $f.\text{rangeRestrict} \colon M_1 \to_{SL[\sigma_{12}]} \text{range}(f)$ is equal to the range restriction of the underlying semilinear map of $f$.

Submodule.subtypeL definition

(p : Submodule R₁ M₁) : p →L[R₁] M₁

Full source

/-- `Submodule.subtype` as a `ContinuousLinearMap`. -/
def _root_.Submodule.subtypeL (p : Submodule R₁ M₁) : p →L[R₁] M₁ where
  cont := continuous_subtype_val
  toLinearMap := p.subtype

Continuous inclusion of a submodule

Informal description

For a submodule $p$ of a topological module $M₁$ over a semiring $R₁$, the inclusion map $p \hookrightarrow M₁$ is a continuous linear map, where the linear structure is inherited from $M₁$ and the continuity follows from the subspace topology on $p$.

Submodule.coe_subtypeL theorem

(p : Submodule R₁ M₁) : (p.subtypeL : p →ₗ[R₁] M₁) = p.subtype

Full source

@[simp, norm_cast]
theorem _root_.Submodule.coe_subtypeL (p : Submodule R₁ M₁) :
    (p.subtypeL : p →ₗ[R₁] M₁) = p.subtype :=
  rfl

Underlying Linear Map of Continuous Inclusion Equals Canonical Inclusion

Informal description

For any submodule $p$ of a topological module $M₁$ over a semiring $R₁$, the underlying linear map of the continuous inclusion map $p \hookrightarrow M₁$ is equal to the canonical linear inclusion map of $p$ into $M₁$.

Submodule.coe_subtypeL' theorem

(p : Submodule R₁ M₁) : ⇑p.subtypeL = p.subtype

Full source

@[simp]
theorem _root_.Submodule.coe_subtypeL' (p : Submodule R₁ M₁) : ⇑p.subtypeL = p.subtype :=
  rfl

Inclusion Map of Submodule as Continuous Linear Map

Informal description

For any submodule $p$ of a topological module $M₁$ over a semiring $R₁$, the underlying function of the continuous linear inclusion map $p \toL[R₁] M₁$ is equal to the canonical inclusion map $p \hookrightarrow M₁$.

Submodule.subtypeL_apply theorem

(p : Submodule R₁ M₁) (x : p) : p.subtypeL x = x

Full source

@[simp]
theorem _root_.Submodule.subtypeL_apply (p : Submodule R₁ M₁) (x : p) : p.subtypeL x = x :=
  rfl

Inclusion of Submodule Acts as Identity

Informal description

For any submodule $p$ of a topological module $M₁$ over a semiring $R₁$, the continuous linear inclusion map $\text{subtypeL}_p : p \to M₁$ satisfies $\text{subtypeL}_p(x) = x$ for all $x \in p$.

Submodule.range_subtypeL theorem

(p : Submodule R₁ M₁) : range p.subtypeL = p

Full source

@[simp]
theorem _root_.Submodule.range_subtypeL (p : Submodule R₁ M₁) : range p.subtypeL = p :=
  Submodule.range_subtype _

Range of Continuous Submodule Inclusion Equals Submodule

Informal description

For a submodule $p$ of a topological module $M₁$ over a semiring $R₁$, the range of the continuous linear inclusion map $p \hookrightarrow M₁$ is equal to $p$ itself.

Submodule.ker_subtypeL theorem

(p : Submodule R₁ M₁) : ker p.subtypeL = ⊥

Full source

@[simp]
theorem _root_.Submodule.ker_subtypeL (p : Submodule R₁ M₁) : ker p.subtypeL = ⊥ :=
  Submodule.ker_subtype _

Trivial Kernel of Submodule Inclusion Map

Informal description

For any submodule $p$ of a topological module $M₁$ over a semiring $R₁$, the kernel of the continuous linear inclusion map $p \hookrightarrow M₁$ is the trivial submodule $\{0\}$.

ContinuousLinearMap.smulRight definition

(c : M₁ →L[R] S) (f : M₂) : M₁ →L[R] M₂

Full source

/-- The linear map `fun x => c x • f`.  Associates to a scalar-valued linear map and an element of
`M₂` the `M₂`-valued linear map obtained by multiplying the two (a.k.a. tensoring by `M₂`).
See also `ContinuousLinearMap.smulRightₗ` and `ContinuousLinearMap.smulRightL`. -/
def smulRight (c : M₁ →L[R] S) (f : M₂) : M₁ →L[R] M₂ :=
  { c.toLinearMap.smulRight f with cont := c.2.smul continuous_const }

Continuous linear map obtained by scalar multiplication with a fixed element

Informal description

Given a continuous linear map $ c : M_1 \to_L[R] S $ and an element $ f \in M_2 $, the function `ContinuousLinearMap.smulRight` constructs a new continuous linear map from $ M_1 $ to $ M_2 $ defined by $ x \mapsto c(x) \cdot f $. This operation combines a scalar-valued linear map with a fixed element of $ M_2 $ to produce a vector-valued linear map via scalar multiplication.

ContinuousLinearMap.smulRight_apply theorem

{c : M₁ →L[R] S} {f : M₂} {x : M₁} : (smulRight c f : M₁ → M₂) x = c x • f

Full source

@[simp]
theorem smulRight_apply {c : M₁ →L[R] S} {f : M₂} {x : M₁} :
    (smulRight c f : M₁ → M₂) x = c x • f :=
  rfl

Evaluation of Continuous Linear Map Constructed via Scalar Multiplication

Informal description

Let $R$ be a semiring, $M_1$ and $M_2$ be topological modules over $R$, and $S$ be another semiring such that $M_2$ is also a module over $S$. Given a continuous linear map $c : M_1 \to_L[R] S$ and an element $f \in M_2$, the evaluation of the continuous linear map $\text{smulRight}(c, f)$ at a point $x \in M_1$ is given by the scalar multiplication of $c(x)$ with $f$, i.e., \[ \text{smulRight}(c, f)(x) = c(x) \cdot f. \]

ContinuousLinearMap.smulRight_one_one theorem

(c : R₁ →L[R₁] M₂) : smulRight (1 : R₁ →L[R₁] R₁) (c 1) = c

Full source

@[simp]
theorem smulRight_one_one (c : R₁ →L[R₁] M₂) : smulRight (1 : R₁ →L[R₁] R₁) (c 1) = c := by
  ext
  simp [← ContinuousLinearMap.map_smul_of_tower]

Identity of Scalar-Right-Multiplied Maps via Evaluation at One

Informal description

Let $R_1$ be a topological semiring and $M_2$ be a topological module over $R_1$. For any continuous $R_1$-linear map $c \colon R_1 \to_{L[R_1]} M_2$, the continuous linear map obtained by scalar multiplication of the identity map $1_{R_1}$ with $c(1)$ equals $c$ itself, i.e., \[ \text{smulRight}(1_{R_1}, c(1)) = c. \]

ContinuousLinearMap.smulRight_one_eq_iff theorem

{f f' : M₂} : smulRight (1 : R₁ →L[R₁] R₁) f = smulRight (1 : R₁ →L[R₁] R₁) f' ↔ f = f'

Full source

@[simp]
theorem smulRight_one_eq_iff {f f' : M₂} :
    smulRightsmulRight (1 : R₁ →L[R₁] R₁) f = smulRight (1 : R₁ →L[R₁] R₁) f' ↔ f = f' := by
  simp only [ContinuousLinearMap.ext_ring_iff, smulRight_apply, one_apply, one_smul]

Equality of scalar-right-multiplied maps by identity is equivalent to equality of elements

Informal description

For any elements $f, f'$ in a topological module $M_2$ over a topological semiring $R_1$, the equality of the continuous linear maps $\text{smulRight}(1_{R_1}, f) = \text{smulRight}(1_{R_1}, f')$ holds if and only if $f = f'$, where $1_{R_1}$ denotes the identity continuous linear map on $R_1$.

ContinuousLinearMap.smulRight_comp theorem

 [ContinuousMul R₁] {x : M₂} {c : R₁} :
  (smulRight (1 : R₁ →L[R₁] R₁) x).comp (smulRight (1 : R₁ →L[R₁] R₁) c) = smulRight (1 : R₁ →L[R₁] R₁) (c • x)

Full source

theorem smulRight_comp [ContinuousMul R₁] {x : M₂} {c : R₁} :
    (smulRight (1 : R₁ →L[R₁] R₁) x).comp (smulRight (1 : R₁ →L[R₁] R₁) c) =
      smulRight (1 : R₁ →L[R₁] R₁) (c • x) := by
  ext
  simp [mul_smul]

Composition of Scalar-Right-Multiplied Maps by Identity Equals Scalar-Right-Multiplied Map of Scalar Multiple

Informal description

Let $R_1$ be a topological semiring with continuous multiplication, and let $M_2$ be a topological module over $R_1$. For any element $x \in M_2$ and any scalar $c \in R_1$, the composition of the continuous linear maps $\text{smulRight}(1_{R_1}, x)$ and $\text{smulRight}(1_{R_1}, c)$ is equal to $\text{smulRight}(1_{R_1}, c \cdot x)$, where $1_{R_1}$ denotes the identity continuous linear map on $R_1$.

ContinuousLinearMap.toSpanSingleton definition

(x : M₁) : R₁ →L[R₁] M₁

Full source

/-- Given an element `x` of a topological space `M` over a semiring `R`, the natural continuous
linear map from `R` to `M` by taking multiples of `x`. -/
def toSpanSingleton (x : M₁) : R₁ →L[R₁] M₁ where
  toLinearMap := LinearMap.toSpanSingleton R₁ M₁ x
  cont := continuous_id.smul continuous_const

Continuous linear map to span of a singleton

Informal description

For an element $x$ in a topological module $M$ over a topological semiring $R$, the continuous linear map $\text{toSpanSingleton}_R^M x$ from $R$ to $M$ sends each scalar $r \in R$ to its scalar multiple $r \cdot x$ in $M$. This map is continuous by the continuity of scalar multiplication.

ContinuousLinearMap.toSpanSingleton_apply theorem

(x : M₁) (r : R₁) : toSpanSingleton R₁ x r = r • x

Full source

theorem toSpanSingleton_apply (x : M₁) (r : R₁) : toSpanSingleton R₁ x r = r • x :=
  rfl

Evaluation of Continuous Linear Map to Span of Singleton

Informal description

For any element $x$ in a topological module $M_1$ over a topological semiring $R_1$, and for any scalar $r \in R_1$, the continuous linear map $\text{toSpanSingleton}_{R_1} x$ evaluated at $r$ equals the scalar multiple $r \cdot x$.

ContinuousLinearMap.toSpanSingleton_add theorem

[ContinuousAdd M₁] (x y : M₁) : toSpanSingleton R₁ (x + y) = toSpanSingleton R₁ x + toSpanSingleton R₁ y

Full source

theorem toSpanSingleton_add [ContinuousAdd M₁] (x y : M₁) :
    toSpanSingleton R₁ (x + y) = toSpanSingleton R₁ x + toSpanSingleton R₁ y := by
  ext1; simp [toSpanSingleton_apply]

Additivity of Continuous Linear Map to Span of Sum

Informal description

Let $M_1$ be a topological module over a topological semiring $R_1$ with continuous addition. For any two elements $x, y \in M_1$, the continuous linear map to the span of the singleton $\{x + y\}$ is equal to the sum of the continuous linear maps to the spans of $\{x\}$ and $\{y\}$. That is, \[ \text{toSpanSingleton}_{R_1}(x + y) = \text{toSpanSingleton}_{R_1}(x) + \text{toSpanSingleton}_{R_1}(y). \]

ContinuousLinearMap.toSpanSingleton_smul' theorem

 {α} [Monoid α] [DistribMulAction α M₁] [ContinuousConstSMul α M₁] [SMulCommClass R₁ α M₁] (c : α) (x : M₁) :
  toSpanSingleton R₁ (c • x) = c • toSpanSingleton R₁ x

Full source

theorem toSpanSingleton_smul' {α} [Monoid α] [DistribMulAction α M₁] [ContinuousConstSMul α M₁]
    [SMulCommClass R₁ α M₁] (c : α) (x : M₁) :
    toSpanSingleton R₁ (c • x) = c • toSpanSingleton R₁ x := by
  ext1; rw [toSpanSingleton_apply, smul_apply, toSpanSingleton_apply, smul_comm]

Scalar Multiplication Commutes with Singleton Span Map: $\text{toSpanSingleton}_R(c \cdot x) = c \cdot \text{toSpanSingleton}_R(x)$

Informal description

Let $\alpha$ be a monoid acting distributively on a topological module $M_1$ over a topological semiring $R_1$, with continuous scalar multiplication by $\alpha$ on $M_1$ and commuting scalar actions of $R_1$ and $\alpha$ on $M_1$. Then for any $c \in \alpha$ and $x \in M_1$, the continuous linear map $\text{toSpanSingleton}_{R_1}(c \cdot x)$ equals the scalar multiple $c \cdot \text{toSpanSingleton}_{R_1}(x)$.

ContinuousLinearMap.toSpanSingleton_smul theorem

 (R) {M₁} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [TopologicalSpace R] [TopologicalSpace M₁]
  [ContinuousSMul R M₁] (c : R) (x : M₁) : toSpanSingleton R (c • x) = c • toSpanSingleton R x

Full source

/-- A special case of `to_span_singleton_smul'` for when `R` is commutative. -/
theorem toSpanSingleton_smul (R) {M₁} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁]
    [TopologicalSpace R] [TopologicalSpace M₁] [ContinuousSMul R M₁] (c : R) (x : M₁) :
    toSpanSingleton R (c • x) = c • toSpanSingleton R x :=
  toSpanSingleton_smul' R c x

Scalar Multiplication Commutes with Singleton Span Map in Commutative Case: $\text{toSpanSingleton}_R(c \cdot x) = c \cdot \text{toSpanSingleton}_R(x)$

Informal description

Let $R$ be a commutative semiring and $M_1$ be an additive commutative monoid with a module structure over $R$, both equipped with topological spaces such that the scalar multiplication $R \times M_1 \to M_1$ is continuous. Then for any $c \in R$ and $x \in M_1$, the continuous linear map $\text{toSpanSingleton}_R(c \cdot x)$ equals the scalar multiple $c \cdot \text{toSpanSingleton}_R(x)$.

ContinuousLinearMap.map_neg theorem

(f : M →SL[σ₁₂] M₂) (x : M) : f (-x) = -f x

Full source

protected theorem map_neg (f : M →SL[σ₁₂] M₂) (x : M) : f (-x) = -f x := by
  exact map_neg f x

Continuous Semilinear Maps Preserve Negation: $f(-x) = -f(x)$

Informal description

For any continuous semilinear map $f \colon M \to_{SL[\sigma_{12}]} M_2$ and any element $x \in M$, the image of $-x$ under $f$ is equal to the negation of the image of $x$, i.e., $f(-x) = -f(x)$.

ContinuousLinearMap.map_sub theorem

(f : M →SL[σ₁₂] M₂) (x y : M) : f (x - y) = f x - f y

Full source

protected theorem map_sub (f : M →SL[σ₁₂] M₂) (x y : M) : f (x - y) = f x - f y := by
  exact map_sub f x y

Continuous Semilinear Maps Preserve Subtraction: $f(x - y) = f(x) - f(y)$

Informal description

For any continuous semilinear map $f \colon M \to_{SL[\sigma_{12}]} M_2$ and any elements $x, y \in M$, the image of $x - y$ under $f$ is equal to the difference of the images, i.e., $f(x - y) = f(x) - f(y)$.

ContinuousLinearMap.sub_apply' theorem

(f g : M →SL[σ₁₂] M₂) (x : M) : ((f : M →ₛₗ[σ₁₂] M₂) - g) x = f x - g x

Full source

@[simp]
theorem sub_apply' (f g : M →SL[σ₁₂] M₂) (x : M) : ((f : M →ₛₗ[σ₁₂] M₂) - g) x = f x - g x :=
  rfl

Evaluation of Difference of Continuous Semilinear Maps

Informal description

For any two continuous semilinear maps $f, g \colon M \to_{SL[\sigma_{12}]} M_2$ and any element $x \in M$, the evaluation of the difference of $f$ and $g$ at $x$ is equal to the difference of the evaluations, i.e., $(f - g)(x) = f(x) - g(x)$.

ContinuousLinearMap.neg instance

: Neg (M →SL[σ₁₂] M₂)

Full source

instance neg : Neg (M →SL[σ₁₂] M₂) :=
  ⟨fun f => ⟨-f, f.2.neg⟩⟩

Additive Group Structure on Continuous Semilinear Maps

Informal description

The set of continuous semilinear maps between topological modules $M$ and $M₂$ over semirings $R$ and $S$ (with respect to a ring homomorphism $\sigma: R \to S$) forms an additive group under pointwise negation.

ContinuousLinearMap.neg_apply theorem

(f : M →SL[σ₁₂] M₂) (x : M) : (-f) x = -f x

Full source

@[simp]
theorem neg_apply (f : M →SL[σ₁₂] M₂) (x : M) : (-f) x = -f x :=
  rfl

Negation of Continuous Semilinear Map Evaluates to Negation of Evaluation

Informal description

For any continuous semilinear map $f \colon M \to_{SL[\sigma_{12}]} M_2$ and any element $x \in M$, the evaluation of the negation of $f$ at $x$ is equal to the negation of the evaluation of $f$ at $x$, i.e., $(-f)(x) = -f(x)$.

ContinuousLinearMap.coe_neg theorem

(f : M →SL[σ₁₂] M₂) : (↑(-f) : M →ₛₗ[σ₁₂] M₂) = -f

Full source

@[simp, norm_cast]
theorem coe_neg (f : M →SL[σ₁₂] M₂) : (↑(-f) : M →ₛₗ[σ₁₂] M₂) = -f :=
  rfl

Negation commutes with coercion of continuous semilinear maps

Informal description

For any continuous semilinear map $f \colon M \to_{SL[\sigma_{12}]} M₂$, the underlying semilinear map of the negation $-f$ is equal to the negation of the underlying semilinear map of $f$. In other words, the coercion of $-f$ to a semilinear map is $-(\text{coercion of } f)$.

ContinuousLinearMap.coe_neg' theorem

(f : M →SL[σ₁₂] M₂) : ⇑(-f) = -f

Full source

@[norm_cast]
theorem coe_neg' (f : M →SL[σ₁₂] M₂) : ⇑(-f) = -f :=
  rfl

Negation of Continuous Semilinear Maps is Pointwise Negation

Informal description

For any continuous semilinear map $f \colon M \to_{SL[\sigma_{12}]} M₂$, the underlying function of the negation $-f$ is equal to the pointwise negation of $f$, i.e., $(-f)(x) = -f(x)$ for all $x \in M$.

ContinuousLinearMap.toContinuousAddMonoidHom_neg theorem

(f : M →SL[σ₁₂] M₂) : ↑(-f) = -(f : ContinuousAddMonoidHom M M₂)

Full source

@[simp, norm_cast]
theorem toContinuousAddMonoidHom_neg (f : M →SL[σ₁₂] M₂) :
    ↑(-f) = -(f : ContinuousAddMonoidHom M M₂) := rfl

Negation Commutes with Coercion to Continuous Additive Monoid Homomorphism

Informal description

For any continuous semilinear map $f \colon M \to_{SL[\sigma_{12}]} M₂$ between topological modules, the coercion of the negation $-f$ to a continuous additive monoid homomorphism equals the negation of the coercion of $f$ to a continuous additive monoid homomorphism, i.e., $\uparrow(-f) = -(\uparrow f)$.

ContinuousLinearMap.sub instance

: Sub (M →SL[σ₁₂] M₂)

Full source

instance sub : Sub (M →SL[σ₁₂] M₂) :=
  ⟨fun f g => ⟨f - g, f.2.sub g.2⟩⟩

Subtraction on Continuous Semilinear Maps

Informal description

The space of continuous semilinear maps $M \to_{SL[\sigma_{12}]} M₂$ between topological modules is equipped with a subtraction operation.

ContinuousLinearMap.addCommGroup instance

: AddCommGroup (M →SL[σ₁₂] M₂)

Full source

instance addCommGroup : AddCommGroup (M →SL[σ₁₂] M₂) where
  __ := ContinuousLinearMap.addCommMonoid
  neg := (-·)
  sub := (· - ·)
  sub_eq_add_neg _ _ := by ext; apply sub_eq_add_neg
  nsmul := (· • ·)
  zsmul := (· • ·)
  zsmul_zero' f := by ext; simp
  zsmul_succ' n f := by ext; simp [add_smul, add_comm]
  zsmul_neg' n f := by ext; simp [add_smul]
  neg_add_cancel _ := by ext; apply neg_add_cancel

Additive Commutative Group Structure on Continuous Semilinear Maps

Informal description

The space of continuous semilinear maps $M \toSL[\sigma_{12}] M₂$ between topological modules forms an additive commutative group under pointwise addition and negation.

ContinuousLinearMap.sub_apply theorem

(f g : M →SL[σ₁₂] M₂) (x : M) : (f - g) x = f x - g x

Full source

theorem sub_apply (f g : M →SL[σ₁₂] M₂) (x : M) : (f - g) x = f x - g x :=
  rfl

Evaluation of Difference of Continuous Semilinear Maps

Informal description

For any two continuous semilinear maps $ f, g : M \to_{SL[\sigma_{12}]} M₂ $ and any element $ x \in M $, the evaluation of their difference at $ x $ satisfies $(f - g)(x) = f(x) - g(x)$.

ContinuousLinearMap.coe_sub theorem

(f g : M →SL[σ₁₂] M₂) : (↑(f - g) : M →ₛₗ[σ₁₂] M₂) = f - g

Full source

@[simp, norm_cast]
theorem coe_sub (f g : M →SL[σ₁₂] M₂) : (↑(f - g) : M →ₛₗ[σ₁₂] M₂) = f - g :=
  rfl

Difference of Continuous Semilinear Maps Preserves Underlying Map Structure

Informal description

Let $M$ and $M₂$ be topological modules over semirings $R$ and $S$ respectively, with a ring homomorphism $\sigma_{12}: R \to S$. For any two continuous semilinear maps $f, g: M \to_{SL[\sigma_{12}]} M₂$, the underlying semilinear map of their difference $f - g$ equals the difference of the underlying semilinear maps, i.e., $(f - g) = f - g$ as maps in $M →ₛₗ[\sigma_{12}] M₂$.

ContinuousLinearMap.coe_sub' theorem

(f g : M →SL[σ₁₂] M₂) : ⇑(f - g) = f - g

Full source

@[simp, norm_cast]
theorem coe_sub' (f g : M →SL[σ₁₂] M₂) : ⇑(f - g) = f - g :=
  rfl

Pointwise Difference of Continuous Semilinear Maps

Informal description

For any two continuous semilinear maps $ f, g : M \to_{SL[\sigma_{12}]} M₂ $, the underlying function of their difference $ f - g $ is equal to the pointwise difference of the underlying functions of $ f $ and $ g $, i.e., $ (f - g)(x) = f(x) - g(x) $ for all $ x \in M $.

ContinuousLinearMap.toContinuousAddMonoidHom_sub theorem

(f g : M →SL[σ₁₂] M₂) : ↑(f - g) = (f - g : ContinuousAddMonoidHom M M₂)

Full source

@[simp, norm_cast]
theorem toContinuousAddMonoidHom_sub (f g : M →SL[σ₁₂] M₂) :
    ↑(f - g) = (f - g : ContinuousAddMonoidHom M M₂) := rfl

Difference of Continuous Semilinear Maps as Additive Monoid Homomorphisms

Informal description

Let $M$ and $M₂$ be topological modules over semirings $R$ and $S$ respectively, with a ring homomorphism $\sigma_{12}: R \to S$. For any two continuous $\sigma_{12}$-semilinear maps $f, g: M \to M₂$, the underlying continuous additive monoid homomorphism of their difference $f - g$ equals the difference of their underlying continuous additive monoid homomorphisms.

ContinuousLinearMap.comp_neg theorem

 [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [IsTopologicalAddGroup M₂] [IsTopologicalAddGroup M₃] (g : M₂ →SL[σ₂₃] M₃)
  (f : M →SL[σ₁₂] M₂) : g.comp (-f) = -g.comp f

Full source

@[simp]
theorem comp_neg [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [IsTopologicalAddGroup M₂]
    [IsTopologicalAddGroup M₃] (g : M₂ →SL[σ₂₃] M₃) (f : M →SL[σ₁₂] M₂) :
    g.comp (-f) = -g.comp f := by
  ext x
  simp

Composition with Negation of Continuous Semilinear Maps: $g \circ (-f) = -(g \circ f)$

Informal description

Let $M$, $M_2$, and $M_3$ be topological modules over semirings $R$, $S$, and $T$ respectively, with ring homomorphisms $\sigma_{12} \colon R \to S$ and $\sigma_{23} \colon S \to T$ forming a composition triple $\sigma_{13} = \sigma_{23} \circ \sigma_{12}$. Assume $M_2$ and $M_3$ are topological additive groups. For any continuous semilinear maps $g \colon M_2 \to_{SL[\sigma_{23}]} M_3$ and $f \colon M \to_{SL[\sigma_{12}]} M_2$, the composition of $g$ with the negation $-f$ equals the negation of the composition $g \circ f$, i.e., $g \circ (-f) = -(g \circ f)$.

ContinuousLinearMap.neg_comp theorem

 [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [IsTopologicalAddGroup M₃] (g : M₂ →SL[σ₂₃] M₃) (f : M →SL[σ₁₂] M₂) :
  (-g).comp f = -g.comp f

Full source

@[simp]
theorem neg_comp [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [IsTopologicalAddGroup M₃] (g : M₂ →SL[σ₂₃] M₃)
    (f : M →SL[σ₁₂] M₂) : (-g).comp f = -g.comp f := by
  ext
  simp

Negation and Composition of Continuous Semilinear Maps

Informal description

Let $M$, $M_2$, and $M_3$ be topological modules over semirings $R$, $S$, and $T$ respectively, with ring homomorphisms $\sigma_{12} \colon R \to S$ and $\sigma_{23} \colon S \to T$ forming a composition triple $\sigma_{13} = \sigma_{23} \circ \sigma_{12}$. Assume $M_3$ is a topological additive group. For any continuous semilinear maps $g \colon M_2 \to_{SL[\sigma_{23}]} M_3$ and $f \colon M \to_{SL[\sigma_{12}]} M_2$, the composition of the negation $-g$ with $f$ equals the negation of the composition $g \circ f$, i.e., $(-g) \circ f = -(g \circ f)$.

ContinuousLinearMap.comp_sub theorem

 [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [IsTopologicalAddGroup M₂] [IsTopologicalAddGroup M₃] (g : M₂ →SL[σ₂₃] M₃)
  (f₁ f₂ : M →SL[σ₁₂] M₂) : g.comp (f₁ - f₂) = g.comp f₁ - g.comp f₂

Full source

@[simp]
theorem comp_sub [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [IsTopologicalAddGroup M₂]
    [IsTopologicalAddGroup M₃] (g : M₂ →SL[σ₂₃] M₃) (f₁ f₂ : M →SL[σ₁₂] M₂) :
    g.comp (f₁ - f₂) = g.comp f₁ - g.comp f₂ := by
  ext
  simp

Composition Distributes Over Difference for Continuous Semilinear Maps: $g \circ (f_1 - f_2) = g \circ f_1 - g \circ f_2$

Informal description

Let $M$, $M_2$, and $M_3$ be topological modules over semirings $R$, $S$, and $T$ respectively, with ring homomorphisms $\sigma_{12} \colon R \to S$ and $\sigma_{23} \colon S \to T$ forming a composition triple $\sigma_{13} = \sigma_{23} \circ \sigma_{12}$. Assume $M_2$ and $M_3$ are topological additive groups. For any continuous semilinear map $g \colon M_2 \to_{SL[\sigma_{23}]} M_3$ and any two continuous semilinear maps $f_1, f_2 \colon M \to_{SL[\sigma_{12}]} M_2$, the composition of $g$ with the difference $f_1 - f_2$ equals the difference of the compositions $g \circ f_1$ and $g \circ f_2$, i.e., $$ g \circ (f_1 - f_2) = g \circ f_1 - g \circ f_2. $$

ContinuousLinearMap.sub_comp theorem

 [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [IsTopologicalAddGroup M₃] (g₁ g₂ : M₂ →SL[σ₂₃] M₃) (f : M →SL[σ₁₂] M₂) :
  (g₁ - g₂).comp f = g₁.comp f - g₂.comp f

Full source

@[simp]
theorem sub_comp [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [IsTopologicalAddGroup M₃] (g₁ g₂ : M₂ →SL[σ₂₃] M₃)
    (f : M →SL[σ₁₂] M₂) : (g₁ - g₂).comp f = g₁.comp f - g₂.comp f := by
  ext
  simp

Difference of Continuous Semilinear Maps Distributes Over Composition

Informal description

Let $M$, $M_2$, and $M_3$ be topological modules over semirings $R$, $S$, and $T$ respectively, with ring homomorphisms $\sigma_{12}: R \to S$ and $\sigma_{23}: S \to T$ forming a composition triple $\sigma_{13} = \sigma_{23} \circ \sigma_{12}$. Suppose $M_3$ is a topological additive group. Then for any continuous semilinear maps $g_1, g_2: M_2 \to_{SL[\sigma_{23}]} M_3$ and $f: M \to_{SL[\sigma_{12}]} M_2$, the composition of the difference $(g_1 - g_2)$ with $f$ equals the difference of the compositions $(g_1 \circ f) - (g_2 \circ f)$. In symbols: $$(g_1 - g_2) \circ f = g_1 \circ f - g_2 \circ f$$

ContinuousLinearMap.ring instance

[IsTopologicalAddGroup M] : Ring (M →L[R] M)

Full source

instance ring [IsTopologicalAddGroup M] : Ring (M →L[R] M) where
  __ := ContinuousLinearMap.semiring
  __ := ContinuousLinearMap.addCommGroup
  intCast z := z • (1 : M →L[R] M)
  intCast_ofNat := natCast_zsmul _
  intCast_negSucc := negSucc_zsmul _

Ring Structure on Continuous Linear Endomorphisms

Informal description

For any topological module $M$ over a semiring $R$ with continuous addition, the space of continuous linear endomorphisms $M \toL[R] M$ forms a ring under pointwise addition and composition of maps.

ContinuousLinearMap.intCast_apply theorem

[IsTopologicalAddGroup M] (z : ℤ) (m : M) : (↑z : M →L[R] M) m = z • m

Full source

@[simp]
theorem intCast_apply [IsTopologicalAddGroup M] (z : ℤ) (m : M) : (↑z : M →L[R] M) m = z • m :=
  rfl

Integer Scalar Action via Continuous Linear Endomorphisms Equals Scalar Multiplication

Informal description

Let $M$ be a topological module over a semiring $R$ with continuous addition. For any integer $z \in \mathbb{Z}$ and any element $m \in M$, the action of the integer scalar $z$ on $m$ via the canonical continuous linear endomorphism $\overline{z} : M \toL[R] M$ equals the integer scalar multiplication $z \cdot m$. In symbols: $$\overline{z}(m) = z \cdot m$$

ContinuousLinearMap.smulRight_one_pow theorem

 [TopologicalSpace R] [IsTopologicalRing R] (c : R) (n : ℕ) :
  smulRight (1 : R →L[R] R) c ^ n = smulRight (1 : R →L[R] R) (c ^ n)

Full source

theorem smulRight_one_pow [TopologicalSpace R] [IsTopologicalRing R] (c : R) (n : ℕ) :
    smulRight (1 : R →L[R] R) c ^ n = smulRight (1 : R →L[R] R) (c ^ n) := by
  induction n with
  | zero => ext; simp
  | succ n ihn => rw [pow_succ, ihn, mul_def, smulRight_comp, smul_eq_mul, pow_succ']

Power of Scalar Multiplication Map Equals Scalar Power Multiplication Map

Informal description

Let $R$ be a topological ring and let $1 \colon R \toL[R] R$ be the identity continuous linear map. For any element $c \in R$ and natural number $n \in \mathbb{N}$, the $n$-th power of the continuous linear map $\text{smulRight}(1, c)$ (which maps $x \in R$ to $c \cdot x$) equals the continuous linear map $\text{smulRight}(1, c^n)$ (which maps $x \in R$ to $c^n \cdot x$). In symbols: $$(\text{smulRight}(1, c))^n = \text{smulRight}(1, c^n)$$

ContinuousLinearMap.projKerOfRightInverse definition

 [IsTopologicalAddGroup M] (f₁ : M →SL[σ₁₂] M₂) (f₂ : M₂ →SL[σ₂₁] M) (h : Function.RightInverse f₂ f₁) :
  M →L[R] LinearMap.ker f₁

Full source

/-- Given a right inverse `f₂ : M₂ →L[R] M` to `f₁ : M →L[R] M₂`,
`projKerOfRightInverse f₁ f₂ h` is the projection `M →L[R] LinearMap.ker f₁` along
`LinearMap.range f₂`. -/
def projKerOfRightInverse [IsTopologicalAddGroup M] (f₁ : M →SL[σ₁₂] M₂) (f₂ : M₂ →SL[σ₂₁] M)
    (h : Function.RightInverse f₂ f₁) : M →L[R] LinearMap.ker f₁ :=
  (id R M - f₂.comp f₁).codRestrict (LinearMap.ker f₁) fun x => by simp [h (f₁ x)]

Projection onto kernel along range of right inverse

Informal description

Given a continuous semilinear map $ f_1 : M \to_{SL[\sigma_{12}]} M_2 $ and a right inverse $ f_2 : M_2 \to_{SL[\sigma_{21}]} M $ of $ f_1 $ (i.e., $ f_1 \circ f_2 = \text{id} $), the projection $ \text{projKerOfRightInverse} $ maps each $ x \in M $ to $ x - f_2(f_1(x)) $, which lies in the kernel of $ f_1 $. This yields a continuous linear map from $ M $ to the kernel of $ f_1 $.

ContinuousLinearMap.coe_projKerOfRightInverse_apply theorem

 [IsTopologicalAddGroup M] (f₁ : M →SL[σ₁₂] M₂) (f₂ : M₂ →SL[σ₂₁] M) (h : Function.RightInverse f₂ f₁) (x : M) :
  (f₁.projKerOfRightInverse f₂ h x : M) = x - f₂ (f₁ x)

Full source

@[simp]
theorem coe_projKerOfRightInverse_apply [IsTopologicalAddGroup M] (f₁ : M →SL[σ₁₂] M₂)
    (f₂ : M₂ →SL[σ₂₁] M) (h : Function.RightInverse f₂ f₁) (x : M) :
    (f₁.projKerOfRightInverse f₂ h x : M) = x - f₂ (f₁ x) :=
  rfl

Projection Formula for Kernel along Right Inverse: $\text{projKer}(x) = x - f₂(f₁ x)$

Informal description

Let $M$ and $M₂$ be topological modules over semirings $R$ and $S$ respectively, with a ring homomorphism $\sigma_{12} : R \to S$. Given continuous semilinear maps $f₁ : M \to_{SL[\sigma_{12}]} M₂$ and $f₂ : M₂ \to_{SL[\sigma_{21}]} M$ such that $f₂$ is a right inverse of $f₁$ (i.e., $f₁ \circ f₂ = \text{id}_{M₂}$), and assuming $M$ is a topological additive group, then for any $x \in M$, the projection onto the kernel of $f₁$ satisfies $(f₁.\text{projKerOfRightInverse}\ f₂\ h\ x) = x - f₂(f₁ x)$.

ContinuousLinearMap.projKerOfRightInverse_apply_idem theorem

 [IsTopologicalAddGroup M] (f₁ : M →SL[σ₁₂] M₂) (f₂ : M₂ →SL[σ₂₁] M) (h : Function.RightInverse f₂ f₁)
  (x : LinearMap.ker f₁) : f₁.projKerOfRightInverse f₂ h x = x

Full source

@[simp]
theorem projKerOfRightInverse_apply_idem [IsTopologicalAddGroup M] (f₁ : M →SL[σ₁₂] M₂)
    (f₂ : M₂ →SL[σ₂₁] M) (h : Function.RightInverse f₂ f₁) (x : LinearMap.ker f₁) :
    f₁.projKerOfRightInverse f₂ h x = x := by
  ext1
  simp

Idempotence of Projection onto Kernel along Right Inverse

Informal description

Let $M$ and $M_2$ be topological modules over semirings $R$ and $S$ respectively, with a ring homomorphism $\sigma_{12} : R \to S$. Suppose $M$ is a topological additive group. Given continuous semilinear maps $f_1 : M \to_{SL[\sigma_{12}]} M_2$ and $f_2 : M_2 \to_{SL[\sigma_{21}]} M$ such that $f_2$ is a right inverse of $f_1$, then for any $x$ in the kernel of $f_1$, the projection $\text{projKerOfRightInverse}(f_1, f_2, h)(x) = x$.

ContinuousLinearMap.projKerOfRightInverse_comp_inv theorem

 [IsTopologicalAddGroup M] (f₁ : M →SL[σ₁₂] M₂) (f₂ : M₂ →SL[σ₂₁] M) (h : Function.RightInverse f₂ f₁) (y : M₂) :
  f₁.projKerOfRightInverse f₂ h (f₂ y) = 0

Full source

@[simp]
theorem projKerOfRightInverse_comp_inv [IsTopologicalAddGroup M] (f₁ : M →SL[σ₁₂] M₂)
    (f₂ : M₂ →SL[σ₂₁] M) (h : Function.RightInverse f₂ f₁) (y : M₂) :
    f₁.projKerOfRightInverse f₂ h (f₂ y) = 0 :=
  Subtype.ext_iff_val.2 <| by simp [h y]

Projection onto Kernel Vanishes on Range of Right Inverse

Informal description

Let $M$ and $M_2$ be topological modules over semirings $R$ and $S$ respectively, with a ring homomorphism $\sigma_{12} : R \to S$. Assume $M$ is a topological additive group. Given continuous semilinear maps $f_1 : M \to_{SL[\sigma_{12}]} M_2$ and $f_2 : M_2 \to_{SL[\sigma_{21}]} M$ such that $f_2$ is a right inverse of $f_1$ (i.e., $f_1 \circ f_2 = \text{id}_{M_2}$), then for any $y \in M_2$, the projection onto the kernel of $f_1$ satisfies $$ \text{projKerOfRightInverse}(f_1, f_2, h)(f_2 y) = 0. $$

ContinuousLinearMap.isOpenMap_of_ne_zero theorem

 [TopologicalSpace R] [DivisionRing R] [ContinuousSub R] [AddCommGroup M] [TopologicalSpace M] [ContinuousAdd M]
  [Module R M] [ContinuousSMul R M] (f : M →L[R] R) (hf : f ≠ 0) : IsOpenMap f

Full source

/-- A nonzero continuous linear functional is open. -/
protected theorem isOpenMap_of_ne_zero [TopologicalSpace R] [DivisionRing R] [ContinuousSub R]
    [AddCommGroup M] [TopologicalSpace M] [ContinuousAdd M] [Module R M] [ContinuousSMul R M]
    (f : M →L[R] R) (hf : f ≠ 0) : IsOpenMap f :=
  let ⟨x, hx⟩ := exists_ne_zero hf
  IsOpenMap.of_sections fun y =>
    ⟨fun a => y + (a - f y) • (f x)⁻¹ • x, Continuous.continuousAt <| by continuity, by simp,
      fun a => by simp [hx]⟩

Nonzero Continuous Linear Functionals are Open Maps

Informal description

Let $R$ be a topological division ring with continuous subtraction, and let $M$ be a topological module over $R$ with continuous addition and scalar multiplication. For any nonzero continuous $R$-linear functional $f \colon M \to R$, the map $f$ is open.

ContinuousLinearMap.smul_comp theorem

(c : S₃) (h : M₂ →SL[σ₂₃] M₃) (f : M →SL[σ₁₂] M₂) : (c • h).comp f = c • h.comp f

Full source

@[simp]
theorem smul_comp (c : S₃) (h : M₂ →SL[σ₂₃] M₃) (f : M →SL[σ₁₂] M₂) :
    (c • h).comp f = c • h.comp f :=
  rfl

Scalar Multiplication Commutes with Composition of Continuous Semilinear Maps

Informal description

Let $S₃$ be a semiring, and let $M$, $M₂$, $M₃$ be topological modules over semirings $R$, $S₂$, $S₃$ respectively, with ring homomorphisms $\sigma_{12} : R \to S₂$ and $\sigma_{23} : S₂ \to S₃$. For any scalar $c \in S₃$, any continuous semilinear map $h : M₂ \toSL[\sigma_{23}] M₃$, and any continuous semilinear map $f : M \toSL[\sigma_{12}] M₂$, the composition of the scalar multiple $c \cdot h$ with $f$ is equal to the scalar multiple $c$ applied to the composition $h \circ f$, i.e., $$(c \cdot h) \circ f = c \cdot (h \circ f).$$

ContinuousLinearMap.comp_smul theorem

 [LinearMap.CompatibleSMul N₂ N₃ S R] (hₗ : N₂ →L[R] N₃) (c : S) (fₗ : M →L[R] N₂) : hₗ.comp (c • fₗ) = c • hₗ.comp fₗ

Full source

@[simp]
theorem comp_smul [LinearMap.CompatibleSMul N₂ N₃ S R] (hₗ : N₂ →L[R] N₃) (c : S)
    (fₗ : M →L[R] N₂) : hₗ.comp (c • fₗ) = c • hₗ.comp fₗ := by
  ext x
  exact hₗ.map_smul_of_tower c (fₗ x)

Composition of Continuous Linear Maps Commutes with Scalar Multiplication

Informal description

Let $R$ and $S$ be semirings, and let $M$, $N_2$, and $N_3$ be topological modules over $R$ with $N_2$ and $N_3$ also having compatible scalar multiplication by $S$. For any continuous $R$-linear map $h_\ell: N_2 \to_{L[R]} N_3$, scalar $c \in S$, and continuous $R$-linear map $f_\ell: M \to_{L[R]} N_2$, the composition $h_\ell \circ (c \cdot f_\ell)$ equals $c \cdot (h_\ell \circ f_\ell)$.

ContinuousLinearMap.comp_smulₛₗ theorem

 [SMulCommClass R₂ R₂ M₂] [SMulCommClass R₃ R₃ M₃] [ContinuousConstSMul R₂ M₂] [ContinuousConstSMul R₃ M₃]
  (h : M₂ →SL[σ₂₃] M₃) (c : R₂) (f : M →SL[σ₁₂] M₂) : h.comp (c • f) = σ₂₃ c • h.comp f

Full source

@[simp]
theorem comp_smulₛₗ [SMulCommClass R₂ R₂ M₂] [SMulCommClass R₃ R₃ M₃] [ContinuousConstSMul R₂ M₂]
    [ContinuousConstSMul R₃ M₃] (h : M₂ →SL[σ₂₃] M₃) (c : R₂) (f : M →SL[σ₁₂] M₂) :
    h.comp (c • f) = σ₂₃ c • h.comp f := by
  ext x
  simp only [coe_smul', coe_comp', Function.comp_apply, Pi.smul_apply,
    ContinuousLinearMap.map_smulₛₗ]

Composition of scalar multiple with continuous semilinear map

Informal description

Let $R_2$ and $R_3$ be semirings, and let $M_2$ and $M_3$ be topological modules over $R_2$ and $R_3$ respectively, with scalar multiplication actions that are continuous in the second variable. Let $\sigma_{23} \colon R_2 \to R_3$ be a ring homomorphism. For any continuous semilinear map $h \colon M_2 \to_{SL[\sigma_{23}]} M_3$, scalar $c \in R_2$, and continuous semilinear map $f \colon M \to_{SL[\sigma_{12}]} M_2$, the composition of $h$ with the scalar multiple $c \cdot f$ satisfies \[ h \circ (c \cdot f) = \sigma_{23}(c) \cdot (h \circ f). \]

ContinuousLinearMap.distribMulAction instance

[ContinuousAdd M₂] : DistribMulAction S₃ (M →SL[σ₁₂] M₂)

Full source

instance distribMulAction [ContinuousAdd M₂] : DistribMulAction S₃ (M →SL[σ₁₂] M₂) where
  smul_add a f g := ext fun x => smul_add a (f x) (g x)
  smul_zero a := ext fun _ => smul_zero a

Distributive Multiplicative Action on Continuous Semilinear Maps

Informal description

For any semiring $S_3$ and topological modules $M$ and $M_2$ over $S_3$, if $M_2$ has a continuous addition operation, then the space of continuous semilinear maps $M \toSL[\sigma_{12}] M_2$ forms a distributive multiplicative action by elements of $S_3$. This means that for any $a, b \in S_3$ and $f, g \in M \toSL[\sigma_{12}] M_2$, the following properties hold: 1. $a \cdot (f + g) = a \cdot f + a \cdot g$ 2. $(a + b) \cdot f = a \cdot f + b \cdot f$ 3. $a \cdot (b \cdot f) = (a * b) \cdot f$ 4. $1 \cdot f = f$

ContinuousLinearMap.module instance

: Module S₃ (M →SL[σ₁₃] M₃)

Full source

instance module : Module S₃ (M →SL[σ₁₃] M₃) where
  zero_smul _ := ext fun _ => zero_smul S₃ _
  add_smul _ _ _ := ext fun _ => add_smul _ _ _

Module Structure on Continuous Semilinear Maps

Informal description

For any semiring $S_3$ and topological modules $M$ over $R$ and $M_3$ over $S_3$ (with respect to a ring homomorphism $\sigma_{13}: R \to S_3$), the space of continuous semilinear maps $M \toSL[\sigma_{13}] M_3$ forms a module over $S_3$ with pointwise operations.

ContinuousLinearMap.isCentralScalar instance

[Module S₃ᵐᵒᵖ M₃] [IsCentralScalar S₃ M₃] : IsCentralScalar S₃ (M →SL[σ₁₃] M₃)

Full source

instance isCentralScalar [Module S₃ᵐᵒᵖ M₃] [IsCentralScalar S₃ M₃] :
    IsCentralScalar S₃ (M →SL[σ₁₃] M₃) where
  op_smul_eq_smul _ _ := ext fun _ => op_smul_eq_smul _ _

Central Scalar Multiplication on Continuous Semilinear Maps

Informal description

For any semiring $S₃$ and topological modules $M$ and $M₃$ over $S₃$, if $M₃$ has a module structure over the multiplicative opposite $S₃^\text{op}$ and the scalar multiplication on $M₃$ is central (i.e., left and right actions coincide), then the space of continuous semilinear maps $M \toSL[σ₁₃] M₃$ also has a central scalar multiplication structure.

ContinuousLinearMap.coeLM definition

: (M →L[R] N₃) →ₗ[S] M →ₗ[R] N₃

Full source

/-- The coercion from `M →L[R] M₂` to `M →ₗ[R] M₂`, as a linear map. -/
@[simps]
def coeLM : (M →L[R] N₃) →ₗ[S] M →ₗ[R] N₃ where
  toFun := (↑)
  map_add' f g := coe_add f g
  map_smul' c f := coe_smul c f

Coercion from continuous linear maps to linear maps as a linear map

Informal description

The linear map that coerces a continuous linear map $ f: M \toL[R] N_3 $ to its underlying linear map $ f: M \toₗ[R] N_3 $. This map preserves addition and scalar multiplication, meaning for any continuous linear maps $ f, g $ and scalar $ c $, we have $ \overline{f + g} = \overline{f} + \overline{g} $ and $ \overline{c \cdot f} = c \cdot \overline{f} $, where $ \overline{f} $ denotes the underlying linear map of $ f $.

ContinuousLinearMap.coeLMₛₗ definition

: (M →SL[σ₁₃] M₃) →ₗ[S₃] M →ₛₗ[σ₁₃] M₃

Full source

/-- The coercion from `M →SL[σ] M₂` to `M →ₛₗ[σ] M₂`, as a linear map. -/
@[simps]
def coeLMₛₗ : (M →SL[σ₁₃] M₃) →ₗ[S₃] M →ₛₗ[σ₁₃] M₃ where
  toFun := (↑)
  map_add' f g := coe_add f g
  map_smul' c f := coe_smul c f

Coercion from continuous semilinear maps to semilinear maps as a linear map

Informal description

The linear map that coerces a continuous semilinear map $ f: M \toSL[\sigma_{13}] M_3 $ to its underlying semilinear map $ f: M \to_{SL[\sigma_{13}]} M_3 $. This map preserves addition and scalar multiplication, meaning for any continuous semilinear maps $ f, g $ and scalar $ c $, we have $ \overline{f + g} = \overline{f} + \overline{g} $ and $ \overline{c \cdot f} = c \cdot \overline{f} $, where $ \overline{f} $ denotes the underlying semilinear map of $ f $.

ContinuousLinearMap.smulRightₗ definition

(c : M →L[R] S) : M₂ →ₗ[T] M →L[R] M₂

Full source

/-- Given `c : E →L[R] S`, `c.smulRightₗ` is the linear map from `F` to `E →L[R] F`
sending `f` to `fun e => c e • f`. See also `ContinuousLinearMap.smulRightL`. -/
def smulRightₗ (c : M →L[R] S) : M₂ →ₗ[T] M →L[R] M₂ where
  toFun := c.smulRight
  map_add' x y := by
    ext e
    apply smul_add (c e)
  map_smul' a x := by
    ext e
    dsimp
    apply smul_comm

Linear map of scalar multiplication with a continuous linear map

Informal description

Given a continuous linear map $ c : M \to_L[R] S $, the function `ContinuousLinearMap.smulRightₗ` is the linear map from $ M_2 $ to the space of continuous linear maps $ M \to_L[R] M_2 $, defined by sending an element $ f \in M_2 $ to the continuous linear map $ e \mapsto c(e) \cdot f $. This construction preserves addition and scalar multiplication, satisfying: - Additivity: $ c(e) \cdot (f + g) = c(e) \cdot f + c(e) \cdot g $ for all $ e \in M $ and $ f, g \in M_2 $. - Scalar compatibility: $ c(e) \cdot (a \cdot f) = a \cdot (c(e) \cdot f) $ for all $ e \in M $, $ f \in M_2 $, and scalar $ a $.

ContinuousLinearMap.coe_smulRightₗ theorem

(c : M →L[R] S) : ⇑(smulRightₗ c : M₂ →ₗ[T] M →L[R] M₂) = c.smulRight

Full source

@[simp]
theorem coe_smulRightₗ (c : M →L[R] S) : ⇑(smulRightₗ c : M₂ →ₗ[T] M →L[R] M₂) = c.smulRight :=
  rfl

Equality of Underlying Functions for Scalar Multiplication Linear Map

Informal description

For any continuous linear map $c \colon M \to_L[R] S$, the underlying function of the linear map $\text{smulRight}_\ell(c) \colon M_2 \to_\ell[T] (M \to_L[R] M_2)$ is equal to the scalar multiplication map $c.\text{smulRight}$.

ContinuousLinearMap.algebra instance

: Algebra R (M₂ →L[R] M₂)

Full source

instance algebra : Algebra R (M₂ →L[R] M₂) :=
  Algebra.ofModule smul_comp fun _ _ _ => comp_smul _ _ _

Algebra Structure on Continuous Linear Endomorphisms

Informal description

For any topological module $M_2$ over a semiring $R$, the space of continuous linear endomorphisms $M_2 \toL[R] M_2$ forms an $R$-algebra under pointwise addition, scalar multiplication, and composition of maps.

ContinuousLinearMap.algebraMap_apply theorem

(r : R) (m : M₂) : algebraMap R (M₂ →L[R] M₂) r m = r • m

Full source

@[simp] theorem algebraMap_apply (r : R) (m : M₂) : algebraMap R (M₂ →L[R] M₂) r m = r • m := rfl

Evaluation of Algebra Homomorphism on Scalar Multiplication: $\text{algebraMap}_R(r)(m) = r \cdot m$

Informal description

For any scalar $r$ in a semiring $R$ and any element $m$ in a topological module $M_2$ over $R$, the evaluation of the algebra homomorphism $\text{algebraMap}_R$ at $r$ applied to $m$ equals the scalar multiplication of $r$ with $m$, i.e., $\text{algebraMap}_R(r)(m) = r \cdot m$.

ContinuousLinearMap.restrictScalars definition

(f : M₁ →L[A] M₂) : M₁ →L[R] M₂

Full source

/-- If `A` is an `R`-algebra, then a continuous `A`-linear map can be interpreted as a continuous
`R`-linear map. We assume `LinearMap.CompatibleSMul M₁ M₂ R A` to match assumptions of
`LinearMap.map_smul_of_tower`. -/
def restrictScalars (f : M₁ →L[A] M₂) : M₁ →L[R] M₂ :=
  ⟨(f : M₁ →ₗ[A] M₂).restrictScalars R, f.continuous⟩

Restriction of scalars for continuous linear maps

Informal description

Given an $A$-algebra $R$ and continuous $A$-linear maps $f \colon M_1 \to M_2$, the function `restrictScalars` interprets $f$ as a continuous $R$-linear map $M_1 \to M_2$ by restricting the scalar action from $A$ to $R$. This requires that the scalar multiplication is compatible between $R$ and $A$ (i.e., `LinearMap.CompatibleSMul M₁ M₂ R A` holds).

ContinuousLinearMap.coe_restrictScalars theorem

(f : M₁ →L[A] M₂) : (f.restrictScalars R : M₁ →ₗ[R] M₂) = (f : M₁ →ₗ[A] M₂).restrictScalars R

Full source

@[simp]
theorem coe_restrictScalars (f : M₁ →L[A] M₂) :
    (f.restrictScalars R : M₁ →ₗ[R] M₂) = (f : M₁ →ₗ[A] M₂).restrictScalars R := rfl

Compatibility of scalar restriction with underlying linear maps

Informal description

For any continuous $A$-linear map $f \colon M_1 \to M_2$, the underlying $R$-linear map obtained by restricting scalars (from $A$ to $R$) of $f$ is equal to the restriction of scalars of the underlying $A$-linear map of $f$. In other words, the following diagram commutes: $$(f.restrictScalars\, R : M_1 \to_{R} M_2) = (f : M_1 \to_{A} M_2).restrictScalars\, R$$

ContinuousLinearMap.coe_restrictScalars' theorem

(f : M₁ →L[A] M₂) : ⇑(f.restrictScalars R) = f

Full source

@[simp]
theorem coe_restrictScalars' (f : M₁ →L[A] M₂) : ⇑(f.restrictScalars R) = f := rfl

Underlying Function Unchanged by Scalar Restriction

Informal description

For any continuous $A$-linear map $f \colon M_1 \to M_2$, the underlying function of its scalar restriction to $R$ (denoted $f.\text{restrictScalars}\, R$) is equal to $f$ itself. In other words, restricting the scalars of $f$ from $A$ to $R$ does not change the function's action on elements of $M_1$.

ContinuousLinearMap.toContinuousAddMonoidHom_restrictScalars theorem

(f : M₁ →L[A] M₂) : ↑(f.restrictScalars R) = (f : ContinuousAddMonoidHom M₁ M₂)

Full source

@[simp]
theorem toContinuousAddMonoidHom_restrictScalars (f : M₁ →L[A] M₂) :
    ↑(f.restrictScalars R) = (f : ContinuousAddMonoidHom M₁ M₂) := rfl

Compatibility of Scalar Restriction with Continuous Additive Monoid Homomorphism Structure

Informal description

Let $M₁$ and $M₂$ be topological modules over a semiring $A$, and let $R$ be an $A$-algebra. For any continuous $A$-linear map $f \colon M₁ \to M₂$, the underlying continuous additive monoid homomorphism of the scalar-restricted map $f.restrictScalars R$ is equal to the underlying continuous additive monoid homomorphism of $f$.

ContinuousLinearMap.restrictScalars_zero theorem

: (0 : M₁ →L[A] M₂).restrictScalars R = 0

Full source

@[simp] lemma restrictScalars_zero : (0 : M₁ →L[A] M₂).restrictScalars R = 0 := rfl

Restriction of scalars preserves the zero map

Informal description

The restriction of scalars of the zero continuous linear map from $M_1$ to $M_2$ (over an $A$-algebra $R$) is equal to the zero continuous linear map.

ContinuousLinearMap.restrictScalars_add theorem

[ContinuousAdd M₂] (f g : M₁ →L[A] M₂) : (f + g).restrictScalars R = f.restrictScalars R + g.restrictScalars R

Full source

@[simp]
lemma restrictScalars_add [ContinuousAdd M₂] (f g : M₁ →L[A] M₂) :
    (f + g).restrictScalars R = f.restrictScalars R + g.restrictScalars R := rfl

Additivity of Scalar Restriction for Continuous Linear Maps

Informal description

Let $M_1$ and $M_2$ be topological modules over a semiring $A$, and let $R$ be an $A$-algebra. For any continuous $A$-linear maps $f, g \colon M_1 \to M_2$, the restriction of scalars of their sum is equal to the sum of their scalar restrictions, i.e., $$(f + g).\text{restrictScalars}\, R = f.\text{restrictScalars}\, R + g.\text{restrictScalars}\, R.$$

ContinuousLinearMap.restrictScalars_smul theorem

(c : S) (f : M₁ →L[A] M₂) : (c • f).restrictScalars R = c • f.restrictScalars R

Full source

@[simp]
theorem restrictScalars_smul (c : S) (f : M₁ →L[A] M₂) :
    (c • f).restrictScalars R = c • f.restrictScalars R :=
  rfl

Compatibility of scalar multiplication with restriction of scalars for continuous linear maps

Informal description

Let $R$ be an $A$-algebra and $S$ a semiring. For any scalar $c \in S$ and any continuous $A$-linear map $f \colon M_1 \to M_2$, the restriction of scalars of the scalar multiple $c \cdot f$ is equal to the scalar multiple of the restriction of scalars of $f$, i.e., $$(c \cdot f)\big|_{R} = c \cdot (f\big|_{R}).$$

ContinuousLinearMap.restrictScalarsₗ definition

: (M₁ →L[A] M₂) →ₗ[S] M₁ →L[R] M₂

Full source

/-- `ContinuousLinearMap.restrictScalars` as a `LinearMap`. See also
`ContinuousLinearMap.restrictScalarsL`. -/
def restrictScalarsₗ : (M₁ →L[A] M₂) →ₗ[S] M₁ →L[R] M₂ where
  toFun := restrictScalars R
  map_add' := restrictScalars_add
  map_smul' := restrictScalars_smul

Linear map of scalar restriction for continuous linear maps

Informal description

The linear map that restricts the scalar action of continuous linear maps from an $A$-algebra $R$ to $S$, where $S$ is a semiring. Specifically, given topological modules $M_1$ and $M_2$ over $A$ and $R$ respectively, the map `restrictScalarsₗ` takes a continuous $A$-linear map $f \colon M_1 \to M_2$ and returns a continuous $R$-linear map $M_1 \to M_2$ by restricting the scalar action from $A$ to $R$. This map is itself $S$-linear, meaning it preserves addition and scalar multiplication by elements of $S$.

ContinuousLinearMap.coe_restrictScalarsₗ theorem

: ⇑(restrictScalarsₗ A M₁ M₂ R S) = restrictScalars R

Full source

@[simp]
theorem coe_restrictScalarsₗ : ⇑(restrictScalarsₗ A M₁ M₂ R S) = restrictScalars R := rfl

Underlying Function of Scalar Restriction Linear Map Equals Scalar Restriction Function

Informal description

The underlying function of the linear map `restrictScalarsₗ` that restricts the scalar action of continuous linear maps from an $A$-algebra $R$ to a semiring $S$ is equal to the function `restrictScalars` that performs the scalar restriction directly.

ContinuousLinearMap.restrictScalars_sub theorem

(f g : M₁ →L[A] M₂) : (f - g).restrictScalars R = f.restrictScalars R - g.restrictScalars R

Full source

@[simp]
lemma restrictScalars_sub (f g : M₁ →L[A] M₂) :
    (f - g).restrictScalars R = f.restrictScalars R - g.restrictScalars R := rfl

Restriction of Scalars Preserves Subtraction of Continuous Linear Maps

Informal description

Let $M_1$ and $M_2$ be topological modules over an $A$-algebra $R$, and let $f, g \colon M_1 \to_{L[A]} M_2$ be continuous $A$-linear maps. Then the restriction of scalars of the difference $f - g$ is equal to the difference of the restrictions of scalars of $f$ and $g$, i.e., $$(f - g).\text{restrictScalars}\, R = f.\text{restrictScalars}\, R - g.\text{restrictScalars}\, R.$$

ContinuousLinearMap.restrictScalars_neg theorem

(f : M₁ →L[A] M₂) : (-f).restrictScalars R = -f.restrictScalars R

Full source

@[simp]
lemma restrictScalars_neg (f : M₁ →L[A] M₂) : (-f).restrictScalars R = -f.restrictScalars R := rfl

Negation Commutes with Restriction of Scalars for Continuous Linear Maps

Informal description

For any continuous $A$-linear map $f \colon M_1 \to M_2$, the restriction of scalars of the negation of $f$ equals the negation of the restriction of scalars of $f$. In other words, $(-f)\restrictScalars R = -(f\restrictScalars R)$.

Submodule.ClosedComplemented definition

(p : Submodule R M) : Prop

Full source

/-- A submodule `p` is called *complemented* if there exists a continuous projection `M →ₗ[R] p`. -/
def ClosedComplemented (p : Submodule R M) : Prop :=
  ∃ f : M →L[R] p, ∀ x : p, f x = x

Complemented submodule

Informal description

A submodule $p$ of a topological module $M$ over a semiring $R$ is called *complemented* if there exists a continuous linear map $f: M \to p$ such that $f(x) = x$ for all $x \in p$. In other words, $f$ is a continuous projection onto $p$.

Submodule.ClosedComplemented.exists_isClosed_isCompl theorem

 {p : Submodule R M} [T1Space p] (h : ClosedComplemented p) : ∃ q : Submodule R M, IsClosed (q : Set M) ∧ IsCompl p q

Full source

theorem ClosedComplemented.exists_isClosed_isCompl {p : Submodule R M} [T1Space p]
    (h : ClosedComplemented p) :
    ∃ q : Submodule R M, IsClosed (q : Set M) ∧ IsCompl p q :=
  Exists.elim h fun f hf => ⟨ker f, isClosed_ker f, LinearMap.isCompl_of_proj hf⟩

Existence of Closed Complement for Complemented Submodules in T₁ Spaces

Informal description

Let $M$ be a topological module over a semiring $R$, and let $p$ be a complemented submodule of $M$ such that $p$ is a T₁ space. Then there exists a submodule $q$ of $M$ such that: 1. The subset corresponding to $q$ is closed in $M$. 2. $p$ and $q$ are complements, i.e., $p \sqcap q = \bot$ and $p \sqcup q = \top$.

Submodule.ClosedComplemented.isClosed theorem

[IsTopologicalAddGroup M] [T1Space M] {p : Submodule R M} (h : ClosedComplemented p) : IsClosed (p : Set M)

Full source

protected theorem ClosedComplemented.isClosed [IsTopologicalAddGroup M] [T1Space M]
    {p : Submodule R M} (h : ClosedComplemented p) : IsClosed (p : Set M) := by
  rcases h with ⟨f, hf⟩
  have : ker (id R M - p.subtypeL.comp f) = p := LinearMap.ker_id_sub_eq_of_proj hf
  exact this ▸ isClosed_ker _

Closedness of Complemented Submodules in T₁ Topological Modules

Informal description

Let $M$ be a topological module over a semiring $R$ such that $M$ is a T₁ space and its additive group is a topological group. If a submodule $p$ of $M$ is complemented (i.e., there exists a continuous linear projection onto $p$), then $p$ is a closed subset of $M$.

Submodule.closedComplemented_bot theorem

: ClosedComplemented (⊥ : Submodule R M)

Full source

@[simp]
theorem closedComplemented_bot : ClosedComplemented (⊥ : Submodule R M) :=
  ⟨0, fun x => by simp only [zero_apply, eq_zero_of_bot_submodule x]⟩

Trivial Submodule is Complemented

Informal description

The trivial submodule $\{0\}$ (denoted as $\bot$) of a topological module $M$ over a semiring $R$ is complemented. That is, there exists a continuous linear projection from $M$ onto $\{0\}$.

Submodule.closedComplemented_top theorem

: ClosedComplemented (⊤ : Submodule R M)

Full source

@[simp]
theorem closedComplemented_top : ClosedComplemented (⊤ : Submodule R M) :=
  ⟨(id R M).codRestrict ⊤ fun _x => trivial, fun x => Subtype.ext_iff_val.2 <| by simp⟩

Top Submodule is Complemented

Informal description

The top submodule $\top$ of a topological module $M$ over a semiring $R$ is complemented, meaning there exists a continuous linear projection from $M$ onto $\top$.

ContinuousLinearMap.closedComplemented_ker_of_rightInverse theorem

 {R : Type*} [Ring R] {M : Type*} [TopologicalSpace M] [AddCommGroup M] {M₂ : Type*} [TopologicalSpace M₂]
  [AddCommGroup M₂] [Module R M] [Module R M₂] [IsTopologicalAddGroup M] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M)
  (h : Function.RightInverse f₂ f₁) : (ker f₁).ClosedComplemented

Full source

theorem ContinuousLinearMap.closedComplemented_ker_of_rightInverse {R : Type*} [Ring R]
    {M : Type*} [TopologicalSpace M] [AddCommGroup M] {M₂ : Type*} [TopologicalSpace M₂]
    [AddCommGroup M₂] [Module R M] [Module R M₂] [IsTopologicalAddGroup M] (f₁ : M →L[R] M₂)
    (f₂ : M₂ →L[R] M) (h : Function.RightInverse f₂ f₁) : (ker f₁).ClosedComplemented :=
  ⟨f₁.projKerOfRightInverse f₂ h, f₁.projKerOfRightInverse_apply_idem f₂ h⟩

Kernel of a Continuous Linear Map with Right Inverse is Complemented

Informal description

Let $R$ be a ring, and let $M$ and $M_2$ be topological additive groups equipped with $R$-module structures. Suppose $M$ is a topological additive group. Given continuous linear maps $f_1 : M \to_L[R] M_2$ and $f_2 : M_2 \to_L[R] M$ such that $f_2$ is a right inverse of $f_1$ (i.e., $f_1 \circ f_2 = \text{id}$), then the kernel of $f_1$ is a complemented submodule. That is, there exists a continuous linear projection from $M$ onto $\ker f_1$.