Mathlib.Analysis.Normed.Operator.LinearIsometry

LinearIsometry structure

(σ₁₂ : R →+* R₂) (E E₂ : Type*) [SeminormedAddCommGroup E]
  [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] extends E →ₛₗ[σ₁₂] E₂

Full source

/-- A `σ₁₂`-semilinear isometric embedding of a normed `R`-module into an `R₂`-module,
denoted as `f : E →ₛₗᵢ[σ₁₂] E₂`. -/
structure LinearIsometry (σ₁₂ : R →+* R₂) (E E₂ : Type*) [SeminormedAddCommGroup E]
  [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] extends E →ₛₗ[σ₁₂] E₂ where
  norm_map' : ∀ x, ‖toLinearMap x‖ = ‖x‖

Semilinear isometric embedding

Informal description

A $\sigma_{12}$-semilinear isometric embedding between two seminormed modules $E$ and $E_2$ over rings $R$ and $R_2$ respectively, where $\sigma_{12} : R \to R_2$ is a ring homomorphism. This structure extends a $\sigma_{12}$-semilinear map and additionally preserves the norm: $\|f(x)\| = \|x\|$ for all $x \in E$.

term_→ₛₗᵢ[_]_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
notation:25 E " →ₛₗᵢ[" σ₁₂:25 "] " E₂:0 => LinearIsometry σ₁₂ E E₂

Semilinear isometric embedding notation

Informal description

The notation `E →ₛₗᵢ[σ₁₂] E₂` represents the type of semilinear isometric embeddings from `E` to `E₂`, where `σ₁₂` is a ring homomorphism between the scalar rings of `E` and `E₂`. These embeddings preserve the norm structure while being linear up to the ring homomorphism `σ₁₂`.

term_→ₗᵢ[_]_ definition

: Lean.TrailingParserDescr✝

Full source

/-- A linear isometric embedding of a normed `R`-module into another one. -/
notation:25 E " →ₗᵢ[" R:25 "] " E₂:0 => LinearIsometry (RingHom.id R) E E₂

Linear isometric embedding notation

Informal description

The notation $ E \to_{l^i}[R] E_2 $ represents a linear isometric embedding from a normed $ R $-module $ E $ to another normed $ R $-module $ E_2 $. This is a linear map that preserves the norm of vectors.

term_→ₗᵢ⋆[_]_ definition

: Lean.TrailingParserDescr✝

Full source

/-- An antilinear isometric embedding of a normed `R`-module into another one. -/
notation:25 E " →ₗᵢ⋆[" R:25 "] " E₂:0 => LinearIsometry (starRingEnd R) E E₂

Antilinear isometric embedding notation

Informal description

The notation $ E \to_{l^i\star}[R] E_2 $ represents an antilinear isometric embedding from a normed $ R $-module $ E $ to another normed $ R $-module $ E_2 $. Here, the map is antilinear with respect to the star ring endomorphism of $ R $.

SemilinearIsometryClass structure

(𝓕 : Type*) {R R₂ : outParam Type*} [Semiring R] [Semiring R₂]
    (σ₁₂ : outParam <| R →+* R₂) (E E₂ : outParam Type*) [SeminormedAddCommGroup E]
    [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] [FunLike 𝓕 E E₂] : Prop
    extends SemilinearMapClass 𝓕 σ₁₂ E E₂

Full source

/-- `SemilinearIsometryClass F σ E E₂` asserts `F` is a type of bundled `σ`-semilinear isometries
`E → E₂`.

See also `LinearIsometryClass F R E E₂` 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 SemilinearIsometryClass (𝓕 : Type*) {R R₂ : outParam Type*} [Semiring R] [Semiring R₂]
    (σ₁₂ : outParam <| R →+* R₂) (E E₂ : outParam Type*) [SeminormedAddCommGroup E]
    [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] [FunLike 𝓕 E E₂] : Prop
    extends SemilinearMapClass 𝓕 σ₁₂ E E₂ where
  norm_map : ∀ (f : 𝓕) (x : E), ‖f x‖ = ‖x‖

Class of Semilinear Isometries

Informal description

The class `SemilinearIsometryClass 𝓕 σ₁₂ E E₂` asserts that `𝓕` is a type of bundled `σ₁₂`-semilinear isometries from `E` to `E₂`. Here, `σ₁₂` is a ring homomorphism between semirings `R` and `R₂`, and `E` and `E₂` are seminormed additive commutative groups equipped with module structures over `R` and `R₂` respectively. A map `f : 𝓕` is a semilinear isometry if it preserves addition (`f (x + y) = f x + f y`), scalar multiplication (`f (c • x) = (σ₁₂ c) • f x`), and the norm (`‖f x‖ = ‖x‖`).

LinearIsometryClass abbrev

 (𝓕 : Type*) (R E E₂ : outParam Type*) [Semiring R] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E]
  [Module R E₂] [FunLike 𝓕 E E₂]

Full source

/-- `LinearIsometryClass F R E E₂` asserts `F` is a type of bundled `R`-linear isometries
`M → M₂`.

This is an abbreviation for `SemilinearIsometryClass F (RingHom.id R) E E₂`.
-/
abbrev LinearIsometryClass (𝓕 : Type*) (R E E₂ : outParam Type*) [Semiring R]
    [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R E₂]
    [FunLike 𝓕 E E₂] :=
  SemilinearIsometryClass 𝓕 (RingHom.id R) E E₂

Class of Linear Isometries between Seminormed Modules

Informal description

