LinearIsometry.injective
theorem LinearIsometry.injective :
∀ {R : Type u_1} {R₂ : Type u_2} {E₂ : Type u_6} {F : Type u_9} [inst : Semiring R] [inst_1 : Semiring R₂]
{σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E₂] [inst_3 : Module R₂ E₂] [inst_4 : NormedAddCommGroup F]
[inst_5 : Module R F] (f₁ : F →ₛₗᵢ[σ₁₂] E₂), Function.Injective ⇑f₁
The theorem `LinearIsometry.injective` states that for any semirings `R` and `R₂`, any seminormed additive commutative group `E₂`, any normed additive commutative group `F`, any module over `R₂` on `E₂`, any module over `R` on `F`, and any linear isometry `f₁` from `F` to `E₂` with ring homomorphism `σ₁₂` from `R` to `R₂`, the corresponding function `f₁` is injective. In other words, if `f₁ x = f₁ y` then `x = y` for any `x` and `y` in `F`. This theorem is a fundamental property of linear isometries in the context of semirings, seminormed additive commutative groups, normed additive commutative groups, and modules.
More concisely: Given any linear isometry `f₁` from a normed additive commutative group `F` to a seminormed additive commutative group `E₂` with compatible ring homomorphisms, `f₁` is injective.
|
LinearIsometryEquiv.symm_apply_apply
theorem LinearIsometryEquiv.symm_apply_apply :
∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
{σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
[inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E]
[inst_7 : Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E), e.symm (e x) = x
This theorem states that for any semiring `R`, another semiring `R₂`, types `E` and `E₂` representing seminormed add commutative groups, and two ring homomorphisms `σ₁₂` and `σ₂₁` that form a pair of inverse homomorphisms between `R` and `R₂`, if `e` is a linear isometry equivalence between `E` and `E₂` with respect to `σ₁₂`, then applying the inverse of this equivalence to the result of applying the equivalence to any element `x` from `E` returns the original element `x`. In simpler terms, the theorem states that the inverse operation of a linear isometry equivalence undoes the effect of the original operation.
More concisely: Given semirings `R` and `R₂`, seminormed add commutative groups `E` and `E₂`, ring homomorphisms σ₁₂ and σ₂₁ forming a pair of inverse homomorphisms between `R` and `R₂`, and a linear isometry equivalence `e` between `E` and `E₂`, for all `x` in `E`, `e⁻¹(e(x)) = x`.
|
LinearIsometry.isometry
theorem LinearIsometry.isometry :
∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
{σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
[inst_5 : Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂), Isometry ⇑f
The theorem asserts that a linear isometry between two seminormed add commutative groups, which are also modules over semirings, preserves the extended distance between points. In other words, for any semirings `R` and `R₂`, any seminormed add commutative groups `E` and `E₂`, any module structures on `E` over `R` and on `E₂` over `R₂`, and any ring homomorphism `σ₁₂` from `R` to `R₂`, if `f` is a linear isometry from `E` to `E₂` then the function `f` is an isometry. Here, an isometry is defined as a map which preserves the extended distance between points in the pseudoemetric space sense.
More concisely: A linear isometry between two seminormed add commutative groups, equipped with module structures over compatible semirings, preserves the extended distances between points.
|
Basis.ext_linearIsometry
theorem Basis.ext_linearIsometry :
∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
{σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
[inst_5 : Module R₂ E₂] {ι : Type u_11} (b : Basis ι R E) {f₁ f₂ : E →ₛₗᵢ[σ₁₂] E₂},
(∀ (i : ι), f₁ (b i) = f₂ (b i)) → f₁ = f₂
The theorem `Basis.ext_linearIsometry` states that for any two linear isometries `f₁` and `f₂` from a vector space `E` over a semiring `R` to a vector space `E₂` over a semiring `R₂`, if they are equal on basis vectors of `E`, then `f₁` and `f₂` are equal. Here, `E` and `E₂` are seminormed add commutative groups, `R` and `R₂` are semirings, and `σ₁₂` is a ring homomorphism from `R` to `R₂`. The basis of `E` is indexed by some type `ι`.
More concisely: If `f₁` and `f₂` are linear isometries from a seminormed add commutative group `E` over semiring `R` to `E₂` over semiring `R₂`, and `f₁` and `f₂` agree on the basis vectors of `E` indexed by type `ι`, then `f₁` and `f₂` are equal.
|
LinearIsometryEquiv.instCoeTCContinuousLinearEquiv.proof_1
theorem LinearIsometryEquiv.instCoeTCContinuousLinearEquiv.proof_1 :
∀ {R : Type u_4} {R₂ : Type u_3} {E : Type u_2} {E₂ : Type u_1} [inst : Semiring R] [inst_1 : Semiring R₂]
{σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
[inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E]
[inst_7 : Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂), Continuous ⇑e.toIsometryEquiv.symm
This theorem states that for any semirings `R` and `R₂`, seminormed add commutative groups `E` and `E₂`, and bijective ring homomorphisms `σ₁₂ : R →+* R₂` and `σ₂₁ : R₂ →+* R` that form inverse pairs, if we have a linear isometry equivalence `e` from `E` to `E₂` over the ring homomorphism `σ₁₂`, then the function defined by the inverse of this linear isometry equivalence (converted to an isometric equivalence) is continuous. In other words, linear isometry equivalences and their inverses preserve continuity.
More concisely: If `σ₁₂` and `σ₂₁` are inverse bijective ring homomorphisms between semirings `R` and `R₂`, and `e` is a linear isometry equivalence from a seminormed add commutative group `E` to `E₂` over `σ₁₂`, then the inverse of `e` is a continuous function from `E₂` to `E`.
|
LinearIsometry.ext
theorem LinearIsometry.ext :
∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
{σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
[inst_5 : Module R₂ E₂] {f g : E →ₛₗᵢ[σ₁₂] E₂}, (∀ (x : E), f x = g x) → f = g
The theorem `LinearIsometry.ext` states that for any two linear isometries `f` and `g` from a seminormed add-commutative group `E` over a semiring `R` to a seminormed add-commutative group `E₂` over a semiring `R₂`, with the linear map from `R` to `R₂` denoted by `σ₁₂`, if `f` and `g` are equal at every point in `E`, then `f` and `g` are equal. In simpler terms, if two linear isometries produce the same result for every input, they are the same linear isometry.
More concisely: If two linear isometries from a seminormed add-commutative group over semirings to another such group, with compatible linear maps between the semirings, agree on every point, then they are equal.
|
LinearIsometryEquiv.refl_trans
theorem LinearIsometryEquiv.refl_trans :
∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
{σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
[inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E]
[inst_7 : Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂), (LinearIsometryEquiv.refl R E).trans e = e
The theorem `LinearIsometryEquiv.refl_trans` states that for any semirings `R` and `R₂`, seminormed additive commutative groups `E` and `E₂`, pair of ring homomorphisms `σ₁₂` and `σ₂₁` that are inverses of each other, and modules `E` over `R` and `E₂` over `R₂`, the composition of a linear isometry equivalence `e : E ≃ₛₗᵢ[σ₁₂] E₂` with the identity linear isometry equivalence on `E` is `e` itself. In other words, applying the identity map first does not change the result of the linear isometry equivalence `e`.
More concisely: For any seminormed additive commutative groups `E` and `E₂`, semirings `R` and `R₂`, ring homomorphisms `σ₁₂` and `σ₂₁` that are inverses of each other, and modules `E` over `R` and `E₂` over `R₂`, the linear isometry equivalence `e : E ≃ₛₗᵢ[σ₁₂] E₂` satisfies `e ∘ id = e`, where `id` is the identity linear isometry equivalence on `E`.
|
Basis.ext_linearIsometryEquiv
theorem Basis.ext_linearIsometryEquiv :
∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
{σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
[inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E]
[inst_7 : Module R₂ E₂] {ι : Type u_11} (b : Basis ι R E) {f₁ f₂ : E ≃ₛₗᵢ[σ₁₂] E₂},
(∀ (i : ι), f₁ (b i) = f₂ (b i)) → f₁ = f₂
This theorem states that if there are two linear isometric equivalences between two seminormed add commutative groups with respective semirings, and if these two equivalences are both equal when applied to all basis vectors from a given basis of the first seminormed add commutative group, then these two equivalences are also equal to each other.
More concisely: If two linear isometric embeddings between seminormed additive commutative groups agree on a basis, they are equal.
|
SemilinearIsometryClass.isometry
theorem SemilinearIsometryClass.isometry :
∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [inst : Semiring R]
[inst_1 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂]
[inst_4 : Module R E] [inst_5 : Module R₂ E₂] [inst_6 : FunLike 𝓕 E E₂]
[inst : SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕), Isometry ⇑f
The theorem `SemilinearIsometryClass.isometry` states that, for any semiring `R`, a second semiring `R₂`, types `E` and `E₂`, and a type `𝓕`, given instances of `E` and `E₂` as seminormed additive commutative groups, `R` and `R₂` as modules over `E` and `E₂` respectively, `𝓕` as a function-like from `E` to `E₂`, and a semilinear isometry class on `𝓕`, `σ₁₂`, `E`, and `E₂`, any function `f` of type `𝓕` is an isometry. In other words, it preserves the edistance (extended distance) between the points in the pseudometric spaces `E` and `E₂`, i.e., the distance between the images of any two points under `f` is the same as the distance between the points themselves.
More concisely: Given seminormed additive commutative groups `E` and `E₂`, semirings `R` and `R₂`, a semilinear isometry class `σ₁₂` on a function-like map `𝓕` from `E` to `E₂`, if `𝓕` is a semilinear isometry between `E` and `𝓕(E)` with respect to `σ₁₂`, then for any `f` in the isometry class of `𝓕`, the extended distance `d₂(f(x), f(y)) = d₁(x, y)` holds for all `x, y` in `E`.
|
LinearIsometryEquiv.norm_map
theorem LinearIsometryEquiv.norm_map :
∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
{σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
[inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E]
[inst_7 : Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E), ‖e x‖ = ‖x‖
This theorem states that for any types `R`, `R₂`, `E`, and `E₂`, given two semirings `R` and `R₂`, two ring homomorphisms `σ₁₂` and `σ₂₁` that form a pair of inverse homomorphisms, two seminormed additive commutative groups `E` and `E₂`, `R` and `R₂` modules over `E` and `E₂`, and a linear isometry equivalence `e` between `E` and `E₂`, the norm of the image of any element `x` under `e` is equal to the norm of `x`. In other words, the linear isometry equivalence preserves norms.
More concisely: Given semirings R and R₂, ring homomorphisms σ₁₂ and σ₂₁ that form a pair of inverse homomorphisms, seminormed additive commutative groups E and E₂ with linear isometry equivalence e between them, and modules M over E and M₂ over E₂: For all x in E, ||ex|| = ||x||, where ||.|| denotes the norm.
|
LinearIsometryEquiv.toLinearEquiv_injective
theorem LinearIsometryEquiv.toLinearEquiv_injective :
∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
{σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
[inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E]
[inst_7 : Module R₂ E₂], Function.Injective LinearIsometryEquiv.toLinearEquiv
The theorem `LinearIsometryEquiv.toLinearEquiv_injective` states that for any two types `R` and `R₂` with semiring structures, two types `E` and `E₂` with seminormed add commutative group structures and modules over `R` and `R₂` respectively, and given a pair of inverse ring homomorphisms `σ₁₂` from `R` to `R₂` and `σ₂₁` from `R₂` to `R`, the function that converts a linear isometry equivalence to a linear equivalence (`LinearIsometryEquiv.toLinearEquiv`) is injective. In other words, if two linear isometry equivalences convert to the same linear equivalence, they were the same linear isometry equivalence to begin with.
More concisely: Given two linear isometry equivalences between seminormed add commutative groups with modules over commutative semirings, if their conversions to linear equivalences are equal, then the original isometries are equal.
|
LinearIsometry.norm_map
theorem LinearIsometry.norm_map :
∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
{σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
[inst_5 : Module R₂ E₂] (f : E →ₛₗᵢ[σ₁₂] E₂) (x : E), ‖f x‖ = ‖x‖
This theorem states that for any semiring R, other semiring R₂, types E and E₂, a semiring homomorphism σ₁₂ from R to R₂, and given that E and E₂ are seminormed additive commutative groups and also modules over R and R₂ respectively, a linear isometry `f` (which is a linear map preserving distances) from E to E₂ preserves the norm. In other words, the norm of the image of any element `x` of E under `f` is equal to the norm of `x` itself.
More concisely: Given semiring homomorphisms σ₁₂ : R → R₂, seminormed additive commutative groups and R-modules E and E₂, and a linear isometry f : E → E₂ between them, the norm of f(x) equals the norm of x for all x in E.
|
LinearIsometry.toLinearMap_injective
theorem LinearIsometry.toLinearMap_injective :
∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
{σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
[inst_5 : Module R₂ E₂], Function.Injective LinearIsometry.toLinearMap
This theorem states that for any two types `R` and `R₂` that are semirings, a ring homomorphism `σ₁₂` from `R` to `R₂`, two types `E` and `E₂` that are seminormed additive commutative groups and also modules over `R` and `R₂` respectively, the function `toLinearMap` that converts a `LinearIsometry` from `E` to `E₂` (preserving the linear structure and the distance) into a `LinearMap` (preserving only the linear structure) is injective. In other words, if two `LinearIsometry` objects are mapped to the same `LinearMap` by `toLinearMap`, then those two `LinearIsometry` objects were originally identical.
More concisely: Given semirings R and R₂, ring homomorphisms σ₁₂ from R to R₂, seminormed additive commutative groups and R-module E, E₂ with a given LinearIsometry f : E ≅ E₂, if toLinearMap(f) = toLinearMap(g) for some LinearIsometry g : E ≅ E₂, then f = g.
|
LinearIsometryEquiv.ext
theorem LinearIsometryEquiv.ext :
∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
{σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
[inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E]
[inst_7 : Module R₂ E₂] {e e' : E ≃ₛₗᵢ[σ₁₂] E₂}, (∀ (x : E), e x = e' x) → e = e'
The theorem `LinearIsometryEquiv.ext` states that for any two types `R` and `R₂` with semiring structures, types `E` and `E₂` with seminormed add commutative group structures and module structures over `R` and `R₂` respectively, and given ring homomorphisms `σ₁₂` and `σ₂₁` that form an inverse pair, if we have two linear isometric equivalences `e` and `e'` between `E` and `E₂` that are compatible with `σ₁₂`, and if these two equivalences map each element of `E` to the same element in `E₂`, then `e` and `e'` must be the same linear isometric equivalence.
More concisely: Given types `E` and `E₂` with seminormed add commutative group structures and module structures over semiring `R` and `R₂`, respectively, and given ring homomorphisms `σ₁₂` and `σ₂₁` with inverse pair, if there exist linear isometric equivalences `e` and `e'` between `E` and `E₂`, compatible with `σ₁₂`, mapping every element in `E` to the same image in `E₂`, then `e` and `e'` are equal.
|
LinearIsometryEquiv.coe_injective
theorem LinearIsometryEquiv.coe_injective :
∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
{σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
[inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E]
[inst_7 : Module R₂ E₂], Function.Injective DFunLike.coe
The theorem `LinearIsometryEquiv.coe_injective` states that for any two types `R` and `R₂` with semiring structures, any two types `E` and `E₂` with seminormed additive commutative group structures and module structures over `R` and `R₂` respectively, and any two ring homomorphisms `σ₁₂` and `σ₂₁` that form an inverse pair, the function `DFunLike.coe` is injective.
In other words, it means that if `DFunLike.coe` applied to two elements of its domain gives the same result, then these two elements were the same to begin with. This implies that no information is lost when mapping from the original space with `DFunLike.coe`.
More concisely: Given types `R`, `R₂` with semiring structures, types `E`, `E₂` with seminormed additive commutative group structures and module structures over `R` and `R₂` respectively, and ring homomorphisms `σ₁₂` and `σ₂₁` forming an inverse pair, the function `DFunLike.coe` from `E` to `E₂` is injective.
|
LinearIsometry.isComplete_image_iff
theorem LinearIsometry.isComplete_image_iff :
∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} {𝓕 : Type u_10} [inst : Semiring R]
[inst_1 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂]
[inst_4 : Module R E] [inst_5 : Module R₂ E₂] [inst_6 : FunLike 𝓕 E E₂]
[inst : SemilinearIsometryClass 𝓕 σ₁₂ E E₂] (f : 𝓕) {s : Set E}, IsComplete (⇑f '' s) ↔ IsComplete s
This theorem states that given several structures, including two semirings `R` and `R₂`, two seminormed additive commutative groups `E` and `E₂`, two modules `E` over `R` and `E₂` over `R₂`, a semilinear isometry class between `E` and `E₂`, and a function `f` from `E` to `E₂`, a set `s` in `E` is complete if and only if the image of `s` under the function `f` is complete. Here, a set is complete if every Cauchy filter that contains the set has a limit within the set.
More concisely: Given semirings R and R₂, seminormed additive commutative groups E and E₂, modules E over R and E₂ over R₂, a semilinear isometry between E and E₂, and a function f: E → E₂: For a set s ⊆ E, s is complete if and only if the image of s under f is complete.
|
LinearIsometryEquiv.isometry
theorem LinearIsometryEquiv.isometry :
∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
{σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
[inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E]
[inst_7 : Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂), Isometry ⇑e
This theorem states that for any linear isometry equivalence `e` between two semi-normed add-commutative groups `E` and `E₂`, over semirings `R` and `R₂` respectively, and with ring homomorphisms `σ₁₂` and `σ₂₁` between `R` and `R₂` (forming a ring homomorphism inverse pair in both directions), the function `e` preserves the pseudo metric space edistance. In other words, applying `e` to any two points in `E` will not change the edistance between them before and after the mapping, which makes `e` an isometry.
More concisely: For any linear isometry equivalence between semi-normed add-commutative groups with compatible ring homomorphism inverse pairs, the isometry preserves the group's pseudo-metric distance.
|
LinearIsometryEquiv.trans_refl
theorem LinearIsometryEquiv.trans_refl :
∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
{σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
[inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E]
[inst_7 : Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂), e.trans (LinearIsometryEquiv.refl R₂ E₂) = e
The theorem `LinearIsometryEquiv.trans_refl` states that for any semiring R, another semiring R₂, any types E and E₂, two ring homomorphisms σ₁₂ (from R to R₂) and σ₂₁ (from R₂ to R) which form a pair of inverse ring homomorphisms, any seminormed additive commutative groups E and E₂, and any modules E over R and E₂ over R₂; if we have a linear isometry equivalence (which is also a semilinear map) from E to E₂, then applying the transformation of this equivalence followed by the identity map on E₂ (which is also considered as a linear isometry equivalence) is the same as applying the original equivalence itself. In other words, applying a transformation followed by the identity transformation has no effect, it is equivalent to applying the original transformation.
More concisely: For any seminormed additive commutative groups E and E₂, and linear isometry equivalences between them that are also semilinear maps, the composition of the equivalence with the identity map on E₂ is equal to the original equivalence.
|
LinearIsometryEquiv.continuous
theorem LinearIsometryEquiv.continuous :
∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
{σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
[inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E]
[inst_7 : Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂), Continuous ⇑e
This theorem states that for any linear isometry equivalence `e` between two seminormed additive commutative group modules `E` and `E₂`, over semirings `R` and `R₂` respectively with ring homomorphism pairs `σ₁₂` and `σ₂₁`, the mapping defined by `e` is continuous. This means, intuitively, that small changes in the input to `e` result in small changes in its output, in the context of topological spaces - which in this case are the modules `E` and `E₂`.
More concisely: For any linear isometry equivalence between seminormed additive commutative group modules over commutative semirings with compatible ring homomorphisms, the equivalence is a continuous linear map between the modules.
|
LinearIsometryEquiv.injective
theorem LinearIsometryEquiv.injective :
∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
{σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
[inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E]
[inst_7 : Module R₂ E₂] (e : E ≃ₛₗᵢ[σ₁₂] E₂), Function.Injective ⇑e
The theorem `LinearIsometryEquiv.injective` states that for any two types `R` and `R₂`, which are semirings, any two types `E` and `E₂`, which are seminormed additive commutative groups and modules over `R` and `R₂` respectively, and given two ring homomorphisms `σ₁₂` from `R` to `R₂` and `σ₂₁` from `R₂` to `R`, that form an inverse pair, then for any linear isometry equivalence `e` between `E` and `E₂`, the function represented by `e` is injective. In other words, if `e` maps two elements in `E` to the same element in `E₂`, then the two original elements in `E` were the same.
More concisely: Given semirings R and R₂, seminormed additive commutative groups and modules E, E₂ over R and R₂ respectively, and ring homomorphisms σ₁₂ from R to R₂ and σ₂₁ from R₂ to R forming an inverse pair, any linear isometry e between E and E₂ implies that e is injective.
|