The class `LinearIsometryClass 𝓕 R E E₂` asserts that `𝓕` is a type of bundled `R`-linear isometries from `E$ to $E₂$, where $R$ is a semiring, and $E$ and $E₂$ are seminormed additive commutative groups equipped with module structures over $R$. A map $f : 𝓕$ is a linear isometry if it preserves addition ($f (x + y) = f x + f y$), scalar multiplication ($f (c \cdot x) = c \cdot f x$), and the norm ($\|f x\| = \|x\|$).

SemilinearIsometryClass.isometry theorem

[SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) : Isometry f

Full source

protected theorem isometry [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) : Isometry f :=
  AddMonoidHomClass.isometry_of_norm _ (norm_map _)

Semilinear Isometries are Isometries

Informal description

For any semilinear isometry $f$ in the class `SemilinearIsometryClass 𝓕 σ₁₂ E E₂`, the map $f$ is an isometry, meaning it preserves distances between points in the seminormed additive commutative groups $E$ and $E₂$.

SemilinearIsometryClass.continuous theorem

[SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) : Continuous f

Full source

@[continuity]
protected theorem continuous [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) : Continuous f :=
  (SemilinearIsometryClass.isometry f).continuous

Continuity of Semilinear Isometries

Informal description

For any semilinear isometry $f$ in the class `SemilinearIsometryClass 𝓕 σ₁₂ E E₂`, the map $f$ is continuous.

SemilinearIsometryClass.nnnorm_map theorem

[SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) (x : E) : ‖f x‖₊ = ‖x‖₊

Full source

theorem nnnorm_map [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) (x : E) : ‖f x‖₊ = ‖x‖₊ :=
  NNReal.eq <| norm_map f x

Seminorm Preservation under Semilinear Isometries: $\|f(x)\|_+ = \|x\|_+$

Informal description

For any semilinear isometry $f$ in the class `SemilinearIsometryClass 𝓕 σ₁₂ E E₂` and any element $x$ in the seminormed additive commutative group $E$, the seminorm of $f(x)$ is equal to the seminorm of $x$, i.e., $\|f(x)\|_+ = \|x\|_+$.

SemilinearIsometryClass.lipschitz theorem

[SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) : LipschitzWith 1 f

Full source

protected theorem lipschitz [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) : LipschitzWith 1 f :=
  (SemilinearIsometryClass.isometry f).lipschitz

Semilinear Isometries are 1-Lipschitz

Informal description

For any semilinear isometry $f \colon E \to E₂$ with respect to a ring homomorphism $\sigma_{12} \colon R \to R₂$, the map $f$ is Lipschitz continuous with constant $1$, i.e., for all $x, y \in E$, \[ \|f(x) - f(y)\| \leq \|x - y\|. \]

SemilinearIsometryClass.antilipschitz theorem

[SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) : AntilipschitzWith 1 f

Full source

protected theorem antilipschitz [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) :
    AntilipschitzWith 1 f :=
  (SemilinearIsometryClass.isometry f).antilipschitz

Antilipschitz Property of Semilinear Isometries: $\|x - y\| \leq \|f(x) - f(y)\|$

Informal description

For any semilinear isometry $f$ in the class `SemilinearIsometryClass 𝓕 σ₁₂ E E₂`, the map $f$ is antilipschitz with constant $1$, meaning that for all $x, y \in E$, we have $\|x - y\| \leq \|f(x) - f(y)\|$.

SemilinearIsometryClass.ediam_image theorem

[SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) (s : Set E) : EMetric.diam (f '' s) = EMetric.diam s

Full source

theorem ediam_image [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) (s : Set E) :
    EMetric.diam (f '' s) = EMetric.diam s :=
  (SemilinearIsometryClass.isometry f).ediam_image s

Preservation of Extended Metric Diameter under Semilinear Isometries

Informal description

Let $E$ and $E₂$ be seminormed additive commutative groups equipped with module structures over semirings $R$ and $R₂$ respectively, and let $\sigma_{12} \colon R \to R₂$ be a ring homomorphism. For any semilinear isometry $f \colon E \to E₂$ in the class `SemilinearIsometryClass 𝓕 σ₁₂ E E₂` and any subset $s \subseteq E$, the extended metric diameter of the image $f(s)$ is equal to the extended metric diameter of $s$, i.e., \[ \text{diam}(f(s)) = \text{diam}(s). \]

SemilinearIsometryClass.ediam_range theorem

[SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) : EMetric.diam (range f) = EMetric.diam (univ : Set E)

Full source

theorem ediam_range [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) :
    EMetric.diam (range f) = EMetric.diam (univ : Set E) :=
  (SemilinearIsometryClass.isometry f).ediam_range

Preservation of Extended Metric Diameter by Semilinear Isometries

Informal description

For any semilinear isometry $f$ from a seminormed additive commutative group $E$ to another seminormed additive commutative group $E₂$ (with respect to a ring homomorphism $\sigma_{12}$), the extended metric diameter of the range of $f$ is equal to the extended metric diameter of the entire space $E$.

SemilinearIsometryClass.diam_image theorem

[SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) (s : Set E) : Metric.diam (f '' s) = Metric.diam s

Full source

theorem diam_image [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) (s : Set E) :
    Metric.diam (f '' s) = Metric.diam s :=
  (SemilinearIsometryClass.isometry f).diam_image s

Diameter Preservation under Semilinear Isometries

Informal description

Let $E$ and $E₂$ be seminormed additive commutative groups with module structures over semirings $R$ and $R₂$ respectively, and let $\sigma₁₂: R \to R₂$ be a ring homomorphism. For any semilinear isometry $f$ in the class `SemilinearIsometryClass 𝓕 σ₁₂ E E₂` and any subset $s \subseteq E$, the diameter of the image $f(s)$ equals the diameter of $s$, i.e., $\text{diam}(f(s)) = \text{diam}(s)$.

SemilinearIsometryClass.diam_range theorem

[SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) : Metric.diam (range f) = Metric.diam (univ : Set E)

Full source

theorem diam_range [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) :
    Metric.diam (range f) = Metric.diam (univ : Set E) :=
  (SemilinearIsometryClass.isometry f).diam_range

Diameter Preservation of Semilinear Isometries

Informal description

For any semilinear isometry $f \colon E \to E_2$ in the class `SemilinearIsometryClass 𝓕 σ₁₂ E E₂`, the diameter of the range of $f$ is equal to the diameter of the entire space $E$. That is, $\text{diam}(\text{range}(f)) = \text{diam}(E)$.

SemilinearIsometryClass.toContinuousSemilinearMapClass instance

[SemilinearIsometryClass 𝓕 σ₁₂ E E₂] : ContinuousSemilinearMapClass 𝓕 σ₁₂ E E₂

Full source

instance (priority := 100) toContinuousSemilinearMapClass
    [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] : ContinuousSemilinearMapClass 𝓕 σ₁₂ E E₂ where
  map_continuous := SemilinearIsometryClass.continuous

Semilinear Isometries are Continuous Semilinear Maps

Informal description

Every semilinear isometry between seminormed modules is a continuous semilinear map.

LinearIsometry.toLinearMap_injective theorem

: Injective (toLinearMap : (E →ₛₗᵢ[σ₁₂] E₂) → E →ₛₗ[σ₁₂] E₂)

Full source

theorem toLinearMap_injective : Injective (toLinearMap : (E →ₛₗᵢ[σ₁₂] E₂) → E →ₛₗ[σ₁₂] E₂)
  | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl

Injectivity of the Underlying Semilinear Map Construction for Semilinear Isometric Embeddings

Informal description

The map from semilinear isometric embeddings $f \colon E \to_{\sigma_{12}} E_2$ to their underlying semilinear maps is injective. In other words, if two semilinear isometric embeddings have the same underlying semilinear map, then they must be equal.

LinearIsometry.toLinearMap_inj theorem

{f g : E →ₛₗᵢ[σ₁₂] E₂} : f.toLinearMap = g.toLinearMap ↔ f = g

Full source

@[simp]
theorem toLinearMap_inj {f g : E →ₛₗᵢ[σ₁₂] E₂} : f.toLinearMap = g.toLinearMap ↔ f = g :=
  toLinearMap_injective.eq_iff

Equality of Semilinear Isometric Embeddings via Underlying Maps

Informal description

For any two semilinear isometric embeddings $f, g \colon E \to_{\sigma_{12}} E_2$ between seminormed modules, the underlying semilinear maps of $f$ and $g$ are equal if and only if $f$ and $g$ are equal as isometric embeddings.

LinearIsometry.instFunLike instance

: FunLike (E →ₛₗᵢ[σ₁₂] E₂) E E₂

Full source

instance instFunLike : FunLike (E →ₛₗᵢ[σ₁₂] E₂) E E₂ where
  coe f := f.toFun
  coe_injective' _ _ h := toLinearMap_injective (DFunLike.coe_injective h)

Function-Like Structure for Semilinear Isometric Embeddings

Informal description

For any semilinear isometric embedding $f : E \to E_2$ between seminormed modules, the type of such embeddings $E \to_{σ₁₂} E_2$ is equipped with a function-like structure, meaning it can be coerced to a function from $E$ to $E_2$ in a way that preserves injectivity.

LinearIsometry.instSemilinearIsometryClass instance

: SemilinearIsometryClass (E →ₛₗᵢ[σ₁₂] E₂) σ₁₂ E E₂

Full source

instance instSemilinearIsometryClass : SemilinearIsometryClass (E →ₛₗᵢ[σ₁₂] E₂) σ₁₂ E E₂ where
  map_add f := map_add f.toLinearMap
  map_smulₛₗ f := map_smulₛₗ f.toLinearMap
  norm_map f := f.norm_map'

Semilinear Isometry Class for Semilinear Isometric Embeddings

Informal description

The type of semilinear isometric embeddings $E \to_{σ₁₂} E₂$ forms a class of semilinear isometries, where each embedding preserves addition, scalar multiplication (with respect to the ring homomorphism $σ₁₂$), and the norm.

LinearIsometry.coe_toLinearMap theorem

: ⇑f.toLinearMap = f

Full source

@[simp]
theorem coe_toLinearMap : ⇑f.toLinearMap = f :=
  rfl

Underlying Function of Linear Isometry's Linear Map Equals the Isometry

Informal description

For a semilinear isometric embedding $f \colon E \to E_2$, the underlying function of its associated linear map $f.toLinearMap$ is equal to $f$ itself.

LinearIsometry.coe_mk theorem

(f : E →ₛₗ[σ₁₂] E₂) (hf) : ⇑(mk f hf) = f

Full source

@[simp]
theorem coe_mk (f : E →ₛₗ[σ₁₂] E₂) (hf) : ⇑(mk f hf) = f :=
  rfl

Underlying Function of Constructed Linear Isometry Equals Original Map

Informal description

For any semilinear map $f \colon E \to E_2$ between seminormed modules that preserves the norm (i.e., $\|f(x)\| = \|x\|$ for all $x \in E$), the underlying function of the constructed linear isometry $\text{mk}(f, hf)$ is equal to $f$.

LinearIsometry.coe_injective theorem

: @Injective (E →ₛₗᵢ[σ₁₂] E₂) (E → E₂) (fun f => f)

Full source

theorem coe_injective : @Injective (E →ₛₗᵢ[σ₁₂] E₂) (E → E₂) (fun f => f) := by
  rintro ⟨_⟩ ⟨_⟩
  simp

Injectivity of the Underlying Function Map for Semilinear Isometric Embeddings

Informal description

The canonical map from the type of semilinear isometric embeddings $E \to_{\sigma_{12}} E_2$ to the type of functions $E \to E_2$ is injective. In other words, if two semilinear isometric embeddings $f$ and $g$ satisfy $f(x) = g(x)$ for all $x \in E$, then $f = g$.

LinearIsometry.Simps.apply definition

 (σ₁₂ : R →+* R₂) (E E₂ : Type*) [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂]
  (h : E →ₛₗᵢ[σ₁₂] E₂) : E → E₂

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 (σ₁₂ : R →+* R₂) (E E₂ : Type*) [SeminormedAddCommGroup E]
    [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (h : E →ₛₗᵢ[σ₁₂] E₂) : E → E₂ :=
  h

Underlying map of a semilinear isometric embedding

Informal description

The function that extracts the underlying map from a semilinear isometric embedding $h \colon E \to_{σ₁₂} E₂$ between seminormed modules $E$ and $E₂$ over rings $R$ and $R₂$ respectively, where $σ₁₂ \colon R \to R₂$ is a ring homomorphism. This function simply returns the map $h$ itself, viewed as a function from $E$ to $E₂$.

LinearIsometry.ext theorem

{f g : E →ₛₗᵢ[σ₁₂] E₂} (h : ∀ x, f x = g x) : f = g

Full source

@[ext]
theorem ext {f g : E →ₛₗᵢ[σ₁₂] E₂} (h : ∀ x, f x = g x) : f = g :=
  coe_injective <| funext h

Extensionality of Semilinear Isometric Embeddings

Informal description

For any two semilinear isometric embeddings $f, g \colon E \to_{\sigma_{12}} E_2$, if $f(x) = g(x)$ for all $x \in E$, then $f = g$.

LinearIsometry.map_zero theorem

: f 0 = 0

Full source

protected theorem map_zero : f 0 = 0 :=
  f.toLinearMap.map_zero

Preservation of Zero under Semilinear Isometric Embeddings

Informal description

For any semilinear isometric embedding $f \colon E \to E_2$, the image of the zero vector is preserved, i.e., $f(0) = 0$.

LinearIsometry.map_add theorem

(x y : E) : f (x + y) = f x + f y

Full source

protected theorem map_add (x y : E) : f (x + y) = f x + f y :=
  f.toLinearMap.map_add x y

Additivity of Semilinear Isometric Embeddings

Informal description

For any semilinear isometric embedding $f \colon E \to E_2$ and any elements $x, y \in E$, the embedding preserves addition, i.e., $f(x + y) = f(x) + f(y)$.

LinearIsometry.map_neg theorem

(x : E) : f (-x) = -f x

Full source

protected theorem map_neg (x : E) : f (-x) = -f x :=
  f.toLinearMap.map_neg x

Negation preservation under semilinear isometric embeddings

Informal description

For any semilinear isometric embedding $f \colon E \to E_2$ and any element $x \in E$, we have $f(-x) = -f(x)$.

LinearIsometry.map_sub theorem

(x y : E) : f (x - y) = f x - f y

Full source

protected theorem map_sub (x y : E) : f (x - y) = f x - f y :=
  f.toLinearMap.map_sub x y

Subtraction Preservation under Semilinear Isometric Embedding

Informal description

For any semilinear isometric embedding $f \colon E \to E_2$ between seminormed modules and any elements $x, y \in E$, the embedding preserves subtraction, i.e., $f(x - y) = f(x) - f(y)$.

LinearIsometry.map_smulₛₗ theorem

(c : R) (x : E) : f (c • x) = σ₁₂ c • f x

Full source

protected theorem map_smulₛₗ (c : R) (x : E) : f (c • x) = σ₁₂ c • f x :=
  f.toLinearMap.map_smulₛₗ c x

Scalar Multiplication Preservation under Semilinear Isometric Embedding

Informal description

Let $E$ and $E_2$ be seminormed modules over rings $R$ and $R_2$ respectively, and let $\sigma_{12} : R \to R_2$ be a ring homomorphism. For any semilinear isometric embedding $f : E \to E_2$ and any scalar $c \in R$ and vector $x \in E$, we have $f(c \cdot x) = \sigma_{12}(c) \cdot f(x)$.

LinearIsometry.map_smul theorem

[Module R E₂] (f : E →ₗᵢ[R] E₂) (c : R) (x : E) : f (c • x) = c • f x

Full source

protected theorem map_smul [Module R E₂] (f : E →ₗᵢ[R] E₂) (c : R) (x : E) : f (c • x) = c • f x :=
  f.toLinearMap.map_smul c x

Scalar Multiplication Preservation under Linear Isometric Embedding

Informal description

Let $E$ and $E_2$ be seminormed modules over a ring $R$, and let $f \colon E \to E_2$ be a linear isometric embedding. Then for any scalar $c \in R$ and any vector $x \in E$, we have $f(c \cdot x) = c \cdot f(x)$.

LinearIsometry.norm_map theorem

(x : E) : ‖f x‖ = ‖x‖

Full source

@[simp]
theorem norm_map (x : E) : ‖f x‖ = ‖x‖ :=
  SemilinearIsometryClass.norm_map f x

Norm Preservation under Semilinear Isometric Embedding

Informal description

For any semilinear isometric embedding $f \colon E \to E_2$ between seminormed modules and any element $x \in E$, the norm of $f(x)$ is equal to the norm of $x$, i.e., $\|f(x)\| = \|x\|$.

LinearIsometry.nnnorm_map theorem

(x : E) : ‖f x‖₊ = ‖x‖₊

Full source

@[simp] -- Should be replaced with `SemilinearIsometryClass.nnorm_map` when https://github.com/leanprover/lean4/issues/3107 is fixed.
theorem nnnorm_map (x : E) : ‖f x‖₊ = ‖x‖₊ :=
  NNReal.eq <| norm_map f x

Seminorm Preservation under Semilinear Isometric Embedding

Informal description

For any semilinear isometric embedding $f \colon E \to E_2$ between seminormed modules and any element $x \in E$, the seminorm of $f(x)$ is equal to the seminorm of $x$, i.e., $\|f(x)\|_+ = \|x\|_+$.

LinearIsometry.isometry theorem

: Isometry f

Full source

protected theorem isometry : Isometry f :=
  AddMonoidHomClass.isometry_of_norm f.toLinearMap (norm_map _)

Semilinear Isometric Embedding Preserves Distances

Informal description

For any semilinear isometric embedding $f \colon E \to E_2$ between seminormed modules, the map $f$ is an isometry, meaning it preserves distances: $d(f(x), f(y)) = d(x,y)$ for all $x, y \in E$.

LinearIsometry.isEmbedding theorem

(f : F →ₛₗᵢ[σ₁₂] E₂) : IsEmbedding f

Full source

lemma isEmbedding (f : F →ₛₗᵢ[σ₁₂] E₂) : IsEmbedding f := f.isometry.isEmbedding

Semilinear Isometric Embedding is an Embedding

Informal description

For any semilinear isometric embedding $f \colon F \to E_2$ between seminormed modules, the map $f$ is an embedding, meaning it is injective and its inverse is continuous on its image.

LinearIsometry.isComplete_image_iff theorem

[SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) {s : Set E} : IsComplete (f '' s) ↔ IsComplete s

Full source

theorem isComplete_image_iff [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) {s : Set E} :
    IsCompleteIsComplete (f '' s) ↔ IsComplete s :=
  _root_.isComplete_image_iff (SemilinearIsometryClass.isometry f).isUniformInducing

Image of Complete Set under Semilinear Isometry is Complete iff Original Set is Complete

Informal description

Let $E$ and $E₂$ be seminormed additive commutative groups equipped with module structures over semirings $R$ and $R₂$ respectively, and let $\sigma₁₂ : R \to R₂$ be a ring homomorphism. For any semilinear isometry $f : E \to E₂$ in the class `SemilinearIsometryClass`, and any subset $s \subseteq E$, the image $f(s)$ is a complete subset of $E₂$ if and only if $s$ is a complete subset of $E$.

LinearIsometry.isComplete_image_iff' theorem

(f : LinearIsometry σ₁₂ E E₂) {s : Set E} : IsComplete (f '' s) ↔ IsComplete s

Full source

@[simp] -- Should be replaced with `LinearIsometry.isComplete_image_iff` when https://github.com/leanprover/lean4/issues/3107 is fixed.
theorem isComplete_image_iff' (f : LinearIsometry σ₁₂ E E₂) {s : Set E} :
    IsCompleteIsComplete (f '' s) ↔ IsComplete s :=
  LinearIsometry.isComplete_image_iff _

Image Completeness under Semilinear Isometric Embedding

Informal description

Let $E$ and $E_2$ be seminormed additive commutative groups equipped with module structures over rings $R$ and $R_2$ respectively, and let $\sigma_{12} : R \to R_2$ be a ring homomorphism. For any $\sigma_{12}$-semilinear isometric embedding $f : E \to E_2$ and any subset $s \subseteq E$, the image $f(s)$ is a complete subset of $E_2$ if and only if $s$ is a complete subset of $E$.

LinearIsometry.isComplete_map_iff theorem

 [RingHomSurjective σ₁₂] {p : Submodule R E} : IsComplete (p.map f.toLinearMap : Set E₂) ↔ IsComplete (p : Set E)

Full source

theorem isComplete_map_iff [RingHomSurjective σ₁₂] {p : Submodule R E} :
    IsCompleteIsComplete (p.map f.toLinearMap : Set E₂) ↔ IsComplete (p : Set E) :=
  isComplete_image_iff f

Completeness of Submodule Image under Linear Isometry iff Submodule is Complete

Informal description

Let $E$ and $E₂$ be seminormed additive commutative groups equipped with module structures over rings $R$ and $R₂$ respectively, and let $\sigma₁₂ : R \to R₂$ be a surjective ring homomorphism. For any $\sigma₁₂$-linear isometry $f : E \to E₂$ and any submodule $p$ of $E$, the image $f(p)$ is a complete subset of $E₂$ if and only if $p$ is a complete subset of $E$.

LinearIsometry.isComplete_map_iff' theorem

 [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) [RingHomSurjective σ₁₂] {p : Submodule R E} :
  IsComplete (p.map f : Set E₂) ↔ IsComplete (p : Set E)

Full source

theorem isComplete_map_iff' [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) [RingHomSurjective σ₁₂]
    {p : Submodule R E} : IsCompleteIsComplete (p.map f : Set E₂) ↔ IsComplete (p : Set E) :=
  isComplete_image_iff f

Completeness Preservation under Semilinear Isometric Image of Submodules

Informal description

Let $E$ and $E_2$ be seminormed additive commutative groups equipped with module structures over semirings $R$ and $R_2$ respectively, and let $\sigma_{12} : R \to R_2$ be a ring homomorphism. For any semilinear isometry $f : E \to E_2$ in the class `SemilinearIsometryClass` that is surjective with respect to $\sigma_{12}$, and any submodule $p$ of $E$, the image $f(p)$ is a complete subset of $E_2$ if and only if $p$ is a complete subset of $E$.

LinearIsometry.completeSpace_map instance

 [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) [RingHomSurjective σ₁₂] (p : Submodule R E) [CompleteSpace p] :
  CompleteSpace (p.map f)

Full source

instance completeSpace_map [SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) [RingHomSurjective σ₁₂]
    (p : Submodule R E) [CompleteSpace p] : CompleteSpace (p.map f) :=
  ((isComplete_map_iff' f).2 <| completeSpace_coe_iff_isComplete.1 ‹_›).completeSpace_coe

Completeness Preservation under Semilinear Isometric Image of Complete Submodules

Informal description

Let $E$ and $E_2$ be seminormed additive commutative groups with module structures over semirings $R$ and $R_2$ respectively, and let $\sigma_{12} : R \to R_2$ be a ring homomorphism. For any semilinear isometry $f : E \to E_2$ in the class `SemilinearIsometryClass` that is surjective with respect to $\sigma_{12}$, and any complete submodule $p$ of $E$, the image $f(p)$ is also a complete space.

LinearIsometry.completeSpace_map' instance

[RingHomSurjective σ₁₂] (p : Submodule R E) [CompleteSpace p] : CompleteSpace (p.map f.toLinearMap)

Full source

instance completeSpace_map' [RingHomSurjective σ₁₂] (p : Submodule R E) [CompleteSpace p] :
    CompleteSpace (p.map f.toLinearMap) :=
  (f.isComplete_map_iff.2 <| completeSpace_coe_iff_isComplete.1 ‹_›).completeSpace_coe

Completeness Preservation under Linear Isometric Image of Complete Submodules

Informal description

Let $E$ and $E_2$ be seminormed additive commutative groups with module structures over rings $R$ and $R_2$ respectively, and let $\sigma_{12} : R \to R_2$ be a ring homomorphism. For any $\sigma_{12}$-linear isometry $f : E \to E_2$ that is surjective with respect to $\sigma_{12}$, and any complete submodule $p$ of $E$, the image $f(p)$ is also a complete space.

LinearIsometry.dist_map theorem

(x y : E) : dist (f x) (f y) = dist x y

Full source

@[simp]
theorem dist_map (x y : E) : dist (f x) (f y) = dist x y :=
  f.isometry.dist_eq x y

Distance Preservation under Semilinear Isometric Embedding

Informal description

For any semilinear isometric embedding $f \colon E \to E_2$ between seminormed modules and any two points $x, y \in E$, the distance between their images $f(x)$ and $f(y)$ is equal to the distance between $x$ and $y$, i.e., $d(f(x), f(y)) = d(x, y)$.

LinearIsometry.edist_map theorem

(x y : E) : edist (f x) (f y) = edist x y

Full source

@[simp]
theorem edist_map (x y : E) : edist (f x) (f y) = edist x y :=
  f.isometry.edist_eq x y

Preservation of Extended Distance under Semilinear Isometric Embedding

Informal description

For any semilinear isometric embedding $f \colon E \to E_2$ between seminormed modules and any two elements $x, y \in E$, the extended distance between $f(x)$ and $f(y)$ equals the extended distance between $x$ and $y$, i.e., $\text{edist}(f(x), f(y)) = \text{edist}(x, y)$.

LinearIsometry.injective theorem

: Injective f₁

Full source

protected theorem injective : Injective f₁ :=
  Isometry.injective (LinearIsometry.isometry f₁)

Injectivity of Semilinear Isometric Embeddings

Informal description

Every semilinear isometric embedding $f_1 \colon E \to E_2$ between seminormed modules is injective, meaning that for any $x, y \in E$, if $f_1(x) = f_1(y)$, then $x = y$.

LinearIsometry.map_eq_iff theorem

{x y : F} : f₁ x = f₁ y ↔ x = y

Full source

@[simp]
theorem map_eq_iff {x y : F} : f₁ x = f₁ y ↔ x = y :=
  f₁.injective.eq_iff

Injectivity Criterion for Semilinear Isometric Embeddings: $ f_1(x) = f_1(y) \leftrightarrow x = y $

Informal description

For any semilinear isometric embedding $ f_1 \colon F \to F_2 $ between seminormed modules and any two elements $ x, y \in F $, the images $ f_1(x) $ and $ f_1(y) $ are equal if and only if $ x $ and $ y $ are equal, i.e., $ f_1(x) = f_1(y) \leftrightarrow x = y $.

LinearIsometry.map_ne theorem

{x y : F} (h : x ≠ y) : f₁ x ≠ f₁ y

Full source

theorem map_ne {x y : F} (h : x ≠ y) : f₁ x ≠ f₁ y :=
  f₁.injective.ne h

Semilinear Isometric Embeddings Preserve Inequality ($x \neq y \Rightarrow f(x) \neq f(y)$)

Informal description

For any semilinear isometric embedding $f_1 \colon E \to E_2$ between seminormed modules and any distinct elements $x, y \in E$ (i.e., $x \neq y$), the images $f_1(x)$ and $f_1(y)$ are also distinct.

LinearIsometry.lipschitz theorem

: LipschitzWith 1 f

Full source

protected theorem lipschitz : LipschitzWith 1 f :=
  f.isometry.lipschitz

Lipschitz Continuity of Semilinear Isometric Embeddings with Constant 1

Informal description

For any semilinear isometric embedding $f \colon E \to E_2$ between seminormed modules, the map $f$ is Lipschitz continuous with constant $1$, i.e., for all $x, y \in E$, we have $\|f(x) - f(y)\| \leq \|x - y\|$.

LinearIsometry.antilipschitz theorem

: AntilipschitzWith 1 f

Full source

protected theorem antilipschitz : AntilipschitzWith 1 f :=
  f.isometry.antilipschitz

Semilinear Isometric Embedding is 1-Antilipschitz

Informal description

A semilinear isometric embedding $f \colon E \to E_2$ between seminormed modules is antilipschitz with constant 1, meaning that for all $x, y \in E$, we have $\|x - y\| \leq \|f(x) - f(y)\|$.

LinearIsometry.continuous theorem

: Continuous f

Full source

@[continuity]
protected theorem continuous : Continuous f :=
  f.isometry.continuous

Continuity of Semilinear Isometric Embeddings

Informal description

Every semilinear isometric embedding $f \colon E \to E_2$ between seminormed modules is continuous.

LinearIsometry.preimage_ball theorem

(x : E) (r : ℝ) : f ⁻¹' Metric.ball (f x) r = Metric.ball x r

Full source

@[simp]
theorem preimage_ball (x : E) (r : ℝ) : f ⁻¹' Metric.ball (f x) r = Metric.ball x r :=
  f.isometry.preimage_ball x r

Preimage of Open Ball under Semilinear Isometric Embedding Equals Open Ball

Informal description

For any semilinear isometric embedding $f \colon E \to E_2$ between seminormed modules, any point $x \in E$, and any radius $r \in \mathbb{R}$, the preimage of the open ball centered at $f(x)$ with radius $r$ under $f$ is equal to the open ball centered at $x$ with radius $r$ in $E$. That is, $$ f^{-1}(B(f(x), r)) = B(x, r). $$

LinearIsometry.preimage_sphere theorem

(x : E) (r : ℝ) : f ⁻¹' Metric.sphere (f x) r = Metric.sphere x r

Full source

@[simp]
theorem preimage_sphere (x : E) (r : ℝ) : f ⁻¹' Metric.sphere (f x) r = Metric.sphere x r :=
  f.isometry.preimage_sphere x r

Preimage of Sphere under Semilinear Isometric Embedding

Informal description

Let $f \colon E \to E_2$ be a semilinear isometric embedding between seminormed modules. For any point $x \in E$ and radius $r \in \mathbb{R}$, the preimage under $f$ of the sphere centered at $f(x)$ with radius $r$ is equal to the sphere centered at $x$ with radius $r$, i.e., $$ f^{-1}(\{y \in E_2 \mid \|y - f(x)\| = r\}) = \{z \in E \mid \|z - x\| = r\}. $$

LinearIsometry.preimage_closedBall theorem

(x : E) (r : ℝ) : f ⁻¹' Metric.closedBall (f x) r = Metric.closedBall x r

Full source

@[simp]
theorem preimage_closedBall (x : E) (r : ℝ) :
    f ⁻¹' Metric.closedBall (f x) r = Metric.closedBall x r :=
  f.isometry.preimage_closedBall x r

Preimage of Closed Ball under Semilinear Isometric Embedding Equals Closed Ball

Informal description

Let $E$ and $E_2$ be seminormed modules over rings $R$ and $R_2$ respectively, and let $f \colon E \to E_2$ be a semilinear isometric embedding. For any $x \in E$ and radius $r \in \mathbb{R}$, the preimage under $f$ of the closed ball centered at $f(x)$ with radius $r$ is equal to the closed ball centered at $x$ with radius $r$. In symbols: $$ f^{-1}\big(\overline{B}(f(x), r)\big) = \overline{B}(x, r). $$

LinearIsometry.ediam_image theorem

(s : Set E) : EMetric.diam (f '' s) = EMetric.diam s

Full source

theorem ediam_image (s : Set E) : EMetric.diam (f '' s) = EMetric.diam s :=
  f.isometry.ediam_image s

Preservation of Extended Metric Diameter under Semilinear Isometric Embedding

Informal description

For any semilinear isometric embedding $f \colon E \to E_2$ between seminormed modules and any subset $s \subseteq E$, the extended metric diameter of the image $f(s)$ is equal to the extended metric diameter of $s$, i.e., $\text{diam}(f(s)) = \text{diam}(s)$.

LinearIsometry.ediam_range theorem

: EMetric.diam (range f) = EMetric.diam (univ : Set E)

Full source

theorem ediam_range : EMetric.diam (range f) = EMetric.diam (univ : Set E) :=
  f.isometry.ediam_range

Extended Diameter of Range Equals Extended Diameter of Domain for Semilinear Isometric Embeddings

Informal description

For a semilinear isometric embedding $f \colon E \to E_2$ between seminormed modules, the extended diameter of the range of $f$ is equal to the extended diameter of the entire space $E$. That is, $\text{diam}(\text{range}\, f) = \text{diam}(E)$.

LinearIsometry.diam_image theorem

(s : Set E) : Metric.diam (f '' s) = Metric.diam s

Full source

theorem diam_image (s : Set E) : Metric.diam (f '' s) = Metric.diam s :=
  Isometry.diam_image (LinearIsometry.isometry f) s

Preservation of Metric Diameter under Semilinear Isometric Embedding

Informal description

For any semilinear isometric embedding $f \colon E \to E_2$ between seminormed modules and any subset $s \subseteq E$, the metric diameter of the image $f(s)$ is equal to the metric diameter of $s$, i.e., $\text{diam}(f(s)) = \text{diam}(s)$.

LinearIsometry.diam_range theorem

: Metric.diam (range f) = Metric.diam (univ : Set E)

Full source

theorem diam_range : Metric.diam (range f) = Metric.diam (univ : Set E) :=
  Isometry.diam_range (LinearIsometry.isometry f)

Diameter Preservation under Semilinear Isometric Embedding

Informal description

For a semilinear isometric embedding $f \colon E \to E_2$ between seminormed modules, the diameter of the range of $f$ is equal to the diameter of the entire space $E$. That is, $\text{diam}(\text{range}\, f) = \text{diam}(E)$.

LinearIsometry.toContinuousLinearMap definition

: E →SL[σ₁₂] E₂

Full source

/-- Interpret a linear isometry as a continuous linear map. -/
def toContinuousLinearMap : E →SL[σ₁₂] E₂ :=
  ⟨f.toLinearMap, f.continuous⟩

Continuous linear map induced by a linear isometry

Informal description

The function converts a linear isometry $f \colon E \to E_2$ (which preserves norms) into a continuous linear map between the seminormed modules $E$ and $E_2$ over the rings $R$ and $R_2$ respectively, where the ring homomorphism $\sigma_{12} \colon R \to R_2$ governs the semilinearity.

LinearIsometry.toContinuousLinearMap_injective theorem

: Function.Injective (toContinuousLinearMap : _ → E →SL[σ₁₂] E₂)

Full source

theorem toContinuousLinearMap_injective :
    Function.Injective (toContinuousLinearMap : _ → E →SL[σ₁₂] E₂) := fun x _ h =>
  coe_injective (congr_arg _ h : ⇑x.toContinuousLinearMap = _)

Injectivity of the Continuous Linear Map Induced by a Semilinear Isometric Embedding

Informal description

The map that converts a semilinear isometric embedding $f \colon E \to E_2$ to its corresponding continuous linear map is injective. That is, if two semilinear isometric embeddings induce the same continuous linear map, then they must be equal.

LinearIsometry.toContinuousLinearMap_inj theorem

{f g : E →ₛₗᵢ[σ₁₂] E₂} : f.toContinuousLinearMap = g.toContinuousLinearMap ↔ f = g

Full source

@[simp]
theorem toContinuousLinearMap_inj {f g : E →ₛₗᵢ[σ₁₂] E₂} :
    f.toContinuousLinearMap = g.toContinuousLinearMap ↔ f = g :=
  toContinuousLinearMap_injective.eq_iff

Equality of Semilinear Isometric Embeddings via Induced Continuous Linear Maps

Informal description

For any two semilinear isometric embeddings $f, g \colon E \to E_2$, the induced continuous linear maps are equal if and only if $f$ and $g$ are equal as functions. That is, $f_{\text{CLM}} = g_{\text{CLM}} \leftrightarrow f = g$, where $f_{\text{CLM}}$ and $g_{\text{CLM}}$ denote the continuous linear maps induced by $f$ and $g$ respectively.

LinearIsometry.coe_toContinuousLinearMap theorem

: ⇑f.toContinuousLinearMap = f

Full source

@[simp]
theorem coe_toContinuousLinearMap : ⇑f.toContinuousLinearMap = f :=
  rfl

Equality of Underlying Functions for Induced Continuous Linear Map

Informal description

For any semilinear isometric embedding $f \colon E \to E_2$, the underlying function of the continuous linear map induced by $f$ is equal to $f$ itself.

LinearIsometry.comp_continuous_iff theorem

{α : Type*} [TopologicalSpace α] {g : α → E} : Continuous (f ∘ g) ↔ Continuous g

Full source

@[simp]
theorem comp_continuous_iff {α : Type*} [TopologicalSpace α] {g : α → E} :
    ContinuousContinuous (f ∘ g) ↔ Continuous g :=
  f.isometry.comp_continuous_iff

Continuity of Composition with Semilinear Isometric Embedding

Informal description

Let $E$ and $E_2$ be seminormed modules over rings $R$ and $R_2$ respectively, with $\sigma_{12} \colon R \to R_2$ a ring homomorphism. For any semilinear isometric embedding $f \colon E \to E_2$ and any topological space $\alpha$, a function $g \colon \alpha \to E$ satisfies that the composition $f \circ g$ is continuous if and only if $g$ itself is continuous.

LinearIsometry.id definition

: E →ₗᵢ[R] E

Full source

/-- The identity linear isometry. -/
def id : E →ₗᵢ[R] E :=
  ⟨LinearMap.id, fun _ => rfl⟩

Identity linear isometry

Informal description

The identity linear isometry on a seminormed module $E$ over a ring $R$, which is a linear map preserving the norm: $\|\text{id}(x)\| = \|x\|$ for all $x \in E$.

LinearIsometry.coe_id theorem

: ((id : E →ₗᵢ[R] E) : E → E) = _root_.id

Full source

@[simp, norm_cast]
theorem coe_id : ((id : E →ₗᵢ[R] E) : E → E) = _root_.id :=
  rfl

Identity Linear Isometry as Identity Function

Informal description

The underlying function of the identity linear isometry on a seminormed module $E$ over a ring $R$ is equal to the identity function on $E$, i.e., $\text{id}(x) = x$ for all $x \in E$.

LinearIsometry.id_apply theorem

(x : E) : (id : E →ₗᵢ[R] E) x = x

Full source

@[simp]
theorem id_apply (x : E) : (id : E →ₗᵢ[R] E) x = x :=
  rfl

Identity Linear Isometry Acts as Identity Function

Informal description

For any element $x$ in a seminormed module $E$ over a ring $R$, the identity linear isometry $\text{id}$ satisfies $\text{id}(x) = x$.

LinearIsometry.id_toLinearMap theorem

: (id.toLinearMap : E →ₗ[R] E) = LinearMap.id

Full source

@[simp]
theorem id_toLinearMap : (id.toLinearMap : E →ₗ[R] E) = LinearMap.id :=
  rfl

Identity Linear Isometry's Underlying Map is Identity

Informal description

The underlying linear map of the identity linear isometry on a seminormed module $E$ over a ring $R$ is equal to the identity linear map on $E$.

LinearIsometry.id_toContinuousLinearMap theorem

: id.toContinuousLinearMap = ContinuousLinearMap.id R E

Full source

@[simp]
theorem id_toContinuousLinearMap : id.toContinuousLinearMap = ContinuousLinearMap.id R E :=
  rfl

Identity Linear Isometry Yields Identity Continuous Linear Map

Informal description

The continuous linear map induced by the identity linear isometry on a seminormed module $E$ over a ring $R$ is equal to the identity continuous linear map on $E$.

LinearIsometry.instInhabited instance

: Inhabited (E →ₗᵢ[R] E)

Full source

instance instInhabited : Inhabited (E →ₗᵢ[R] E) := ⟨id⟩

Inhabited Type of Linear Isometries on a Seminormed Module

Informal description

For any seminormed module $E$ over a ring $R$, the type of linear isometries from $E$ to itself is inhabited. In particular, the identity linear isometry serves as a canonical inhabitant.

LinearIsometry.comp definition

(g : E₂ →ₛₗᵢ[σ₂₃] E₃) (f : E →ₛₗᵢ[σ₁₂] E₂) : E →ₛₗᵢ[σ₁₃] E₃

Full source

/-- Composition of linear isometries. -/
def comp (g : E₂ →ₛₗᵢ[σ₂₃] E₃) (f : E →ₛₗᵢ[σ₁₂] E₂) : E →ₛₗᵢ[σ₁₃] E₃ :=
  ⟨g.toLinearMap.comp f.toLinearMap, fun _ => (norm_map g _).trans (norm_map f _)⟩

Composition of semilinear isometric embeddings

Informal description

The composition of two semilinear isometric embeddings $ g : E_2 \to E_3 $ and $ f : E \to E_2 $ is a semilinear isometric embedding $ g \circ f : E \to E_3 $, where the composition preserves the norm: $\|g(f(x))\| = \|x\|$ for all $x \in E$.

LinearIsometry.coe_comp theorem

(g : E₂ →ₛₗᵢ[σ₂₃] E₃) (f : E →ₛₗᵢ[σ₁₂] E₂) : ⇑(g.comp f) = g ∘ f

Full source

@[simp]
theorem coe_comp (g : E₂ →ₛₗᵢ[σ₂₃] E₃) (f : E →ₛₗᵢ[σ₁₂] E₂) : ⇑(g.comp f) = g ∘ f :=
  rfl

Composition of Semilinear Isometries Preserves Function Application

Informal description

For any semilinear isometric embeddings $g : E_2 \to E_3$ and $f : E \to E_2$, the underlying function of their composition $g \circ f$ is equal to the composition of their underlying functions, i.e., $(g \circ f)(x) = g(f(x))$ for all $x \in E$.

LinearIsometry.id_comp theorem

: (id : E₂ →ₗᵢ[R₂] E₂).comp f = f

Full source

@[simp]
theorem id_comp : (id : E₂ →ₗᵢ[R₂] E₂).comp f = f :=
  ext fun _ => rfl

Identity Isometry Composition Law: $\text{id} \circ f = f$

Informal description

For any semilinear isometric embedding $f \colon E \to E_2$ between seminormed modules over rings $R$ and $R_2$ respectively, the composition of the identity isometry on $E_2$ with $f$ equals $f$ itself, i.e., $\text{id}_{E_2} \circ f = f$.

LinearIsometry.comp_id theorem

: f.comp id = f

Full source

@[simp]
theorem comp_id : f.comp id = f :=
  ext fun _ => rfl

Right Identity Law for Composition of Semilinear Isometries

Informal description

For any semilinear isometric embedding $f \colon E \to E_2$, the composition of $f$ with the identity isometry on $E$ is equal to $f$ itself, i.e., $f \circ \text{id} = f$.

LinearIsometry.comp_assoc theorem

 (f : E₃ →ₛₗᵢ[σ₃₄] E₄) (g : E₂ →ₛₗᵢ[σ₂₃] E₃) (h : E →ₛₗᵢ[σ₁₂] E₂) : (f.comp g).comp h = f.comp (g.comp h)

Full source

theorem comp_assoc (f : E₃ →ₛₗᵢ[σ₃₄] E₄) (g : E₂ →ₛₗᵢ[σ₂₃] E₃) (h : E →ₛₗᵢ[σ₁₂] E₂) :
    (f.comp g).comp h = f.comp (g.comp h) :=
  rfl

Associativity of Composition for Semilinear Isometric Embeddings

Informal description

For semilinear isometric embeddings $f \colon E_3 \to E_4$, $g \colon E_2 \to E_3$, and $h \colon E \to E_2$, the composition operation satisfies the associativity property $(f \circ g) \circ h = f \circ (g \circ h)$.

LinearIsometry.instMonoid instance

: Monoid (E →ₗᵢ[R] E)

Full source

instance instMonoid : Monoid (E →ₗᵢ[R] E) where
  one := id
  mul := comp
  mul_assoc := comp_assoc
  one_mul := id_comp
  mul_one := comp_id

Monoid Structure on Linear Isometries of a Seminormed Module

Informal description

The set of linear isometries from a seminormed module $E$ to itself forms a monoid under composition, where the identity isometry serves as the identity element.

LinearIsometry.coe_one theorem

: ((1 : E →ₗᵢ[R] E) : E → E) = _root_.id

Full source

@[simp]
theorem coe_one : ((1 : E →ₗᵢ[R] E) : E → E) = _root_.id :=
  rfl

Identity Linear Isometry Equals Identity Function

Informal description

The identity linear isometry $1 \colon E \to_{L^1[R]} E$ on a seminormed module $E$ over a ring $R$ is equal to the identity function $\text{id} \colon E \to E$.

LinearIsometry.coe_mul theorem

(f g : E →ₗᵢ[R] E) : ⇑(f * g) = f ∘ g

Full source

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

Composition of Linear Isometries as Function Composition

Informal description

For any two linear isometries $f, g : E \to_{R} E$ on a seminormed module $E$ over a ring $R$, the underlying function of their composition $f * g$ is equal to the function composition $f \circ g$.

LinearIsometry.one_def theorem

: (1 : E →ₗᵢ[R] E) = id

Full source

theorem one_def : (1 : E →ₗᵢ[R] E) = id :=
  rfl

Identity Element in Monoid of Linear Isometries is the Identity Map

Informal description

The multiplicative identity element in the monoid of linear isometries from a seminormed module $E$ to itself over a ring $R$ is equal to the identity linear isometry $\text{id}$.

LinearIsometry.mul_def theorem

(f g : E →ₗᵢ[R] E) : (f * g : E →ₗᵢ[R] E) = f.comp g

Full source

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

Product of Linear Isometries as Composition

Informal description

For any two linear isometries $f, g \colon E \to E$ on a seminormed module $E$ over a ring $R$, the product $f * g$ in the monoid of linear isometries is equal to the composition $f \circ g$.

LinearIsometry.coe_pow theorem

(f : E →ₗᵢ[R] E) (n : ℕ) : ⇑(f ^ n) = f^[n]

Full source

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

Iteration of Linear Isometry via Monoid Power: $f^n = f^{[n]}$

Informal description

For any linear isometry $f \colon E \to E$ on a seminormed module $E$ over a ring $R$ and any natural number $n$, the $n$-th power of $f$ in the monoid of linear isometries is equal to the $n$-th iterate of $f$, i.e., $f^n = f^{[n]}$.

LinearMap.toLinearIsometry definition

(f : E →ₛₗ[σ₁₂] E₂) (hf : Isometry f) : E →ₛₗᵢ[σ₁₂] E₂

Full source

/-- Construct a `LinearIsometry` from a `LinearMap` satisfying `Isometry`. -/
def LinearMap.toLinearIsometry (f : E →ₛₗ[σ₁₂] E₂) (hf : Isometry f) : E →ₛₗᵢ[σ₁₂] E₂ :=
  { f with
    norm_map' := by
      simp_rw [← dist_zero_right]
      simpa using (hf.dist_eq · 0) }

Construction of a semilinear isometric embedding from an isometric semilinear map

Informal description

Given a $\sigma_{12}$-semilinear map $f \colon E \to E_2$ between seminormed modules that is also an isometry (i.e., preserves distances), this definition constructs a $\sigma_{12}$-semilinear isometric embedding from $f$. The resulting map satisfies $\|f(x)\| = \|x\|$ for all $x \in E$.

Submodule.subtypeₗᵢ definition

: p →ₗᵢ[R'] E

Full source

/-- `Submodule.subtype` as a `LinearIsometry`. -/
def subtypeₗᵢ : p →ₗᵢ[R'] E :=
  ⟨p.subtype, fun _ => rfl⟩

Linear isometric inclusion of a submodule

Informal description

The canonical inclusion map of a submodule $p$ into its ambient seminormed module $E$ as a linear isometry. This map preserves the norm: $\|\text{subtype}_{\mathcal{l}i}(x)\| = \|x\|$ for all $x \in p$.

Submodule.coe_subtypeₗᵢ theorem

: ⇑p.subtypeₗᵢ = p.subtype

Full source

@[simp]
theorem coe_subtypeₗᵢ : ⇑p.subtypeₗᵢ = p.subtype :=
  rfl

Linear isometric inclusion coincides with canonical inclusion

Informal description

The underlying function of the linear isometric inclusion map from a submodule $p$ to its ambient seminormed module $E$ is equal to the canonical subtype map from $p$ to $E$.

Submodule.subtypeₗᵢ_toLinearMap theorem

: p.subtypeₗᵢ.toLinearMap = p.subtype

Full source

@[simp]
theorem subtypeₗᵢ_toLinearMap : p.subtypeₗᵢ.toLinearMap = p.subtype :=
  rfl

Linear isometric inclusion as linear map equals canonical inclusion

Informal description

The underlying linear map of the linear isometric inclusion $\text{subtype}_{\mathcal{l}i}$ from a submodule $p$ into its ambient seminormed module $E$ coincides with the canonical linear inclusion map $p.\text{subtype}$.

Submodule.subtypeₗᵢ_toContinuousLinearMap theorem

: p.subtypeₗᵢ.toContinuousLinearMap = p.subtypeL

Full source

@[simp]
theorem subtypeₗᵢ_toContinuousLinearMap : p.subtypeₗᵢ.toContinuousLinearMap = p.subtypeL :=
  rfl

Continuous linear map of isometric inclusion equals canonical inclusion

Informal description

The continuous linear map induced by the linear isometric inclusion of a submodule $p$ into its ambient seminormed module $E$ is equal to the canonical continuous linear inclusion map $p.\text{subtypeL}$.

LinearIsometryEquiv structure

(σ₁₂ : R →+* R₂) {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁]
  [RingHomInvPair σ₂₁ σ₁₂] (E E₂ : Type*) [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂]
  [Module R E] [Module R₂ E₂] extends E ≃ₛₗ[σ₁₂] E₂

Full source

/-- A semilinear isometric equivalence between two normed vector spaces,
denoted as `f : E ≃ₛₗᵢ[σ₁₂] E₂`. -/
structure LinearIsometryEquiv (σ₁₂ : R →+* R₂) {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁]
  [RingHomInvPair σ₂₁ σ₁₂] (E E₂ : Type*) [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂]
  [Module R E] [Module R₂ E₂] extends E ≃ₛₗ[σ₁₂] E₂ where
  norm_map' : ∀ x, ‖toLinearEquiv x‖ = ‖x‖

Semilinear Isometric Equivalence

Informal description

A semilinear isometric equivalence between two normed vector spaces $E$ and $E₂$ over rings $R$ and $R₂$ respectively, denoted as $f : E \simeq_{σ₁₂} E₂$, is a bijective semilinear map that preserves the norm. Here, $σ₁₂ : R \to R₂$ is a ring homomorphism, and there exists an inverse ring homomorphism $σ₂₁ : R₂ \to R$ such that $σ₁₂$ and $σ₂₁$ form a pair of mutually inverse ring homomorphisms. The spaces $E$ and $E₂$ are equipped with seminormed additive commutative group structures and module structures over $R$ and $R₂$ respectively.

term_≃ₛₗᵢ[_]_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
notation:25 E " ≃ₛₗᵢ[" σ₁₂:25 "] " E₂:0 => LinearIsometryEquiv σ₁₂ E E₂

Semilinear isometric equivalence notation

Informal description

The notation `E ≃ₛₗᵢ[σ₁₂] E₂` represents a semilinear isometric equivalence between the seminormed additive commutative groups `E` and `E₂`, where `σ₁₂` is a ring homomorphism that defines the semilinearity. This is a bundled version of a bijective semilinear map that preserves the norm.

term_≃ₗᵢ[_]_ definition

: Lean.TrailingParserDescr✝

Full source

/-- A linear isometric equivalence between two normed vector spaces. -/
notation:25 E " ≃ₗᵢ[" R:25 "] " E₂:0 => LinearIsometryEquiv (RingHom.id R) E E₂

Linear isometric equivalence notation

Informal description

The notation $ E \simeq_{l i}[R] E_2 $ represents a linear isometric equivalence between two normed vector spaces $ E $ and $ E_2 $ over the ring $ R $. This means it is a linear isomorphism that preserves the norm, i.e., for any $ x \in E $, the norm of $ x $ in $ E $ is equal to the norm of its image in $ E_2 $.

term_≃ₗᵢ⋆[_]_ definition

: Lean.TrailingParserDescr✝

Full source

/-- An antilinear isometric equivalence between two normed vector spaces. -/
notation:25 E " ≃ₗᵢ⋆[" R:25 "] " E₂:0 => LinearIsometryEquiv (starRingEnd R) E E₂

Antilinear isometric equivalence

Informal description

The notation $ E \simeq_{L^i\star}[R] E_2 $ represents an antilinear isometric equivalence between two normed vector spaces $ E $ and $ E_2 $ over the field $ R $. This means it is a bijective map that preserves the norm and is antilinear with respect to the field automorphism given by the star operation on $ R $.

SemilinearIsometryEquivClass structure

(𝓕 : Type*) {R R₂ : outParam Type*} [Semiring R]
  [Semiring R₂] (σ₁₂ : outParam <| R →+* R₂) {σ₂₁ : outParam <| R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁]
  [RingHomInvPair σ₂₁ σ₁₂] (E E₂ : outParam Type*) [SeminormedAddCommGroup E]
  [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] [EquivLike 𝓕 E E₂] : Prop
  extends SemilinearEquivClass 𝓕 σ₁₂ E E₂

Full source

/-- `SemilinearIsometryEquivClass F σ E E₂` asserts `F` is a type of bundled `σ`-semilinear
isometric equivs `E → E₂`.

See also `LinearIsometryEquivClass F R E E₂` 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 SemilinearIsometryEquivClass (𝓕 : Type*) {R R₂ : outParam Type*} [Semiring R]
  [Semiring R₂] (σ₁₂ : outParam <| R →+* R₂) {σ₂₁ : outParam <| R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁]
  [RingHomInvPair σ₂₁ σ₁₂] (E E₂ : outParam Type*) [SeminormedAddCommGroup E]
  [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] [EquivLike 𝓕 E E₂] : Prop
  extends SemilinearEquivClass 𝓕 σ₁₂ E E₂ where
  norm_map : ∀ (f : 𝓕) (x : E), ‖f x‖ = ‖x‖

Class of Semilinear Isometric Equivalences

Informal description

The class `SemilinearIsometryEquivClass 𝓕 σ₁₂ E E₂` asserts that `𝓕` is a type of bundled `σ₁₂`-semilinear isometric equivalences between the seminormed additive commutative groups `E` and `E₂`, where `σ₁₂ : R →+* R₂` is a ring homomorphism between semirings `R` and `R₂`. An element `f : 𝓕` is a bijective map `f : E → E₂` that satisfies: 1. **Semilinearity**: `f (x + y) = f x + f y` and `f (c • x) = (σ₁₂ c) • f x` for all `x, y ∈ E` and `c ∈ R`. 2. **Isometry**: `‖f x‖ = ‖x‖` for all `x ∈ E`. This class extends `SemilinearEquivClass` and requires the existence of an inverse ring homomorphism `σ₂₁ : R₂ →+* R` such that `σ₁₂` and `σ₂₁` form a ring homomorphism inverse pair.

LinearIsometryEquivClass abbrev

 (𝓕 : Type*) (R E E₂ : outParam Type*) [Semiring R] [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E]
  [Module R E₂] [EquivLike 𝓕 E E₂]

Full source

/-- `LinearIsometryEquivClass F R E E₂` asserts `F` is a type of bundled `R`-linear isometries
`M → M₂`.

This is an abbreviation for `SemilinearIsometryEquivClass F (RingHom.id R) E E₂`.
-/
abbrev LinearIsometryEquivClass (𝓕 : Type*) (R E E₂ : outParam Type*) [Semiring R]
    [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R E₂]
    [EquivLike 𝓕 E E₂] :=
  SemilinearIsometryEquivClass 𝓕 (RingHom.id R) E E₂

Class of Linear Isometric Equivalences

Informal description

The class `LinearIsometryEquivClass 𝓕 R E E₂` asserts that `𝓕` is a type of bundled `R`-linear isometric equivalences between the seminormed additive commutative groups `E` and `E₂`, where `R` is a semiring. An element `f : 𝓕` is a bijective map `f : E → E₂` that satisfies: 1. **Linearity**: `f (x + y) = f x + f y` and `f (c • x) = c • f x` for all `x, y ∈ E` and `c ∈ R`. 2. **Isometry**: `‖f x‖ = ‖x‖` for all `x ∈ E`. This class extends `EquivLike` and requires that `E` and `E₂` are modules over `R`.

SemilinearIsometryEquivClass.toSemilinearIsometryClass instance

 [EquivLike 𝓕 E E₂] [s : SemilinearIsometryEquivClass 𝓕 σ₁₂ E E₂] : SemilinearIsometryClass 𝓕 σ₁₂ E E₂

Full source

instance (priority := 100) toSemilinearIsometryClass [EquivLike 𝓕 E E₂]
    [s : SemilinearIsometryEquivClass 𝓕 σ₁₂ E E₂] : SemilinearIsometryClass 𝓕 σ₁₂ E E₂ :=
  { s with }

Semilinear Isometric Equivalences are Semilinear Isometries

Informal description

For any type `𝓕` that is a semilinear isometric equivalence class between seminormed additive commutative groups `E` and `E₂` with respect to a ring homomorphism `σ₁₂`, every element of `𝓕` is also a semilinear isometry. More precisely, if `𝓕` is equipped with an `EquivLike` structure and satisfies `SemilinearIsometryEquivClass 𝓕 σ₁₂ E E₂`, then it automatically satisfies `SemilinearIsometryClass 𝓕 σ₁₂ E E₂`. This means every `f : 𝓕` preserves addition (`f (x + y) = f x + f y`), scalar multiplication (`f (c • x) = (σ₁₂ c) • f x`), and the norm (`‖f x‖ = ‖x‖`).

LinearIsometryEquiv.toLinearEquiv_injective theorem

: Injective (toLinearEquiv : (E ≃ₛₗᵢ[σ₁₂] E₂) → E ≃ₛₗ[σ₁₂] E₂)

Full source

theorem toLinearEquiv_injective : Injective (toLinearEquiv : (E ≃ₛₗᵢ[σ₁₂] E₂) → E ≃ₛₗ[σ₁₂] E₂)
  | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl

Injectivity of the Underlying Semilinear Equivalence Map for Semilinear Isometric Equivalences

Informal description

The function that maps a semilinear isometric equivalence $f : E \simeq_{σ₁₂} E₂$ to its underlying semilinear equivalence is injective. In other words, if two semilinear isometric equivalences $f$ and $g$ have the same underlying semilinear equivalence, then $f = g$.

LinearIsometryEquiv.toLinearEquiv_inj theorem

{f g : E ≃ₛₗᵢ[σ₁₂] E₂} : f.toLinearEquiv = g.toLinearEquiv ↔ f = g

Full source

@[simp]
theorem toLinearEquiv_inj {f g : E ≃ₛₗᵢ[σ₁₂] E₂} : f.toLinearEquiv = g.toLinearEquiv ↔ f = g :=
  toLinearEquiv_injective.eq_iff

Equality of Semilinear Isometric Equivalences via Underlying Semilinear Equivalences

Informal description

For any two semilinear isometric equivalences $f, g : E \simeq_{σ₁₂} E₂$ between seminormed additive commutative groups $E$ and $E₂$, the underlying semilinear equivalences of $f$ and $g$ are equal if and only if $f$ and $g$ are equal.

LinearIsometryEquiv.instEquivLike instance

: EquivLike (E ≃ₛₗᵢ[σ₁₂] E₂) E E₂

Full source

instance instEquivLike : EquivLike (E ≃ₛₗᵢ[σ₁₂] E₂) E E₂ where
  coe e := e.toFun
  inv e := e.invFun
  coe_injective' f g h₁ h₂ := by
    obtain ⟨f', _⟩ := f
    obtain ⟨g', _⟩ := g
    cases f'
    cases g'
    simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, DFunLike.coe_fn_eq] at h₁
    congr
  left_inv e := e.left_inv
  right_inv e := e.right_inv

Equivalence-like Structure of Semilinear Isometric Equivalences

Informal description

For any semilinear isometric equivalence $f : E \simeq_{σ₁₂} E₂$ between seminormed additive commutative groups $E$ and $E₂$ with module structures over rings $R$ and $R₂$ respectively, the type $E \simeq_{σ₁₂} E₂$ can be injectively coerced to bijections between $E$ and $E₂$. This means that terms of type $E \simeq_{σ₁₂} E₂$ can be viewed as bijective functions from $E$ to $E₂$ in a natural way.

LinearIsometryEquiv.instSemilinearIsometryEquivClass instance

: SemilinearIsometryEquivClass (E ≃ₛₗᵢ[σ₁₂] E₂) σ₁₂ E E₂

Full source

instance instSemilinearIsometryEquivClass :
    SemilinearIsometryEquivClass (E ≃ₛₗᵢ[σ₁₂] E₂) σ₁₂ E E₂ where
  map_add f := map_add f.toLinearEquiv
  map_smulₛₗ e := map_smulₛₗ e.toLinearEquiv
  norm_map e := e.norm_map'

Class of Semilinear Isometric Equivalences

Informal description

The type of semilinear isometric equivalences $E \simeq_{σ₁₂} E₂$ between seminormed additive commutative groups $E$ and $E₂$ with module structures over rings $R$ and $R₂$ forms a class of semilinear isometric equivalences. This means every such equivalence is a bijective semilinear map that preserves the norm, where $σ₁₂: R \to R₂$ is a ring homomorphism with an inverse $σ₂₁: R₂ \to R$ forming a ring homomorphism inverse pair.

LinearIsometryEquiv.instCoeFun instance

: CoeFun (E ≃ₛₗᵢ[σ₁₂] E₂) fun _ ↦ E → E₂

Full source

/-- Shortcut instance, saving 8.5% of compilation time in
`Mathlib.Analysis.InnerProductSpace.Adjoint`.

(This instance was pinpointed by benchmarks; we didn't do an in depth investigation why it is
specifically needed.)
-/
instance instCoeFun : CoeFun (E ≃ₛₗᵢ[σ₁₂] E₂) fun _ ↦ E → E₂ := ⟨DFunLike.coe⟩

Semilinear Isometric Equivalences as Functions

Informal description

For any semilinear isometric equivalence $f : E \simeq_{σ₁₂} E₂$ between seminormed additive commutative groups $E$ and $E₂$ with module structures over rings $R$ and $R₂$ respectively, there is a canonical way to treat $f$ as a function from $E$ to $E₂$.

LinearIsometryEquiv.coe_injective theorem

: @Function.Injective (E ≃ₛₗᵢ[σ₁₂] E₂) (E → E₂) (↑)

Full source

theorem coe_injective : @Function.Injective (E ≃ₛₗᵢ[σ₁₂] E₂) (E → E₂) (↑) :=
  DFunLike.coe_injective

Injectivity of the Semilinear Isometric Equivalence to Function Map

Informal description

The canonical map from the type of semilinear isometric equivalences $E \simeq_{\sigma_{12}} E₂$ to the type of functions $E \to E₂$ is injective. That is, if two semilinear isometric equivalences $f, g : E \simeq_{\sigma_{12}} E₂$ satisfy $f(x) = g(x)$ for all $x \in E$, then $f = g$.

LinearIsometryEquiv.coe_mk theorem

(e : E ≃ₛₗ[σ₁₂] E₂) (he : ∀ x, ‖e x‖ = ‖x‖) : ⇑(mk e he) = e

Full source

@[simp]
theorem coe_mk (e : E ≃ₛₗ[σ₁₂] E₂) (he : ∀ x, ‖e x‖ = ‖x‖) : ⇑(mk e he) = e :=
  rfl

Underlying Function of Constructed Linear Isometric Equivalence

Informal description

Let $E$ and $E₂$ be seminormed additive commutative groups with module structures over rings $R$ and $R₂$ respectively, and let $\sigma_{12}: R \to R₂$ be a ring homomorphism. Given a semilinear equivalence $e: E \simeq_{\sigma_{12}} E₂$ that preserves the norm (i.e., $\|e(x)\| = \|x\|$ for all $x \in E$), the underlying function of the constructed linear isometric equivalence $\text{mk}(e, he)$ is equal to $e$.

LinearIsometryEquiv.coe_toLinearEquiv theorem

(e : E ≃ₛₗᵢ[σ₁₂] E₂) : ⇑e.toLinearEquiv = e

Full source

@[simp]
theorem coe_toLinearEquiv (e : E ≃ₛₗᵢ[σ₁₂] E₂) : ⇑e.toLinearEquiv = e :=
  rfl

Underlying Function of Linear Isometric Equivalence Matches Its Linear Equivalence

Informal description

For any semilinear isometric equivalence $e : E \simeq_{σ₁₂} E₂$, the underlying function of the associated linear equivalence $e.toLinearEquiv$ is equal to $e$ itself.

LinearIsometryEquiv.ext theorem

{e e' : E ≃ₛₗᵢ[σ₁₂] E₂} (h : ∀ x, e x = e' x) : e = e'

Full source

@[ext]
theorem ext {e e' : E ≃ₛₗᵢ[σ₁₂] E₂} (h : ∀ x, e x = e' x) : e = e' :=
  toLinearEquiv_injective <| LinearEquiv.ext h

Extensionality of Semilinear Isometric Equivalences

Informal description

Let $E$ and $E₂$ be seminormed additive commutative groups with module structures over rings $R$ and $R₂$ respectively, and let $\sigma_{12}: R \to R₂$ be a ring homomorphism. For any two semilinear isometric equivalences $e, e' : E \simeq_{\sigma_{12}} E₂$, if $e(x) = e'(x)$ for all $x \in E$, then $e = e'$.

LinearIsometryEquiv.congr_arg theorem

{f : E ≃ₛₗᵢ[σ₁₂] E₂} : ∀ {x x' : E}, x = x' → f x = f x'

Full source

protected theorem congr_arg {f : E ≃ₛₗᵢ[σ₁₂] E₂} : ∀ {x x' : E}, x = x' → f x = f x'
  | _, _, rfl => rfl

Semilinear Isometric Equivalence Preserves Equality

Informal description

For any semilinear isometric equivalence $f : E \simeq_{\sigma_{12}} E₂$ and any elements $x, x' \in E$, if $x = x'$, then $f(x) = f(x')$.

LinearIsometryEquiv.congr_fun theorem

{f g : E ≃ₛₗᵢ[σ₁₂] E₂} (h : f = g) (x : E) : f x = g x

Full source

protected theorem congr_fun {f g : E ≃ₛₗᵢ[σ₁₂] E₂} (h : f = g) (x : E) : f x = g x :=
  h ▸ rfl

Semilinear Isometric Equivalence Preserves Function Equality

Informal description

For any two semilinear isometric equivalences $f, g : E \simeq_{\sigma_{12}} E₂$ between seminormed additive commutative groups $E$ and $E₂$, if $f = g$, then for any $x \in E$, we have $f(x) = g(x)$.

LinearIsometryEquiv.ofBounds definition

 (e : E ≃ₛₗ[σ₁₂] E₂) (h₁ : ∀ x, ‖e x‖ ≤ ‖x‖) (h₂ : ∀ y, ‖e.symm y‖ ≤ ‖y‖) : E ≃ₛₗᵢ[σ₁₂] E₂

Full source

/-- Construct a `LinearIsometryEquiv` from a `LinearEquiv` and two inequalities:
`∀ x, ‖e x‖ ≤ ‖x‖` and `∀ y, ‖e.symm y‖ ≤ ‖y‖`. -/
def ofBounds (e : E ≃ₛₗ[σ₁₂] E₂) (h₁ : ∀ x, ‖e x‖ ≤ ‖x‖) (h₂ : ∀ y, ‖e.symm y‖ ≤ ‖y‖) :
    E ≃ₛₗᵢ[σ₁₂] E₂ :=
  ⟨e, fun x => le_antisymm (h₁ x) <| by simpa only [e.symm_apply_apply] using h₂ (e x)⟩

Construction of Semilinear Isometric Equivalence from Bounded Semilinear Equivalence

Informal description

Given a semilinear equivalence $e \colon E \simeq_{\sigma_{12}} E_2$ between seminormed additive commutative groups, if $e$ satisfies the inequalities $\|e(x)\| \leq \|x\|$ for all $x \in E$ and $\|e^{-1}(y)\| \leq \|y\|$ for all $y \in E_2$, then $e$ is a semilinear isometric equivalence.

LinearIsometryEquiv.norm_map theorem

(x : E) : ‖e x‖ = ‖x‖

Full source

@[simp]
theorem norm_map (x : E) : ‖e x‖ = ‖x‖ :=
  e.norm_map' x

Norm Preservation under Semilinear Isometric Equivalence

Informal description

For any semilinear isometric equivalence $e \colon E \simeq_{\sigma_{12}} E_2$ and any element $x \in E$, the norm of $e(x)$ is equal to the norm of $x$, i.e., $\|e(x)\| = \|x\|$.

LinearIsometryEquiv.toLinearIsometry definition

: E →ₛₗᵢ[σ₁₂] E₂

Full source

/-- Reinterpret a `LinearIsometryEquiv` as a `LinearIsometry`. -/
def toLinearIsometry : E →ₛₗᵢ[σ₁₂] E₂ :=
  ⟨e.1, e.2⟩

Semilinear isometric equivalence as an embedding

Informal description

The function converts a semilinear isometric equivalence $e \colon E \simeq_{\sigma_{12}} E_2$ between seminormed modules into a semilinear isometric embedding $E \to_{\sigma_{12}} E_2$ by forgetting the bijectivity and keeping only the norm-preserving property.

LinearIsometryEquiv.toLinearIsometry_injective theorem

: Function.Injective (toLinearIsometry : _ → E →ₛₗᵢ[σ₁₂] E₂)

Full source

theorem toLinearIsometry_injective : Function.Injective (toLinearIsometry : _ → E →ₛₗᵢ[σ₁₂] E₂) :=
  fun x _ h => coe_injective (congr_arg _ h : ⇑x.toLinearIsometry = _)

Injectivity of the Semilinear Isometric Equivalence to Embedding Map

Informal description

The map from semilinear isometric equivalences $E \simeq_{\sigma_{12}} E_2$ to semilinear isometric embeddings $E \to_{\sigma_{12}} E_2$ is injective. That is, if two semilinear isometric equivalences $f, g \colon E \simeq_{\sigma_{12}} E_2$ satisfy $f(x) = g(x)$ for all $x \in E$, then $f = g$.

LinearIsometryEquiv.toLinearIsometry_inj theorem

{f g : E ≃ₛₗᵢ[σ₁₂] E₂} : f.toLinearIsometry = g.toLinearIsometry ↔ f = g

Full source

@[simp]
theorem toLinearIsometry_inj {f g : E ≃ₛₗᵢ[σ₁₂] E₂} :
    f.toLinearIsometry = g.toLinearIsometry ↔ f = g :=
  toLinearIsometry_injective.eq_iff

Equality of Semilinear Isometric Equivalences via Their Embeddings

Informal description

For any two semilinear isometric equivalences $f, g \colon E \simeq_{\sigma_{12}} E_2$ between seminormed modules, the associated semilinear isometric embeddings $f.toLinearIsometry$ and $g.toLinearIsometry$ are equal if and only if $f = g$.

LinearIsometryEquiv.coe_toLinearIsometry theorem

: ⇑e.toLinearIsometry = e

Full source

@[simp]
theorem coe_toLinearIsometry : ⇑e.toLinearIsometry = e :=
  rfl

Underlying Function of Semilinear Isometric Equivalence as Embedding

Informal description

For a semilinear isometric equivalence $e \colon E \simeq_{\sigma_{12}} E_2$, the underlying function of the associated semilinear isometric embedding $e.toLinearIsometry$ is equal to $e$ itself.

LinearIsometryEquiv.isometry theorem

: Isometry e

Full source

protected theorem isometry : Isometry e :=
  e.toLinearIsometry.isometry

Semilinear Isometric Equivalence Preserves Distances

Informal description

A semilinear isometric equivalence $e \colon E \simeq_{\sigma_{12}} E_2$ between seminormed modules is an isometry, meaning it preserves distances: $d(e(x), e(y)) = d(x,y)$ for all $x, y \in E$.

LinearIsometryEquiv.toIsometryEquiv definition

: E ≃ᵢ E₂

Full source

/-- Reinterpret a `LinearIsometryEquiv` as an `IsometryEquiv`. -/
def toIsometryEquiv : E ≃ᵢ E₂ :=
  ⟨e.toLinearEquiv.toEquiv, e.isometry⟩

Semilinear isometric equivalence as isometric equivalence

Informal description

The function converts a semilinear isometric equivalence $e \colon E \simeq_{\sigma_{12}} E_2$ between seminormed modules into an isometric equivalence $E \simeq E_2$, preserving the distance between points.

LinearIsometryEquiv.toIsometryEquiv_injective theorem

: Function.Injective (toIsometryEquiv : (E ≃ₛₗᵢ[σ₁₂] E₂) → E ≃ᵢ E₂)

Full source

theorem toIsometryEquiv_injective :
    Function.Injective (toIsometryEquiv : (E ≃ₛₗᵢ[σ₁₂] E₂) → E ≃ᵢ E₂) := fun x _ h =>
  coe_injective (congr_arg _ h : ⇑x.toIsometryEquiv = _)

Injectivity of the Semilinear-to-Isometric Equivalence Conversion

Informal description

The map that converts a semilinear isometric equivalence $f \colon E \simeq_{\sigma_{12}} E_2$ to an isometric equivalence $E \simeq E_2$ is injective. That is, if two semilinear isometric equivalences $f, g \colon E \simeq_{\sigma_{12}} E_2$ satisfy $f(x) = g(x)$ for all $x \in E$ when viewed as isometric equivalences, then $f = g$ as semilinear isometric equivalences.

LinearIsometryEquiv.toIsometryEquiv_inj theorem

{f g : E ≃ₛₗᵢ[σ₁₂] E₂} : f.toIsometryEquiv = g.toIsometryEquiv ↔ f = g

Full source

@[simp]
theorem toIsometryEquiv_inj {f g : E ≃ₛₗᵢ[σ₁₂] E₂} :
    f.toIsometryEquiv = g.toIsometryEquiv ↔ f = g :=
  toIsometryEquiv_injective.eq_iff

Equality of Semilinear Isometric Equivalences via Induced Isometric Equivalences

Informal description

For any two semilinear isometric equivalences $f, g \colon E \simeq_{\sigma_{12}} E_2$ between seminormed modules, the induced isometric equivalences $f.\text{toIsometryEquiv}$ and $g.\text{toIsometryEquiv}$ are equal if and only if $f = g$.

LinearIsometryEquiv.coe_toIsometryEquiv theorem

: ⇑e.toIsometryEquiv = e

Full source

@[simp]
theorem coe_toIsometryEquiv : ⇑e.toIsometryEquiv = e :=
  rfl

Coercion of Semilinear Isometric Equivalence to Isometric Equivalence Preserves Function

Informal description

For any semilinear isometric equivalence $e \colon E \simeq_{\sigma_{12}} E_2$, the underlying function of the corresponding isometric equivalence $e.\text{toIsometryEquiv}$ is equal to $e$ itself. In other words, the coercion of $e.\text{toIsometryEquiv}$ to a function coincides with $e$.

LinearIsometryEquiv.range_eq_univ theorem

(e : E ≃ₛₗᵢ[σ₁₂] E₂) : Set.range e = Set.univ

Full source

theorem range_eq_univ (e : E ≃ₛₗᵢ[σ₁₂] E₂) : Set.range e = Set.univ := by
  rw [← coe_toIsometryEquiv]
  exact IsometryEquiv.range_eq_univ _

Range of Semilinear Isometric Equivalence is Entire Codomain

Informal description

For any semilinear isometric equivalence $e \colon E \simeq_{\sigma_{12}} E_2$ between seminormed modules $E$ and $E_2$, the range of $e$ is equal to the entire space $E_2$.

LinearIsometryEquiv.toHomeomorph definition

: E ≃ₜ E₂

Full source

/-- Reinterpret a `LinearIsometryEquiv` as a `Homeomorph`. -/
def toHomeomorph : E ≃ₜ E₂ :=
  e.toIsometryEquiv.toHomeomorph

Semilinear isometric equivalence as homeomorphism

Informal description

The function converts a semilinear isometric equivalence $e \colon E \simeq_{\sigma_{12}} E_2$ between seminormed modules into a homeomorphism $E \simeq E_2$, preserving the topological structure.

LinearIsometryEquiv.toHomeomorph_injective theorem

: Function.Injective (toHomeomorph : (E ≃ₛₗᵢ[σ₁₂] E₂) → E ≃ₜ E₂)

Full source

theorem toHomeomorph_injective : Function.Injective (toHomeomorph : (E ≃ₛₗᵢ[σ₁₂] E₂) → E ≃ₜ E₂) :=
  fun x _ h => coe_injective (congr_arg _ h : ⇑x.toHomeomorph = _)

Injectivity of the Semilinear Isometric Equivalence to Homeomorphism Map

Informal description

The map that converts a semilinear isometric equivalence $f : E \simeq_{\sigma_{12}} E_2$ to a homeomorphism $E \simeq E_2$ is injective. That is, if two semilinear isometric equivalences $f, g : E \simeq_{\sigma_{12}} E_2$ induce the same homeomorphism, then $f = g$.

LinearIsometryEquiv.toHomeomorph_inj theorem

{f g : E ≃ₛₗᵢ[σ₁₂] E₂} : f.toHomeomorph = g.toHomeomorph ↔ f = g

Full source

@[simp]
theorem toHomeomorph_inj {f g : E ≃ₛₗᵢ[σ₁₂] E₂} : f.toHomeomorph = g.toHomeomorph ↔ f = g :=
  toHomeomorph_injective.eq_iff

Equality of Semilinear Isometric Equivalences via Homeomorphisms

Informal description

For any two semilinear isometric equivalences $f, g \colon E \simeq_{\sigma_{12}} E_2$ between seminormed modules, the induced homeomorphisms $f.toHomeomorph$ and $g.toHomeomorph$ are equal if and only if $f = g$.

LinearIsometryEquiv.coe_toHomeomorph theorem

: ⇑e.toHomeomorph = e

Full source

@[simp]
theorem coe_toHomeomorph : ⇑e.toHomeomorph = e :=
  rfl

Homeomorphism Coercion of Semilinear Isometric Equivalence

Informal description

For a semilinear isometric equivalence $e \colon E \simeq_{\sigma_{12}} E_2$ between seminormed modules, the underlying function of the induced homeomorphism $e.toHomeomorph$ is equal to $e$ itself.

LinearIsometryEquiv.continuous theorem

: Continuous e

Full source

protected theorem continuous : Continuous e :=
  e.isometry.continuous

Continuity of Semilinear Isometric Equivalence

Informal description

A semilinear isometric equivalence $e \colon E \simeq_{\sigma_{12}} E_2$ between seminormed modules is continuous.

LinearIsometryEquiv.continuousAt theorem

{x} : ContinuousAt e x

Full source

protected theorem continuousAt {x} : ContinuousAt e x :=
  e.continuous.continuousAt

Pointwise Continuity of Semilinear Isometric Equivalence

Informal description

For any semilinear isometric equivalence $e \colon E \simeq_{\sigma_{12}} E_2$ between seminormed modules and any point $x \in E$, the map $e$ is continuous at $x$.

LinearIsometryEquiv.continuousOn theorem

{s} : ContinuousOn e s

Full source

protected theorem continuousOn {s} : ContinuousOn e s :=
  e.continuous.continuousOn

Continuity of Semilinear Isometric Equivalence on Subsets

Informal description

For any semilinear isometric equivalence $e \colon E \simeq_{\sigma_{12}} E_2$ between seminormed modules and any subset $s \subseteq E$, the restriction of $e$ to $s$ is continuous on $s$.

LinearIsometryEquiv.continuousWithinAt theorem

{s x} : ContinuousWithinAt e s x

Full source

protected theorem continuousWithinAt {s x} : ContinuousWithinAt e s x :=
  e.continuous.continuousWithinAt

Continuity Within a Subset for Semilinear Isometric Equivalences

Informal description

For any semilinear isometric equivalence $e \colon E \simeq_{\sigma_{12}} E_2$ between seminormed modules, a point $x \in E$, and a subset $s \subseteq E$, the map $e$ is continuous at $x$ within the subset $s$.

LinearIsometryEquiv.toContinuousLinearEquiv definition

: E ≃SL[σ₁₂] E₂

Full source

/-- Interpret a `LinearIsometryEquiv` as a `ContinuousLinearEquiv`. -/
def toContinuousLinearEquiv : E ≃SL[σ₁₂] E₂ :=
  { e.toLinearIsometry.toContinuousLinearMap, e.toHomeomorph with }

Semilinear isometric equivalence as continuous linear equivalence

Informal description

The function converts a semilinear isometric equivalence $e \colon E \simeq_{\sigma_{12}} E_2$ between seminormed modules into a continuous linear equivalence $E \simeq_{\sigma_{12}} E_2$, preserving both the linear and topological structures.

LinearIsometryEquiv.toContinuousLinearEquiv_injective theorem

: Function.Injective (toContinuousLinearEquiv : _ → E ≃SL[σ₁₂] E₂)

Full source

theorem toContinuousLinearEquiv_injective :
    Function.Injective (toContinuousLinearEquiv : _ → E ≃SL[σ₁₂] E₂) := fun x _ h =>
  coe_injective (congr_arg _ h : ⇑x.toContinuousLinearEquiv = _)

Injectivity of the Semilinear Isometric to Continuous Linear Equivalence Map

Informal description

The map from semilinear isometric equivalences $E \simeq_{\sigma_{12}} E_2$ to continuous linear equivalences $E \simeq_{\sigma_{12}} E_2$ is injective. That is, if two semilinear isometric equivalences $f, g \colon E \simeq_{\sigma_{12}} E_2$ have the same image under this map, then $f = g$.

LinearIsometryEquiv.toContinuousLinearEquiv_inj theorem

{f g : E ≃ₛₗᵢ[σ₁₂] E₂} : f.toContinuousLinearEquiv = g.toContinuousLinearEquiv ↔ f = g

Full source

@[simp]
theorem toContinuousLinearEquiv_inj {f g : E ≃ₛₗᵢ[σ₁₂] E₂} :
    f.toContinuousLinearEquiv = g.toContinuousLinearEquiv ↔ f = g :=
  toContinuousLinearEquiv_injective.eq_iff

Injectivity of the Semilinear Isometric to Continuous Linear Equivalence Map

Informal description

For any two semilinear isometric equivalences $f, g \colon E \simeq_{\sigma_{12}} E_2$ between seminormed modules $E$ and $E_2$, the continuous linear equivalences induced by $f$ and $g$ are equal if and only if $f = g$. In other words, the map from semilinear isometric equivalences to continuous linear equivalences is injective.

LinearIsometryEquiv.coe_toContinuousLinearEquiv theorem

: ⇑e.toContinuousLinearEquiv = e

Full source

@[simp]
theorem coe_toContinuousLinearEquiv : ⇑e.toContinuousLinearEquiv = e :=
  rfl

Equality of Underlying Functions in Semilinear Isometric Equivalence

Informal description

For any semilinear isometric equivalence $e \colon E \simeq_{\sigma_{12}} E_2$ between seminormed modules $E$ and $E_2$, the underlying function of the continuous linear equivalence $e.toContinuousLinearEquiv$ is equal to $e$ itself.

LinearIsometryEquiv.refl definition

: E ≃ₗᵢ[R] E

Full source

/-- Identity map as a `LinearIsometryEquiv`. -/
def refl : E ≃ₗᵢ[R] E :=
  ⟨LinearEquiv.refl R E, fun _ => rfl⟩

Identity linear isometric equivalence

Informal description

The identity map on a normed vector space $E$ over a ring $R$, viewed as a linear isometric equivalence from $E$ to itself. This map preserves both the linear structure and the norm, i.e., for any $x \in E$, we have $\|x\| = \|\text{refl}\, x\|$.

LinearIsometryEquiv.ulift definition

: ULift E ≃ₗᵢ[R] E

Full source

/-- Linear isometry equiv between a space and its lift to another universe. -/
def ulift : ULiftULift E ≃ₗᵢ[R] E :=
  { ContinuousLinearEquiv.ulift with norm_map' := fun _ => rfl }

Linear isometric equivalence between a space and its universe lift

Informal description

The linear isometric equivalence between a normed vector space $E$ and its lift to another universe, denoted as $\text{ULift}\, E \simeq_{R} E$, is a bijective linear map that preserves the norm. Here, $\text{ULift}\, E$ represents the lifted version of $E$ to another universe, and the equivalence is defined over the ring $R$.

LinearIsometryEquiv.instInhabited instance

: Inhabited (E ≃ₗᵢ[R] E)

Full source

instance instInhabited : Inhabited (E ≃ₗᵢ[R] E) := ⟨refl R E⟩

Inhabited Type of Linear Isometric Self-Equivalences

Informal description

For any normed vector space $E$ over a ring $R$, the type of linear isometric equivalences from $E$ to itself is inhabited. In particular, the identity map serves as a canonical inhabitant.

LinearIsometryEquiv.coe_refl theorem

: ⇑(refl R E) = id

Full source

@[simp]
theorem coe_refl : ⇑(refl R E) = id :=
  rfl

Identity Linear Isometric Equivalence as Identity Function

Informal description

The underlying function of the identity linear isometric equivalence on a normed vector space $E$ over a ring $R$ is equal to the identity function, i.e., $\text{refl}_R E = \text{id}$.

LinearIsometryEquiv.symm definition

: E₂ ≃ₛₗᵢ[σ₂₁] E

Full source

/-- The inverse `LinearIsometryEquiv`. -/
def symm : E₂ ≃ₛₗᵢ[σ₂₁] E :=
  ⟨e.toLinearEquiv.symm, fun x =>
    (e.norm_map _).symm.trans <| congr_arg norm <| e.toLinearEquiv.apply_symm_apply x⟩

Inverse of a semilinear isometric equivalence

Informal description

The inverse of a semilinear isometric equivalence $e : E \simeq_{σ₁₂} E₂$ is a semilinear isometric equivalence $e^{-1} : E₂ \simeq_{σ₂₁} E$, where $σ₂₁$ is the inverse ring homomorphism of $σ₁₂$. The inverse map preserves the norm, meaning that for any $x \in E₂$, the norm of $e^{-1}(x)$ in $E$ is equal to the norm of $x$ in $E₂$.

LinearIsometryEquiv.apply_symm_apply theorem

(x : E₂) : e (e.symm x) = x

Full source

@[simp]
theorem apply_symm_apply (x : E₂) : e (e.symm x) = x :=
  e.toLinearEquiv.apply_symm_apply x

Inverse Image Application Identity: $e(e^{-1}(x)) = x$

Informal description

For any semilinear isometric equivalence $e : E \simeq_{\sigma_{12}} E_2$ and any element $x \in E_2$, applying $e$ to the inverse image $e^{-1}(x)$ yields $x$, i.e., $e(e^{-1}(x)) = x$.

LinearIsometryEquiv.symm_apply_apply theorem

(x : E) : e.symm (e x) = x

Full source

@[simp]
theorem symm_apply_apply (x : E) : e.symm (e x) = x :=
  e.toLinearEquiv.symm_apply_apply x

Inverse Application of Semilinear Isometric Equivalence: $e^{-1}(e(x)) = x$

Informal description

For any semilinear isometric equivalence $e : E \simeq_{\sigma_{12}} E_2$ and any element $x \in E$, applying the inverse map $e^{-1}$ to the image $e(x)$ yields the original element $x$, i.e., $e^{-1}(e(x)) = x$.

LinearIsometryEquiv.map_eq_zero_iff theorem

{x : E} : e x = 0 ↔ x = 0

Full source

theorem map_eq_zero_iff {x : E} : e x = 0 ↔ x = 0 :=
  e.toLinearEquiv.map_eq_zero_iff

Semilinear Isometric Equivalence Preserves Zero: $e(x) = 0 \leftrightarrow x = 0$

Informal description

For any element $x$ in a seminormed additive commutative group $E$, a semilinear isometric equivalence $e : E \simeq_{σ₁₂} E₂$ maps $x$ to zero if and only if $x$ is zero, i.e., $e(x) = 0 \leftrightarrow x = 0$.

LinearIsometryEquiv.symm_symm theorem

: e.symm.symm = e

Full source

@[simp]
theorem symm_symm : e.symm.symm = e := rfl

Double Inverse of Semilinear Isometric Equivalence

Informal description

For any semilinear isometric equivalence $e : E \simeq_{σ₁₂} E₂$, the inverse of the inverse of $e$ is equal to $e$ itself, i.e., $(e^{-1})^{-1} = e$.

LinearIsometryEquiv.symm_bijective theorem

: Function.Bijective (symm : (E₂ ≃ₛₗᵢ[σ₂₁] E) → _)

Full source

theorem symm_bijective : Function.Bijective (symm : (E₂ ≃ₛₗᵢ[σ₂₁] E) → _) :=
  Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Bijectivity of the Inverse Operation on Semilinear Isometric Equivalences

Informal description

The inverse operation `symm` on semilinear isometric equivalences is bijective. That is, the map sending a semilinear isometric equivalence $e : E \simeq_{\sigma_{12}} E_2$ to its inverse $e^{-1} : E_2 \simeq_{\sigma_{21}} E$ is both injective and surjective.

LinearIsometryEquiv.toLinearEquiv_symm theorem

: e.toLinearEquiv.symm = e.symm.toLinearEquiv

Full source

@[simp]
theorem toLinearEquiv_symm : e.toLinearEquiv.symm = e.symm.toLinearEquiv :=
  rfl

Inverse of Underlying Linear Equivalence of Semilinear Isometric Equivalence

Informal description

For a semilinear isometric equivalence $e : E \simeq_{σ₁₂} E₂$, the inverse of the underlying linear equivalence $e.toLinearEquiv$ is equal to the linear equivalence underlying the inverse isometric equivalence $e.symm.toLinearEquiv$. That is, $(e.toLinearEquiv)^{-1} = e.symm.toLinearEquiv$.

LinearIsometryEquiv.toIsometryEquiv_symm theorem

: e.toIsometryEquiv.symm = e.symm.toIsometryEquiv

Full source

@[simp]
theorem toIsometryEquiv_symm : e.toIsometryEquiv.symm = e.symm.toIsometryEquiv :=
  rfl

Inverse of Isometric Equivalence from Semilinear Isometric Equivalence

Informal description

For a semilinear isometric equivalence $e \colon E \simeq_{\sigma_{12}} E_2$, the inverse of the isometric equivalence obtained from $e$ is equal to the isometric equivalence obtained from the inverse of $e$. That is, $(e.toIsometryEquiv)^{-1} = e.symm.toIsometryEquiv$.

LinearIsometryEquiv.toHomeomorph_symm theorem

: e.toHomeomorph.symm = e.symm.toHomeomorph

Full source

@[simp]
theorem toHomeomorph_symm : e.toHomeomorph.symm = e.symm.toHomeomorph :=
  rfl

Inverse of Homeomorphism from Semilinear Isometric Equivalence

Informal description

For a semilinear isometric equivalence $e \colon E \simeq_{\sigma_{12}} E_2$, the inverse of the homeomorphism obtained from $e$ is equal to the homeomorphism obtained from the inverse of $e$. That is, $(e.toHomeomorph)^{-1} = e.symm.toHomeomorph$.

LinearIsometryEquiv.Simps.apply definition

 (σ₁₂ : R →+* R₂) {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (E E₂ : Type*)
  [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (h : E ≃ₛₗᵢ[σ₁₂] E₂) : E → E₂

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 (σ₁₂ : R →+* R₂) {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂]
    (E E₂ : Type*) [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E]
    [Module R₂ E₂] (h : E ≃ₛₗᵢ[σ₁₂] E₂) : E → E₂ :=
  h

Application of semilinear isometric equivalence

Informal description

The function application for a semilinear isometric equivalence $h : E \simeq_{σ₁₂} E₂$ between seminormed additive commutative groups $E$ and $E₂$ with module structures over rings $R$ and $R₂$ respectively. Here $σ₁₂ : R \to R₂$ is a ring homomorphism with inverse $σ₂₁ : R₂ \to R$ forming a pair of mutually inverse ring homomorphisms. The function maps an element of $E$ to its corresponding element in $E₂$ while preserving both the linear structure and the norm.

LinearIsometryEquiv.Simps.symm_apply definition

 (σ₁₂ : R →+* R₂) {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (E E₂ : Type*)
  [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂] [Module R E] [Module R₂ E₂] (h : E ≃ₛₗᵢ[σ₁₂] E₂) : E₂ → E

Full source

/-- See Note [custom simps projection] -/
def Simps.symm_apply (σ₁₂ : R →+* R₂) {σ₂₁ : R₂ →+* R} [RingHomInvPair σ₁₂ σ₂₁]
    [RingHomInvPair σ₂₁ σ₁₂] (E E₂ : Type*) [SeminormedAddCommGroup E] [SeminormedAddCommGroup E₂]
    [Module R E] [Module R₂ E₂] (h : E ≃ₛₗᵢ[σ₁₂] E₂) : E₂ → E :=
  h.symm

Inverse application of semilinear isometric equivalence

Informal description

The function maps an element of $E₂$ to its corresponding element in $E$ via the inverse of the semilinear isometric equivalence $h : E \simeq_{σ₁₂} E₂$. Here, $σ₁₂ : R \to R₂$ is a ring homomorphism with inverse $σ₂₁ : R₂ \to R$ forming a pair of mutually inverse ring homomorphisms, and $E$ and $E₂$ are seminormed additive commutative groups with module structures over $R$ and $R₂$ respectively.

LinearIsometryEquiv.trans definition

(e' : E₂ ≃ₛₗᵢ[σ₂₃] E₃) : E ≃ₛₗᵢ[σ₁₃] E₃

Full source

/-- Composition of `LinearIsometryEquiv`s as a `LinearIsometryEquiv`. -/
def trans (e' : E₂ ≃ₛₗᵢ[σ₂₃] E₃) : E ≃ₛₗᵢ[σ₁₃] E₃ :=
  ⟨e.toLinearEquiv.trans e'.toLinearEquiv, fun _ => (e'.norm_map _).trans (e.norm_map _)⟩

Composition of semilinear isometric equivalences

Informal description

Given a semilinear isometric equivalence $e' : E₂ \simeq_{σ₂₃} E₃$, the composition of $e : E \simeq_{σ₁₂} E₂$ with $e'$ yields a semilinear isometric equivalence $E \simeq_{σ₁₃} E₃$. Here, $σ_{ij}$ are ring homomorphisms between the respective scalar rings, and the composition preserves both the linear structure and the norm.

LinearIsometryEquiv.coe_trans theorem

(e₁ : E ≃ₛₗᵢ[σ₁₂] E₂) (e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃) : ⇑(e₁.trans e₂) = e₂ ∘ e₁

Full source

@[simp]
theorem coe_trans (e₁ : E ≃ₛₗᵢ[σ₁₂] E₂) (e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃) : ⇑(e₁.trans e₂) = e₂ ∘ e₁ :=
  rfl

Composition of Semilinear Isometric Equivalences Preserves Function Application

Informal description

For any semilinear isometric equivalences $e_1 : E \simeq_{\sigma_{12}} E_2$ and $e_2 : E_2 \simeq_{\sigma_{23}} E_3$, the underlying function of their composition $e_1 \circ e_2$ is equal to the composition of their underlying functions, i.e., $(e_1 \circ e_2)(x) = e_2(e_1(x))$ for all $x \in E$.

LinearIsometryEquiv.trans_apply theorem

 (e₁ : E ≃ₛₗᵢ[σ₁₂] E₂) (e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃) (c : E) : (e₁.trans e₂ : E ≃ₛₗᵢ[σ₁₃] E₃) c = e₂ (e₁ c)

Full source

@[simp]
theorem trans_apply (e₁ : E ≃ₛₗᵢ[σ₁₂] E₂) (e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃) (c : E) :
    (e₁.trans e₂ : E ≃ₛₗᵢ[σ₁₃] E₃) c = e₂ (e₁ c) :=
  rfl

Composition of Semilinear Isometric Equivalences Preserves Application

Informal description

Let $E$, $E₂$, and $E₃$ be seminormed additive commutative groups with module structures over rings $R$, $R₂$, and $R₃$ respectively, and let $\sigma_{12} : R \to R₂$, $\sigma_{23} : R₂ \to R₃$ be ring homomorphisms. Given semilinear isometric equivalences $e₁ : E \simeq_{\sigma_{12}} E₂$ and $e₂ : E₂ \simeq_{\sigma_{23}} E₃$, the composition $e₁ \circ e₂$ satisfies $(e₁ \circ e₂)(c) = e₂(e₁(c))$ for any $c \in E$.

LinearIsometryEquiv.toLinearEquiv_trans theorem

(e' : E₂ ≃ₛₗᵢ[σ₂₃] E₃) : (e.trans e').toLinearEquiv = e.toLinearEquiv.trans e'.toLinearEquiv

Full source

@[simp]
theorem toLinearEquiv_trans (e' : E₂ ≃ₛₗᵢ[σ₂₃] E₃) :
    (e.trans e').toLinearEquiv = e.toLinearEquiv.trans e'.toLinearEquiv :=
  rfl

Compatibility of Composition with Underlying Linear Equivalence for Semilinear Isometric Equivalences

Informal description

For any semilinear isometric equivalences $e : E \simeq_{σ₁₂} E₂$ and $e' : E₂ \simeq_{σ₂₃} E₃$, the underlying linear equivalence of the composition $e \circ e'$ is equal to the composition of the underlying linear equivalences of $e$ and $e'$. That is, $(e \circ e').toLinearEquiv = e.toLinearEquiv \circ e'.toLinearEquiv$.

LinearIsometryEquiv.trans_refl theorem

: e.trans (refl R₂ E₂) = e

Full source

@[simp]
theorem trans_refl : e.trans (refl R₂ E₂) = e :=
  ext fun _ => rfl

Right Identity Property of Semilinear Isometric Equivalence Composition

Informal description

For any semilinear isometric equivalence $e : E \simeq_{\sigma_{12}} E₂$ between seminormed vector spaces $E$ and $E₂$, the composition of $e$ with the identity isometric equivalence on $E₂$ equals $e$ itself. That is, $e \circ \text{refl}_{E₂} = e$.

LinearIsometryEquiv.refl_trans theorem

: (refl R E).trans e = e

Full source

@[simp]
theorem refl_trans : (refl R E).trans e = e :=
  ext fun _ => rfl

Identity Composition Law for Semilinear Isometric Equivalences

Informal description

For any semilinear isometric equivalence $e : E \simeq_{\sigma_{12}} E₂$, the composition of the identity isometric equivalence $\text{refl}_R E$ with $e$ is equal to $e$ itself. That is, $\text{refl}_R E \circ e = e$.

LinearIsometryEquiv.self_trans_symm theorem

: e.trans e.symm = refl R E

Full source

@[simp]
theorem self_trans_symm : e.trans e.symm = refl R E :=
  ext e.symm_apply_apply

Composition of Semilinear Isometric Equivalence with its Inverse Yields Identity

Informal description

For any semilinear isometric equivalence $e : E \simeq_{\sigma_{12}} E_2$, the composition of $e$ with its inverse $e^{-1}$ is equal to the identity isometric equivalence on $E$, i.e., $e \circ e^{-1} = \text{id}_E$.

LinearIsometryEquiv.symm_trans_self theorem

: e.symm.trans e = refl R₂ E₂

Full source

@[simp]
theorem symm_trans_self : e.symm.trans e = refl R₂ E₂ :=
  ext e.apply_symm_apply

Inverse Composition Yields Identity: $e^{-1} \circ e = \text{id}_{E_2}$

Informal description

For any semilinear isometric equivalence $e : E \simeq_{\sigma_{12}} E_2$ between seminormed vector spaces $E$ and $E_2$ over rings $R$ and $R_2$ respectively, the composition of the inverse equivalence $e^{-1} : E_2 \simeq_{\sigma_{21}} E$ with $e$ yields the identity equivalence on $E_2$. That is, $e^{-1} \circ e = \text{id}_{E_2}$.

LinearIsometryEquiv.symm_comp_self theorem

: e.symm ∘ e = id

Full source

@[simp]
theorem symm_comp_self : e.symm ∘ e = id :=
  funext e.symm_apply_apply

Inverse Composition Identity for Semilinear Isometric Equivalence

Informal description

For any semilinear isometric equivalence $e : E \simeq_{\sigma_{12}} E_2$, the composition of its inverse $e^{-1}$ with $e$ is equal to the identity function on $E$, i.e., $e^{-1} \circ e = \text{id}_E$.

LinearIsometryEquiv.self_comp_symm theorem

: e ∘ e.symm = id

Full source

@[simp]
theorem self_comp_symm : e ∘ e.symm = id :=
  e.symm.symm_comp_self

Composition of Semilinear Isometric Equivalence with Its Inverse Yields Identity

Informal description

For any semilinear isometric equivalence $e : E \simeq_{\sigma_{12}} E_2$, the composition of $e$ with its inverse $e^{-1}$ is equal to the identity function on $E_2$, i.e., $e \circ e^{-1} = \text{id}_{E_2}$.

LinearIsometryEquiv.symm_trans theorem

 (e₁ : E ≃ₛₗᵢ[σ₁₂] E₂) (e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃) : (e₁.trans e₂).symm = e₂.symm.trans e₁.symm

Full source

@[simp]
theorem symm_trans (e₁ : E ≃ₛₗᵢ[σ₁₂] E₂) (e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃) :
    (e₁.trans e₂).symm = e₂.symm.trans e₁.symm :=
  rfl

Inverse of Composition of Semilinear Isometric Equivalences

Informal description

Let $E$, $E₂$, and $E₃$ be seminormed additive commutative groups equipped with module structures over rings $R$, $R₂$, and $R₃$ respectively. Let $\sigma_{12} : R \to R₂$ and $\sigma_{23} : R₂ \to R₃$ be ring homomorphisms with corresponding inverse homomorphisms $\sigma_{21}$ and $\sigma_{32}$ forming ring homomorphism inverse pairs. Given semilinear isometric equivalences $e₁ : E \simeq_{\sigma_{12}} E₂$ and $e₂ : E₂ \simeq_{\sigma_{23}} E₃$, the inverse of their composition $(e₁ \circ e₂)^{-1}$ is equal to the composition of their inverses in reverse order, i.e., $e₂^{-1} \circ e₁^{-1}$.

LinearIsometryEquiv.coe_symm_trans theorem

 (e₁ : E ≃ₛₗᵢ[σ₁₂] E₂) (e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃) : ⇑(e₁.trans e₂).symm = e₁.symm ∘ e₂.symm

Full source

theorem coe_symm_trans (e₁ : E ≃ₛₗᵢ[σ₁₂] E₂) (e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃) :
    ⇑(e₁.trans e₂).symm = e₁.symm ∘ e₂.symm :=
  rfl

Inverse of Composition of Semilinear Isometric Equivalences is Reverse Composition of Inverses

Informal description

Let $E$, $E₂$, and $E₃$ be seminormed additive commutative groups equipped with module structures over rings $R$, $R₂$, and $R₃$ respectively. Let $σ_{12} : R \to R₂$ and $σ_{23} : R₂ \to R₃$ be ring homomorphisms with corresponding inverses $σ_{21}$ and $σ_{32}$. Given semilinear isometric equivalences $e_1 : E \simeq_{σ_{12}} E₂$ and $e_2 : E₂ \simeq_{σ_{23}} E₃$, the inverse of their composition $(e_1 \circ e_2)^{-1}$ is equal to the composition of their inverses in reverse order, i.e., $(e_1 \circ e_2)^{-1} = e_2^{-1} \circ e_1^{-1}$.

LinearIsometryEquiv.trans_assoc theorem

 (eEE₂ : E ≃ₛₗᵢ[σ₁₂] E₂) (eE₂E₃ : E₂ ≃ₛₗᵢ[σ₂₃] E₃) (eE₃E₄ : E₃ ≃ₛₗᵢ[σ₃₄] E₄) :
  eEE₂.trans (eE₂E₃.trans eE₃E₄) = (eEE₂.trans eE₂E₃).trans eE₃E₄

Full source

theorem trans_assoc (eEE₂ : E ≃ₛₗᵢ[σ₁₂] E₂) (eE₂E₃ : E₂ ≃ₛₗᵢ[σ₂₃] E₃) (eE₃E₄ : E₃ ≃ₛₗᵢ[σ₃₄] E₄) :
    eEE₂.trans (eE₂E₃.trans eE₃E₄) = (eEE₂.trans eE₂E₃).trans eE₃E₄ :=
  rfl

Associativity of Composition for Semilinear Isometric Equivalences

Informal description

For semilinear isometric equivalences $e_{EE₂} : E \simeq_{σ₁₂} E₂$, $e_{E₂E₃} : E₂ \simeq_{σ₂₃} E₃$, and $e_{E₃E₄} : E₃ \simeq_{σ₃₄} E₄$, the composition operation satisfies the associativity property: $$ e_{EE₂} \circ (e_{E₂E₃} \circ e_{E₃E₄}) = (e_{EE₂} \circ e_{E₂E₃}) \circ e_{E₃E₄} $$ where $\circ$ denotes the composition of semilinear isometric equivalences.

LinearIsometryEquiv.instGroup instance

: Group (E ≃ₗᵢ[R] E)

Full source

instance instGroup : Group (E ≃ₗᵢ[R] E) where
  mul e₁ e₂ := e₂.trans e₁
  one := refl _ _
  inv := symm
  one_mul := trans_refl
  mul_one := refl_trans
  mul_assoc _ _ _ := trans_assoc _ _ _
  inv_mul_cancel := self_trans_symm

Group Structure on Linear Isometric Equivalences

Informal description

The set of linear isometric equivalences from a normed vector space $E$ to itself forms a group under composition, where the identity element is the identity map, the inverse of an isometry is its inverse map, and the group operation is given by composition of maps.

LinearIsometryEquiv.coe_one theorem

: ⇑(1 : E ≃ₗᵢ[R] E) = id

Full source

@[simp]
theorem coe_one : ⇑(1 : E ≃ₗᵢ[R] E) = id :=
  rfl

Identity Element of Linear Isometric Equivalence Group is Identity Map

Informal description

The identity element in the group of linear isometric equivalences from a normed vector space $E$ to itself corresponds to the identity function, i.e., the map associated with $1 \in E \simeq_{R} E$ is the identity map $\text{id} : E \to E$.

LinearIsometryEquiv.coe_mul theorem

(e e' : E ≃ₗᵢ[R] E) : ⇑(e * e') = e ∘ e'

Full source

@[simp]
theorem coe_mul (e e' : E ≃ₗᵢ[R] E) : ⇑(e * e') = e ∘ e' :=
  rfl

Composition of Linear Isometric Equivalences Preserves Function Composition

Informal description

For any linear isometric equivalences $e, e' : E \simeq_{R} E$ on a normed vector space $E$ over a ring $R$, the underlying function of the composition $e * e'$ is equal to the composition of the underlying functions $e \circ e'$.

LinearIsometryEquiv.coe_inv theorem

(e : E ≃ₗᵢ[R] E) : ⇑e⁻¹ = e.symm

Full source

@[simp]
theorem coe_inv (e : E ≃ₗᵢ[R] E) : ⇑e⁻¹ = e.symm :=
  rfl

Inverse of Linear Isometric Equivalence Equals its Symmetric Map

Informal description

For any linear isometric equivalence $e : E \simeq_{R} E$ on a normed vector space $E$ over a ring $R$, the inverse map $e^{-1}$ is equal to the symmetric map $e^{\text{symm}}$, i.e., $e^{-1} = e^{\text{symm}}$.

LinearIsometryEquiv.one_def theorem

: (1 : E ≃ₗᵢ[R] E) = refl _ _

Full source

theorem one_def : (1 : E ≃ₗᵢ[R] E) = refl _ _ :=
  rfl

Identity Element as Identity Linear Isometric Equivalence

Informal description

The identity element of the group of linear isometric equivalences from a normed vector space $E$ to itself over a ring $R$ is equal to the identity linear isometric equivalence, i.e., $1 = \text{refl}_R E$.

LinearIsometryEquiv.mul_def theorem

(e e' : E ≃ₗᵢ[R] E) : (e * e' : E ≃ₗᵢ[R] E) = e'.trans e

Full source

theorem mul_def (e e' : E ≃ₗᵢ[R] E) : (e * e' : E ≃ₗᵢ[R] E) = e'.trans e :=
  rfl

Group Multiplication of Linear Isometric Equivalences as Composition

Informal description

For any two linear isometric equivalences $e, e' : E \simeq_{R} E$ on a normed vector space $E$ over a ring $R$, the group multiplication $e * e'$ is equal to the composition $e' \circ e$ (denoted as `e'.trans e` in Lean).

LinearIsometryEquiv.inv_def theorem

(e : E ≃ₗᵢ[R] E) : (e⁻¹ : E ≃ₗᵢ[R] E) = e.symm

Full source

theorem inv_def (e : E ≃ₗᵢ[R] E) : (e⁻¹ : E ≃ₗᵢ[R] E) = e.symm :=
  rfl

Inverse of Linear Isometric Equivalence Equals Symmetric Map

Informal description

For any linear isometric equivalence $e : E \simeq_{R} E$ on a normed vector space $E$ over a ring $R$, the group inverse $e^{-1}$ is equal to the symmetric isometric equivalence $e^{\text{symm}}$, which is the inverse map of $e$.

LinearIsometryEquiv.trans_one theorem

: e.trans (1 : E₂ ≃ₗᵢ[R₂] E₂) = e

Full source

@[simp]
theorem trans_one : e.trans (1 : E₂ ≃ₗᵢ[R₂] E₂) = e :=
  trans_refl _

Right Identity Property of Linear Isometric Equivalence Composition

Informal description

For any linear isometric equivalence $e : E \simeq_{R} E_2$ between normed vector spaces $E$ and $E_2$ over rings $R$ and $R_2$ respectively, the composition of $e$ with the identity isometric equivalence on $E_2$ equals $e$ itself. That is, $e \circ \text{id}_{E_2} = e$.

LinearIsometryEquiv.one_trans theorem

: (1 : E ≃ₗᵢ[R] E).trans e = e

Full source

@[simp]
theorem one_trans : (1 : E ≃ₗᵢ[R] E).trans e = e :=
  refl_trans _

Identity Composition Law for Linear Isometric Equivalences

Informal description

For any linear isometric equivalence $e : E \simeq_{R} E_2$ between normed vector spaces $E$ and $E_2$ over a ring $R$, the composition of the identity isometric equivalence $1 : E \simeq_{R} E$ with $e$ equals $e$. That is, $1 \circ e = e$.

LinearIsometryEquiv.refl_mul theorem

(e : E ≃ₗᵢ[R] E) : refl _ _ * e = e

Full source

@[simp]
theorem refl_mul (e : E ≃ₗᵢ[R] E) : refl _ _ * e = e :=
  trans_refl _

Left Identity Property of Linear Isometric Equivalence Composition

Informal description

For any linear isometric equivalence $e : E \simeq_{R} E$ on a normed vector space $E$ over a ring $R$, the composition of the identity isometric equivalence with $e$ equals $e$. That is, $\text{refl}_E \circ e = e$.

LinearIsometryEquiv.mul_refl theorem

(e : E ≃ₗᵢ[R] E) : e * refl _ _ = e

Full source

@[simp]
theorem mul_refl (e : E ≃ₗᵢ[R] E) : e * refl _ _ = e :=
  refl_trans _

Composition with Identity Preserves Linear Isometric Equivalence

Informal description

For any linear isometric equivalence $e \colon E \simeq_{R} E$ on a normed vector space $E$ over a ring $R$, the composition of $e$ with the identity isometric equivalence $\text{refl}_R E$ is equal to $e$ itself, i.e., $e \circ \text{refl}_R E = e$.

LinearIsometryEquiv.instCoeTCContinuousLinearEquiv instance

: CoeTC (E ≃ₛₗᵢ[σ₁₂] E₂) (E ≃SL[σ₁₂] E₂)

Full source

/-- Reinterpret a `LinearIsometryEquiv` as a `ContinuousLinearEquiv`. -/
instance instCoeTCContinuousLinearEquiv : CoeTC (E ≃ₛₗᵢ[σ₁₂] E₂) (E ≃SL[σ₁₂] E₂) :=
  ⟨fun e => ⟨e.toLinearEquiv, e.continuous, e.toIsometryEquiv.symm.continuous⟩⟩

Semilinear Isometric Equivalence as Continuous Semilinear Equivalence

Informal description

Every semilinear isometric equivalence $f \colon E \simeq_{\sigma_{12}} E_2$ between seminormed modules can be interpreted as a continuous semilinear equivalence $f \colon E \simeq_{SL[\sigma_{12}]} E_2$.

LinearIsometryEquiv.instCoeTCContinuousLinearMap instance

: CoeTC (E ≃ₛₗᵢ[σ₁₂] E₂) (E →SL[σ₁₂] E₂)

Full source

instance instCoeTCContinuousLinearMap : CoeTC (E ≃ₛₗᵢ[σ₁₂] E₂) (E →SL[σ₁₂] E₂) :=
  ⟨fun e => ↑(e : E ≃SL[σ₁₂] E₂)⟩

Semilinear Isometric Equivalence as Continuous Semilinear Map

Informal description

Every semilinear isometric equivalence $e \colon E \simeq_{\sigma_{12}} E_2$ between seminormed modules can be naturally viewed as a continuous semilinear map $E \to_{SL[\sigma_{12}]} E_2$.

LinearIsometryEquiv.coe_coe theorem

: ⇑(e : E ≃SL[σ₁₂] E₂) = e

Full source

@[simp]
theorem coe_coe : ⇑(e : E ≃SL[σ₁₂] E₂) = e :=
  rfl

Coercion of Semilinear Isometric Equivalence to Continuous Semilinear Equivalence Preserves Underlying Function

Informal description

For a semilinear isometric equivalence $e \colon E \simeq_{\sigma_{12}} E_2$, the underlying function of $e$ when viewed as a continuous semilinear equivalence (via coercion) is equal to $e$ itself.

LinearIsometryEquiv.coe_coe'' theorem

: ⇑(e : E →SL[σ₁₂] E₂) = e

Full source

@[simp]
theorem coe_coe'' : ⇑(e : E →SL[σ₁₂] E₂) = e :=
  rfl

Coercion of Semilinear Isometric Equivalence to Continuous Semilinear Map Preserves Function

Informal description

For a semilinear isometric equivalence $e \colon E \simeq_{\sigma_{12}} E_2$, the underlying function of $e$ when viewed as a continuous semilinear map (via coercion) is equal to $e$ itself.

LinearIsometryEquiv.map_zero theorem

: e 0 = 0

Full source

theorem map_zero : e 0 = 0 :=
  e.1.map_zero

Preservation of Zero by Semilinear Isometric Equivalence

Informal description

For any semilinear isometric equivalence $e \colon E \simeq_{\sigma_{12}} E_2$, the map $e$ preserves the zero element, i.e., $e(0) = 0$.

LinearIsometryEquiv.map_add theorem

(x y : E) : e (x + y) = e x + e y

Full source

theorem map_add (x y : E) : e (x + y) = e x + e y :=
  e.1.map_add x y

Additivity of Semilinear Isometric Equivalence

Informal description

For any semilinear isometric equivalence $e \colon E \simeq_{\sigma_{12}} E_2$ and any elements $x, y \in E$, the map $e$ preserves addition, i.e., $e(x + y) = e(x) + e(y)$.

LinearIsometryEquiv.map_sub theorem

(x y : E) : e (x - y) = e x - e y

Full source

theorem map_sub (x y : E) : e (x - y) = e x - e y :=
  e.1.map_sub x y

Subtraction Preservation by Semilinear Isometric Equivalence

Informal description

For any semilinear isometric equivalence $e \colon E \simeq_{\sigma_{12}} E_2$ and any elements $x, y \in E$, the map $e$ preserves subtraction, i.e., $e(x - y) = e(x) - e(y)$.

LinearIsometryEquiv.map_smulₛₗ theorem

(c : R) (x : E) : e (c • x) = σ₁₂ c • e x

Full source

theorem map_smulₛₗ (c : R) (x : E) : e (c • x) = σ₁₂ c • e x :=
  e.1.map_smulₛₗ c x

Semilinear Property of Isometric Equivalence

Informal description

For any semilinear isometric equivalence $e \colon E \simeq_{\sigma_{12}} E_2$, any scalar $c \in R$, and any vector $x \in E$, the map $e$ satisfies the semilinear property $e(c \cdot x) = \sigma_{12}(c) \cdot e(x)$.

LinearIsometryEquiv.map_smul theorem

[Module R E₂] {e : E ≃ₗᵢ[R] E₂} (c : R) (x : E) : e (c • x) = c • e x

Full source

theorem map_smul [Module R E₂] {e : E ≃ₗᵢ[R] E₂} (c : R) (x : E) : e (c • x) = c • e x :=
  e.1.map_smul c x

Linear Isometric Equivalence Preserves Scalar Multiplication

Informal description

For any linear isometric equivalence $e \colon E \simeq_{R} E_2$ between seminormed spaces $E$ and $E_2$ over the same ring $R$, and for any scalar $c \in R$ and vector $x \in E$, the map $e$ preserves scalar multiplication, i.e., $e(c \cdot x) = c \cdot e(x)$.

LinearIsometryEquiv.nnnorm_map theorem

(x : E) : ‖e x‖₊ = ‖x‖₊

Full source

@[simp] -- Should be replaced with `SemilinearIsometryClass.nnorm_map` when https://github.com/leanprover/lean4/issues/3107 is fixed.
theorem nnnorm_map (x : E) : ‖e x‖₊ = ‖x‖₊ :=
  SemilinearIsometryClass.nnnorm_map e x

Nonnegative Norm Preservation under Semilinear Isometric Equivalence: $\|e(x)\|_+ = \|x\|_+$

Informal description

For any semilinear isometric equivalence $e \colon E \simeq_{\sigma_{12}} E_2$ and any vector $x \in E$, the nonnegative norm of $e(x)$ is equal to the nonnegative norm of $x$, i.e., $\|e(x)\|_+ = \|x\|_+$.

LinearIsometryEquiv.dist_map theorem

(x y : E) : dist (e x) (e y) = dist x y

Full source

@[simp]
theorem dist_map (x y : E) : dist (e x) (e y) = dist x y :=
  e.toLinearIsometry.dist_map x y

Distance Preservation under Semilinear Isometric Equivalence: $d(e(x), e(y)) = d(x, y)$

Informal description

For any semilinear isometric equivalence $e \colon E \simeq_{\sigma_{12}} E_2$ and any two vectors $x, y \in E$, the distance between $e(x)$ and $e(y)$ is equal to the distance between $x$ and $y$, i.e., $d(e(x), e(y)) = d(x, y)$.

LinearIsometryEquiv.edist_map theorem

(x y : E) : edist (e x) (e y) = edist x y

Full source

@[simp]
theorem edist_map (x y : E) : edist (e x) (e y) = edist x y :=
  e.toLinearIsometry.edist_map x y

Preservation of Extended Distance under Semilinear Isometric Equivalence: $\text{edist}(e(x), e(y)) = \text{edist}(x, y)$

Informal description

For any semilinear isometric equivalence $e \colon E \simeq_{\sigma_{12}} E_2$ and any two vectors $x, y \in E$, the extended distance between $e(x)$ and $e(y)$ equals the extended distance between $x$ and $y$, i.e., $\text{edist}(e(x), e(y)) = \text{edist}(x, y)$.

LinearIsometryEquiv.bijective theorem

: Bijective e

Full source

protected theorem bijective : Bijective e :=
  e.1.bijective

Bijectivity of Semilinear Isometric Equivalences

Informal description

A semilinear isometric equivalence $e : E \simeq_{σ₁₂} E₂$ is bijective, meaning it is both injective and surjective as a function from $E$ to $E₂$.

LinearIsometryEquiv.injective theorem

: Injective e

Full source

protected theorem injective : Injective e :=
  e.1.injective

Injectivity of Semilinear Isometric Equivalences

Informal description

A semilinear isometric equivalence $e : E \simeq_{σ₁₂} E₂$ is injective, meaning that for any $x, y \in E$, if $e(x) = e(y)$, then $x = y$.

LinearIsometryEquiv.surjective theorem

: Surjective e

Full source

protected theorem surjective : Surjective e :=
  e.1.surjective

Surjectivity of Semilinear Isometric Equivalences

Informal description

A semilinear isometric equivalence $e : E \simeq_{σ₁₂} E₂$ is surjective, meaning that for every $y \in E₂$, there exists an $x \in E$ such that $e(x) = y$.

LinearIsometryEquiv.map_eq_iff theorem

{x y : E} : e x = e y ↔ x = y

Full source

theorem map_eq_iff {x y : E} : e x = e y ↔ x = y :=
  e.injective.eq_iff

Injective Characterization of Semilinear Isometric Equivalences: $e(x) = e(y) \leftrightarrow x = y$

Informal description

For any semilinear isometric equivalence $e : E \simeq_{σ₁₂} E₂$ and any elements $x, y \in E$, the images $e(x)$ and $e(y)$ are equal if and only if $x = y$.

LinearIsometryEquiv.map_ne theorem

{x y : E} (h : x ≠ y) : e x ≠ e y

Full source

theorem map_ne {x y : E} (h : x ≠ y) : e x ≠ e y :=
  e.injective.ne h

Semilinear Isometric Equivalence Preserves Inequality

Informal description

For any semilinear isometric equivalence $e : E \simeq_{σ₁₂} E₂$ and any elements $x, y \in E$, if $x \neq y$, then $e(x) \neq e(y)$.

LinearIsometryEquiv.lipschitz theorem

: LipschitzWith 1 e

Full source

protected theorem lipschitz : LipschitzWith 1 e :=
  e.isometry.lipschitz

Lipschitz Continuity of Semilinear Isometric Equivalences with Constant 1

Informal description

A semilinear isometric equivalence $e \colon E \simeq_{\sigma_{12}} E_2$ is Lipschitz continuous with constant 1, meaning that for all $x, y \in E$, the distance satisfies $d(e(x), e(y)) \leq d(x,y)$.

LinearIsometryEquiv.antilipschitz theorem

: AntilipschitzWith 1 e

Full source

protected theorem antilipschitz : AntilipschitzWith 1 e :=
  e.isometry.antilipschitz

Antilipschitz Property of Semilinear Isometric Equivalences with Constant 1

Informal description

A semilinear isometric equivalence $e \colon E \simeq_{\sigma_{12}} E_2$ is antilipschitz with constant 1, meaning that for all $x, y \in E$, the distance satisfies $d(x,y) \leq d(e(x), e(y))$.

LinearIsometryEquiv.image_eq_preimage theorem

(s : Set E) : e '' s = e.symm ⁻¹' s

Full source

theorem image_eq_preimage (s : Set E) : e '' s = e.symm ⁻¹' s :=
  e.toLinearEquiv.image_eq_preimage s

Image Equals Preimage under Semilinear Isometric Equivalence

Informal description

For any semilinear isometric equivalence $e : E \simeq_{σ₁₂} E₂$ and any subset $s \subseteq E$, the image of $s$ under $e$ is equal to the preimage of $s$ under the inverse map $e^{-1} : E₂ \simeq_{σ₂₁} E$. That is, $e(s) = e^{-1}^{-1}(s)$.

LinearIsometryEquiv.ediam_image theorem

(s : Set E) : EMetric.diam (e '' s) = EMetric.diam s

Full source

@[simp]
theorem ediam_image (s : Set E) : EMetric.diam (e '' s) = EMetric.diam s :=
  e.isometry.ediam_image s

Preservation of Extended Metric Diameter under Semilinear Isometric Equivalence

Informal description

For any semilinear isometric equivalence $e \colon E \simeq_{\sigma_{12}} E_2$ between seminormed modules and any subset $s \subseteq E$, the extended metric diameter of the image $e(s)$ is equal to the extended metric diameter of $s$, i.e., $\text{diam}(e(s)) = \text{diam}(s)$.

LinearIsometryEquiv.diam_image theorem

(s : Set E) : Metric.diam (e '' s) = Metric.diam s

Full source

@[simp]
theorem diam_image (s : Set E) : Metric.diam (e '' s) = Metric.diam s :=
  e.isometry.diam_image s

Diameter Preservation under Semilinear Isometric Equivalence

Informal description

For any semilinear isometric equivalence $e \colon E \simeq_{\sigma_{12}} E_2$ between seminormed modules and any subset $s \subseteq E$, the diameter of the image $e(s)$ equals the diameter of $s$. That is, $\text{diam}(e(s)) = \text{diam}(s)$.

LinearIsometryEquiv.preimage_ball theorem

(x : E₂) (r : ℝ) : e ⁻¹' Metric.ball x r = Metric.ball (e.symm x) r

Full source

@[simp]
theorem preimage_ball (x : E₂) (r : ℝ) : e ⁻¹' Metric.ball x r = Metric.ball (e.symm x) r :=
  e.toIsometryEquiv.preimage_ball x r

Preimage of Open Ball under Semilinear Isometric Equivalence

Informal description

Let $e \colon E \simeq_{\sigma_{12}} E_2$ be a semilinear isometric equivalence between seminormed modules $E$ and $E_2$. For any point $x \in E_2$ and radius $r \in \mathbb{R}$, the preimage of the open ball $\text{ball}(x, r)$ under $e$ is equal to the open ball $\text{ball}(e^{-1}(x), r)$ in $E$.

LinearIsometryEquiv.preimage_sphere theorem

(x : E₂) (r : ℝ) : e ⁻¹' Metric.sphere x r = Metric.sphere (e.symm x) r

Full source

@[simp]
theorem preimage_sphere (x : E₂) (r : ℝ) : e ⁻¹' Metric.sphere x r = Metric.sphere (e.symm x) r :=
  e.toIsometryEquiv.preimage_sphere x r

Preimage of Sphere under Semilinear Isometric Equivalence

Informal description

For any semilinear isometric equivalence $e \colon E \simeq_{\sigma_{12}} E_2$ between seminormed modules, any point $x \in E_2$, and any radius $r \in \mathbb{R}$, the preimage of the sphere centered at $x$ with radius $r$ under $e$ is equal to the sphere centered at $e^{-1}(x)$ with radius $r$ in $E$. That is, $$ e^{-1}(\text{sphere}(x, r)) = \text{sphere}(e^{-1}(x), r). $$

LinearIsometryEquiv.preimage_closedBall theorem

(x : E₂) (r : ℝ) : e ⁻¹' Metric.closedBall x r = Metric.closedBall (e.symm x) r

Full source

@[simp]
theorem preimage_closedBall (x : E₂) (r : ℝ) :
    e ⁻¹' Metric.closedBall x r = Metric.closedBall (e.symm x) r :=
  e.toIsometryEquiv.preimage_closedBall x r

Preimage of Closed Ball under Semilinear Isometric Equivalence

Informal description

For any semilinear isometric equivalence $e \colon E \simeq_{\sigma_{12}} E_2$, point $x \in E_2$, and radius $r \geq 0$, the preimage of the closed ball $\overline{B}(x, r)$ under $e$ is equal to the closed ball $\overline{B}(e^{-1}(x), r)$ in $E$.

LinearIsometryEquiv.image_ball theorem

(x : E) (r : ℝ) : e '' Metric.ball x r = Metric.ball (e x) r

Full source

@[simp]
theorem image_ball (x : E) (r : ℝ) : e '' Metric.ball x r = Metric.ball (e x) r :=
  e.toIsometryEquiv.image_ball x r

Image of Open Ball under Semilinear Isometric Equivalence

Informal description

Let $E$ and $E_2$ be seminormed vector spaces, and let $e \colon E \simeq_{\sigma_{12}} E_2$ be a semilinear isometric equivalence. For any point $x \in E$ and radius $r > 0$, the image under $e$ of the open ball centered at $x$ with radius $r$ is equal to the open ball centered at $e(x)$ with radius $r$ in $E_2$. That is, $$ e(B(x, r)) = B(e(x), r). $$

LinearIsometryEquiv.image_sphere theorem

(x : E) (r : ℝ) : e '' Metric.sphere x r = Metric.sphere (e x) r

Full source

@[simp]
theorem image_sphere (x : E) (r : ℝ) : e '' Metric.sphere x r = Metric.sphere (e x) r :=
  e.toIsometryEquiv.image_sphere x r

Image of Sphere under Semilinear Isometric Equivalence

Informal description

Let $E$ and $E_2$ be seminormed additive commutative groups with module structures over rings $R$ and $R_2$ respectively, and let $e : E \simeq_{\sigma_{12}} E_2$ be a semilinear isometric equivalence. For any point $x \in E$ and radius $r \in \mathbb{R}$, the image of the sphere $\{y \in E \mid \|y - x\| = r\}$ under $e$ is equal to the sphere $\{z \in E_2 \mid \|z - e(x)\| = r\}$ centered at $e(x)$ with radius $r$ in $E_2$.

LinearIsometryEquiv.image_closedBall theorem

(x : E) (r : ℝ) : e '' Metric.closedBall x r = Metric.closedBall (e x) r

Full source

@[simp]
theorem image_closedBall (x : E) (r : ℝ) : e '' Metric.closedBall x r = Metric.closedBall (e x) r :=
  e.toIsometryEquiv.image_closedBall x r

Image of Closed Ball under Semilinear Isometric Equivalence

Informal description

Let $e \colon E \simeq_{\sigma_{12}} E_2$ be a semilinear isometric equivalence between seminormed modules. For any point $x \in E$ and radius $r \geq 0$, the image under $e$ of the closed ball centered at $x$ with radius $r$ is equal to the closed ball centered at $e(x)$ with radius $r$ in $E_2$. That is, $$ e(\overline{B}(x, r)) = \overline{B}(e(x), r). $$

LinearIsometryEquiv.comp_continuousOn_iff theorem

{f : α → E} {s : Set α} : ContinuousOn (e ∘ f) s ↔ ContinuousOn f s

Full source

@[simp]
theorem comp_continuousOn_iff {f : α → E} {s : Set α} : ContinuousOnContinuousOn (e ∘ f) s ↔ ContinuousOn f s :=
  e.isometry.comp_continuousOn_iff

Composition with Semilinear Isometric Equivalence Preserves Continuity on Subset

Informal description

Let $e \colon E \simeq_{\sigma_{12}} E_2$ be a semilinear isometric equivalence between seminormed modules, and let $f \colon \alpha \to E$ be a function defined on a topological space $\alpha$ with a subset $s \subseteq \alpha$. Then the composition $e \circ f$ is continuous on $s$ if and only if $f$ is continuous on $s$.

LinearIsometryEquiv.comp_continuous_iff theorem

{f : α → E} : Continuous (e ∘ f) ↔ Continuous f

Full source

@[simp]
theorem comp_continuous_iff {f : α → E} : ContinuousContinuous (e ∘ f) ↔ Continuous f :=
  e.isometry.comp_continuous_iff

Continuity of Composition with Semilinear Isometric Equivalence

Informal description

For any function $f \colon \alpha \to E$, the composition $e \circ f$ is continuous if and only if $f$ is continuous, where $e \colon E \simeq_{\sigma_{12}} E_2$ is a semilinear isometric equivalence between seminormed modules.

LinearIsometryEquiv.completeSpace_map instance

(p : Submodule R E) [CompleteSpace p] : CompleteSpace (p.map (e.toLinearEquiv : E →ₛₗ[σ₁₂] E₂))

Full source

instance completeSpace_map (p : Submodule R E) [CompleteSpace p] :
    CompleteSpace (p.map (e.toLinearEquiv : E →ₛₗ[σ₁₂] E₂)) :=
  e.toLinearIsometry.completeSpace_map' p

Completeness Preservation under Semilinear Isometric Equivalence

Informal description

For any complete submodule $p$ of a seminormed module $E$, the image of $p$ under a semilinear isometric equivalence $e \colon E \simeq_{\sigma_{12}} E_2$ is also a complete space.

LinearIsometryEquiv.ofSurjective definition

(f : F →ₛₗᵢ[σ₁₂] E₂) (hfr : Function.Surjective f) : F ≃ₛₗᵢ[σ₁₂] E₂

Full source

/-- Construct a linear isometry equiv from a surjective linear isometry. -/
noncomputable def ofSurjective (f : F →ₛₗᵢ[σ₁₂] E₂) (hfr : Function.Surjective f) :
    F ≃ₛₗᵢ[σ₁₂] E₂ :=
  { LinearEquiv.ofBijective f.toLinearMap ⟨f.injective, hfr⟩ with norm_map' := f.norm_map }

Semilinear isometric equivalence from a surjective isometric embedding

Informal description

Given a surjective semilinear isometric embedding $ f : F \to E₂ $ between seminormed modules, the function constructs a semilinear isometric equivalence $ F \simeq_{σ₁₂} E₂ $. This equivalence preserves the norm, i.e., $ \|f(x)\| = \|x\| $ for all $ x \in F $.

LinearIsometryEquiv.coe_ofSurjective theorem

(f : F →ₛₗᵢ[σ₁₂] E₂) (hfr : Function.Surjective f) : ⇑(LinearIsometryEquiv.ofSurjective f hfr) = f

Full source

@[simp]
theorem coe_ofSurjective (f : F →ₛₗᵢ[σ₁₂] E₂) (hfr : Function.Surjective f) :
    ⇑(LinearIsometryEquiv.ofSurjective f hfr) = f := by
  ext
  rfl

Underlying Function of Semilinear Isometric Equivalence from Surjective Embedding Equals Original Function

Informal description

Let $F$ and $E_2$ be seminormed modules over rings $R$ and $R_2$ respectively, with a ring homomorphism $\sigma_{12} : R \to R_2$. Given a surjective $\sigma_{12}$-semilinear isometric embedding $f : F \to E_2$, the underlying function of the semilinear isometric equivalence constructed from $f$ via `LinearIsometryEquiv.ofSurjective` is equal to $f$ itself. That is, $\operatorname{toFun} (\text{ofSurjective}\, f\, \text{hfr}) = f$.

LinearIsometryEquiv.ofLinearIsometry definition

 (f : E →ₛₗᵢ[σ₁₂] E₂) (g : E₂ →ₛₗ[σ₂₁] E) (h₁ : f.toLinearMap.comp g = LinearMap.id)
  (h₂ : g.comp f.toLinearMap = LinearMap.id) : E ≃ₛₗᵢ[σ₁₂] E₂

Full source

/-- If a linear isometry has an inverse, it is a linear isometric equivalence. -/
def ofLinearIsometry (f : E →ₛₗᵢ[σ₁₂] E₂) (g : E₂ →ₛₗ[σ₂₁] E)
    (h₁ : f.toLinearMap.comp g = LinearMap.id) (h₂ : g.comp f.toLinearMap = LinearMap.id) :
    E ≃ₛₗᵢ[σ₁₂] E₂ :=
  { toLinearEquiv := LinearEquiv.ofLinear f.toLinearMap g h₁ h₂
    norm_map' := fun x => f.norm_map x }

Semilinear isometric equivalence from inverse semilinear maps

Informal description

Given a semilinear isometric embedding $ f \colon E \to E_2 $ and a semilinear map $ g \colon E_2 \to E $ such that $ f \circ g = \text{id} $ and $ g \circ f = \text{id} $, this constructs a semilinear isometric equivalence $ E \simeq_{\sigma_{12}} E_2 $. The equivalence preserves the norm, i.e., $ \|f(x)\| = \|x\| $ for all $ x \in E $.

LinearIsometryEquiv.coe_ofLinearIsometry theorem

 (f : E →ₛₗᵢ[σ₁₂] E₂) (g : E₂ →ₛₗ[σ₂₁] E) (h₁ : f.toLinearMap.comp g = LinearMap.id)
  (h₂ : g.comp f.toLinearMap = LinearMap.id) : (ofLinearIsometry f g h₁ h₂ : E → E₂) = (f : E → E₂)

Full source

@[simp]
theorem coe_ofLinearIsometry (f : E →ₛₗᵢ[σ₁₂] E₂) (g : E₂ →ₛₗ[σ₂₁] E)
    (h₁ : f.toLinearMap.comp g = LinearMap.id) (h₂ : g.comp f.toLinearMap = LinearMap.id) :
    (ofLinearIsometry f g h₁ h₂ : E → E₂) = (f : E → E₂) :=
  rfl

Underlying Function of Semilinear Isometric Equivalence from Inverse Maps Equals Original Embedding

Informal description

Let $E$ and $E_2$ be seminormed modules over rings $R$ and $R_2$ respectively, with a ring homomorphism $\sigma_{12} \colon R \to R_2$. Given a $\sigma_{12}$-semilinear isometric embedding $f \colon E \to E_2$ and a $\sigma_{21}$-semilinear map $g \colon E_2 \to E$ (where $\sigma_{21} \colon R_2 \to R$ is the inverse homomorphism) such that $f \circ g = \text{id}$ and $g \circ f = \text{id}$, the underlying function of the semilinear isometric equivalence constructed from $f$ and $g$ via `ofLinearIsometry` equals $f$ itself. That is, $\text{ofLinearIsometry}\, f\, g\, h_1\, h_2 = f$ as functions from $E$ to $E_2$.

LinearIsometryEquiv.coe_ofLinearIsometry_symm theorem

 (f : E →ₛₗᵢ[σ₁₂] E₂) (g : E₂ →ₛₗ[σ₂₁] E) (h₁ : f.toLinearMap.comp g = LinearMap.id)
  (h₂ : g.comp f.toLinearMap = LinearMap.id) : ((ofLinearIsometry f g h₁ h₂).symm : E₂ → E) = (g : E₂ → E)

Full source

@[simp]
theorem coe_ofLinearIsometry_symm (f : E →ₛₗᵢ[σ₁₂] E₂) (g : E₂ →ₛₗ[σ₂₁] E)
    (h₁ : f.toLinearMap.comp g = LinearMap.id) (h₂ : g.comp f.toLinearMap = LinearMap.id) :
    ((ofLinearIsometry f g h₁ h₂).symm : E₂ → E) = (g : E₂ → E) :=
  rfl

Inverse of Semilinear Isometric Equivalence Construction Equals Given Inverse Map

Informal description

Let $E$ and $E_2$ be seminormed additive commutative groups with module structures over rings $R$ and $R_2$ respectively, and let $\sigma_{12} : R \to R_2$ and $\sigma_{21} : R_2 \to R$ be mutually inverse ring homomorphisms. Given a $\sigma_{12}$-semilinear isometric embedding $f : E \to E_2$ and a $\sigma_{21}$-semilinear map $g : E_2 \to E$ such that $f \circ g = \text{id}$ and $g \circ f = \text{id}$, the inverse of the semilinear isometric equivalence $\text{ofLinearIsometry}(f, g, h_1, h_2) : E \simeq_{\sigma_{12}} E_2$ is equal to $g$ as a function from $E_2$ to $E$.

LinearIsometryEquiv.neg definition

: E ≃ₗᵢ[R] E

Full source

/-- The negation operation on a normed space `E`, considered as a linear isometry equivalence. -/
def neg : E ≃ₗᵢ[R] E :=
  { LinearEquiv.neg R with norm_map' := norm_neg }

Negation as a linear isometry equivalence

Informal description

The negation operation on a normed space $E$, considered as a linear isometry equivalence, is the map $x \mapsto -x$ that preserves the norm (i.e., $\| -x \| = \|x\|$ for all $x \in E$).

LinearIsometryEquiv.coe_neg theorem

: (neg R : E → E) = fun x => -x

Full source

@[simp]
theorem coe_neg : (neg R : E → E) = fun x => -x :=
  rfl

Negation as a Linear Isometry Equivalence: $x \mapsto -x$

Informal description

For a normed space $E$ over a ring $R$, the negation operation as a linear isometry equivalence is given by the function $x \mapsto -x$.

LinearIsometryEquiv.symm_neg theorem

: (neg R : E ≃ₗᵢ[R] E).symm = neg R

Full source

@[simp]
theorem symm_neg : (neg R : E ≃ₗᵢ[R] E).symm = neg R :=
  rfl

Inverse of Negation Isometry Equals Itself

Informal description

For a normed space $E$ over a ring $R$, the inverse of the negation map (as a linear isometry equivalence) is equal to itself, i.e., $(\text{neg}_R)^{-1} = \text{neg}_R$.

LinearIsometryEquiv.prodAssoc definition

[Module R E₂] [Module R E₃] : (E × E₂) × E₃ ≃ₗᵢ[R] E × E₂ × E₃

Full source

/-- The natural equivalence `(E × E₂) × E₃ ≃ E × (E₂ × E₃)` is a linear isometry. -/
def prodAssoc [Module R E₂] [Module R E₃] : (E × E₂) × E₃(E × E₂) × E₃ ≃ₗᵢ[R] E × E₂ × E₃ :=
  { LinearEquiv.prodAssoc R E E₂ E₃ with
    norm_map' := by
      rintro ⟨⟨e, f⟩, g⟩
      simp only [LinearEquiv.prodAssoc_apply, AddEquiv.toEquiv_eq_coe,
        Equiv.toFun_as_coe, EquivLike.coe_coe, AddEquiv.coe_prodAssoc,
        Equiv.prodAssoc_apply, Prod.norm_def, max_assoc] }

Associativity of products under linear isometric equivalence

Informal description

The natural equivalence $(E \times E_2) \times E_3 \simeq E \times (E_2 \times E_3)$ is a linear isometry, where $E$, $E_2$, and $E_3$ are seminormed vector spaces over the same ring $R$. This means the equivalence preserves both the linear structure and the norm.

LinearIsometryEquiv.coe_prodAssoc theorem

 [Module R E₂] [Module R E₃] : (prodAssoc R E E₂ E₃ : (E × E₂) × E₃ → E × E₂ × E₃) = Equiv.prodAssoc E E₂ E₃

Full source

@[simp]
theorem coe_prodAssoc [Module R E₂] [Module R E₃] :
    (prodAssoc R E E₂ E₃ : (E × E₂) × E₃ → E × E₂ × E₃) = Equiv.prodAssoc E E₂ E₃ :=
  rfl

Underlying Function of Associative Linear Isometric Equivalence Equals Standard Associativity Equivalence

Informal description

Let $E$, $E_2$, and $E_3$ be seminormed vector spaces over a ring $R$. The underlying function of the linear isometric equivalence $\text{prodAssoc}_R E E_2 E_3 : (E \times E_2) \times E_3 \simeq_{R} E \times (E_2 \times E_3)$ is equal to the standard associativity equivalence $\text{Equiv.prodAssoc} E E_2 E_3$ that reassociates the components of the product.

LinearIsometryEquiv.coe_prodAssoc_symm theorem

 [Module R E₂] [Module R E₃] :
  ((prodAssoc R E E₂ E₃).symm : E × E₂ × E₃ → (E × E₂) × E₃) = (Equiv.prodAssoc E E₂ E₃).symm

Full source

@[simp]
theorem coe_prodAssoc_symm [Module R E₂] [Module R E₃] :
    ((prodAssoc R E E₂ E₃).symm : E × E₂ × E₃ → (E × E₂) × E₃) = (Equiv.prodAssoc E E₂ E₃).symm :=
  rfl

Inverse of Linear Isometric Associativity Equivalence Equals Standard Inverse

Informal description

Let $E$, $E₂$, and $E₃$ be seminormed vector spaces over a ring $R$ with module structures. The inverse of the linear isometric equivalence $(E \times E₂) \times E₃ \simeq_{R} E \times (E₂ \times E₃)$ is equal to the inverse of the standard associativity equivalence $(E \times E₂) \times E₃ \simeq E \times (E₂ \times E₃)$ as functions.

LinearIsometryEquiv.ofTop definition

{R : Type*} [Ring R] [Module R E] (p : Submodule R E) (hp : p = ⊤) : p ≃ₗᵢ[R] E

Full source

/-- If `p` is a submodule that is equal to `⊤`, then `LinearIsometryEquiv.ofTop p hp` is the
"identity" equivalence between `p` and `E`. -/
@[simps! toLinearEquiv apply symm_apply_coe]
def ofTop {R : Type*} [Ring R] [Module R E] (p : Submodule R E) (hp : p = ⊤) : p ≃ₗᵢ[R] E :=
  { p.subtypeₗᵢ with toLinearEquiv := LinearEquiv.ofTop p hp }

Identity linear isometric equivalence for the top submodule

Informal description

Given a submodule $p$ of a normed module $E$ over a ring $R$ such that $p$ is equal to the entire space (i.e., $p = \top$), the function `LinearIsometryEquiv.ofTop p hp` constructs a linear isometric equivalence between $p$ and $E$. This equivalence is the identity map when viewed as a map from $p$ to $E$, preserving both the linear structure and the norm.

LinearIsometryEquiv.ofEq definition

(hpq : p = q) : p ≃ₗᵢ[R'] q

Full source

/-- `LinearEquiv.ofEq` as a `LinearIsometryEquiv`. -/
def ofEq (hpq : p = q) : p ≃ₗᵢ[R'] q :=
  { LinearEquiv.ofEq p q hpq with norm_map' := fun _ => rfl }

Linear isometric equivalence between equal submodules

Informal description

Given two equal submodules $p$ and $q$ of a normed module over a ring $R'$, the function `LinearIsometryEquiv.ofEq p q hpq` constructs a linear isometric equivalence between $p$ and $q$, where $hpq$ is a proof that $p = q$. This equivalence preserves both the linear structure and the norm, and is essentially the identity map when viewed as a map from $p$ to $q$.

LinearIsometryEquiv.coe_ofEq_apply theorem

(h : p = q) (x : p) : (ofEq p q h x : E) = x

Full source

@[simp]
theorem coe_ofEq_apply (h : p = q) (x : p) : (ofEq p q h x : E) = x :=
  rfl

Identity Action of Linear Isometric Equivalence Between Equal Submodules

Informal description

Let $p$ and $q$ be submodules of a normed module over a ring $R'$ such that $p = q$ (with proof $h$). For any element $x \in p$, the image of $x$ under the linear isometric equivalence $\text{ofEq } p q h$ (when viewed as an element of the ambient module $E$) is equal to $x$ itself. In other words, the map $\text{ofEq } p q h$ acts as the identity on elements of $p$.

LinearIsometryEquiv.ofEq_symm theorem

(h : p = q) : (ofEq p q h).symm = ofEq q p h.symm

Full source

@[simp]
theorem ofEq_symm (h : p = q) : (ofEq p q h).symm = ofEq q p h.symm :=
  rfl

Symmetry of Linear Isometric Equivalence Between Equal Submodules

Informal description

Given two equal submodules $p$ and $q$ of a normed module over a ring $R'$ with equality proof $h : p = q$, the inverse of the linear isometric equivalence $\text{ofEq } p q h$ is equal to the linear isometric equivalence $\text{ofEq } q p h^{-1}$, where $h^{-1}$ is the symmetric equality proof $q = p$.

LinearIsometryEquiv.ofEq_rfl theorem

: ofEq p p rfl = LinearIsometryEquiv.refl R' p

Full source

@[simp]
theorem ofEq_rfl : ofEq p p rfl = LinearIsometryEquiv.refl R' p := rfl

Identity of Linear Isometric Equivalence for Reflexive Equality

Informal description

The linear isometric equivalence constructed between a submodule $p$ and itself (via reflexivity) is equal to the identity linear isometric equivalence on $p$.

Basis.ext_linearIsometry theorem

 {ι : Type*} (b : Basis ι R E) {f₁ f₂ : E →ₛₗᵢ[σ₁₂] E₂} (h : ∀ i, f₁ (b i) = f₂ (b i)) : f₁ = f₂

Full source

/-- Two linear isometries are equal if they are equal on basis vectors. -/
theorem Basis.ext_linearIsometry {ι : Type*} (b : Basis ι R E) {f₁ f₂ : E →ₛₗᵢ[σ₁₂] E₂}
    (h : ∀ i, f₁ (b i) = f₂ (b i)) : f₁ = f₂ :=
  LinearIsometry.toLinearMap_injective <| b.ext h

Equality of Semilinear Isometries on Basis Vectors

Informal description

Let $E$ and $E_2$ be seminormed modules over rings $R$ and $R_2$ respectively, with $\sigma_{12} : R \to R_2$ a ring homomorphism. Given a basis $b$ of $E$ indexed by $\iota$, and two $\sigma_{12}$-semilinear isometric embeddings $f_1, f_2 : E \to E_2$, if $f_1(b(i)) = f_2(b(i))$ for all basis vectors $b(i)$, then $f_1 = f_2$.

Basis.ext_linearIsometryEquiv theorem

 {ι : Type*} (b : Basis ι R E) {f₁ f₂ : E ≃ₛₗᵢ[σ₁₂] E₂} (h : ∀ i, f₁ (b i) = f₂ (b i)) : f₁ = f₂

Full source

/-- Two linear isometric equivalences are equal if they are equal on basis vectors. -/
theorem Basis.ext_linearIsometryEquiv {ι : Type*} (b : Basis ι R E) {f₁ f₂ : E ≃ₛₗᵢ[σ₁₂] E₂}
    (h : ∀ i, f₁ (b i) = f₂ (b i)) : f₁ = f₂ :=
  LinearIsometryEquiv.toLinearEquiv_injective <| b.ext' h

Equality of Semilinear Isometric Equivalences on Basis Vectors

Informal description

Let $E$ and $E_2$ be seminormed vector spaces over rings $R$ and $R_2$ respectively, with a ring homomorphism $\sigma_{12} : R \to R_2$ and its inverse $\sigma_{21} : R_2 \to R$. Given a basis $b$ of $E$ indexed by $\iota$, and two semilinear isometric equivalences $f_1, f_2 : E \simeq_{\sigma_{12}} E_2$, if $f_1(b(i)) = f_2(b(i))$ for all basis vectors $b(i)$, then $f_1 = f_2$.

LinearIsometry.equivRange definition

 {R S : Type*} [Semiring R] [Ring S] [Module S E] [Module R F] {σ₁₂ : R →+* S} {σ₂₁ : S →+* R} [RingHomInvPair σ₁₂ σ₂₁]
  [RingHomInvPair σ₂₁ σ₁₂] (f : F →ₛₗᵢ[σ₁₂] E) : F ≃ₛₗᵢ[σ₁₂] (LinearMap.range f.toLinearMap)

Full source

/-- Reinterpret a `LinearIsometry` as a `LinearIsometryEquiv` to the range. -/
@[simps! apply_coe]
noncomputable def LinearIsometry.equivRange {R S : Type*} [Semiring R] [Ring S] [Module S E]
    [Module R F] {σ₁₂ : R →+* S} {σ₂₁ : S →+* R} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂]
    (f : F →ₛₗᵢ[σ₁₂] E) : F ≃ₛₗᵢ[σ₁₂] (LinearMap.range f.toLinearMap) :=
  { f with toLinearEquiv := LinearEquiv.ofInjective f.toLinearMap f.injective }

Semilinear isometric equivalence to the range of an embedding

Informal description

Given a semilinear isometric embedding $f : F \to E$ between modules $F$ and $E$ over rings $R$ and $S$ respectively, with ring homomorphisms $\sigma_{12} : R \to S$ and $\sigma_{21} : S \to R$ forming a pair of mutual inverses, the function `LinearIsometry.equivRange` constructs a semilinear isometric equivalence between $F$ and the range of $f$ (viewed as a submodule of $E$). This equivalence is obtained by restricting the codomain of $f$ to its range and using the injectivity of $f$.