(Semi-)linear isometries #
In this file we define LinearIsometry σ₁₂ E E₂ (notation: E →ₛₗᵢ[σ₁₂] E₂) to be a semilinear
isometric embedding of E into E₂ and LinearIsometryEquiv (notation: E ≃ₛₗᵢ[σ₁₂] E₂) to be
a semilinear isometric equivalence between E and E₂. The notation for the associated purely
linear concepts is E →ₗᵢ[R] E₂, E ≃ₗᵢ[R] E₂, and E →ₗᵢ⋆[R] E₂, E ≃ₗᵢ⋆[R] E₂ for
the star-linear versions.
We also prove some trivial lemmas and provide convenience constructors.
Since a lot of elementary properties don't require ‖x‖ = 0 → x = 0 we start setting up the
theory for SeminormedAddCommGroup and we specialize to NormedAddCommGroup when needed.
structure
LinearIsometry
{R : Type u_1}
{R₂ : Type u_2}
[Semiring R]
[Semiring R₂]
(σ₁₂ : R →+* R₂)
(E : Type u_11)
(E₂ : Type u_12)
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
extends E →ₛₗ[σ₁₂] E₂ :
Type (max u_11 u_12)
A σ₁₂-semilinear isometric embedding of a normed R-module into an R₂-module.
- toFun : E → E₂
A σ₁₂-semilinear isometric embedding of a normed R-module into an R₂-module.
Equations
- One or more equations did not get rendered due to their size.
A linear isometric embedding of a normed R-module into another one.
Equations
- One or more equations did not get rendered due to their size.
An antilinear isometric embedding of a normed R-module into another one.
Equations
- One or more equations did not get rendered due to their size.
class
SemilinearIsometryClass
(𝓕 : Type u_11)
{R : outParam (Type u_12)}
{R₂ : outParam (Type u_13)}
[Semiring R]
[Semiring R₂]
(σ₁₂ : outParam (R →+* R₂))
(E : outParam (Type u_14))
(E₂ : outParam (Type u_15))
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
[FunLike 𝓕 E E₂]
extends SemilinearMapClass 𝓕 σ₁₂ E E₂ :
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.
- map_smulₛₗ : ∀ (f : 𝓕) (c : R) (x : E), f (c • x) = σ₁₂ c • f x
@[reducible, inline]
abbrev
LinearIsometryClass
(𝓕 : Type u_11)
(R : outParam (Type u_12))
(E : outParam (Type u_13))
(E₂ : outParam (Type u_14))
[Semiring R]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R E₂]
[FunLike 𝓕 E E₂]
:
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₂.
Equations
- LinearIsometryClass 𝓕 R E E₂ = SemilinearIsometryClass 𝓕 (RingHom.id R) E E₂
theorem
SemilinearIsometryClass.isometry
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
{𝓕 : Type u_10}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
[FunLike 𝓕 E E₂]
[SemilinearIsometryClass 𝓕 σ₁₂ E E₂]
(f : 𝓕)
:
Isometry ⇑f
theorem
SemilinearIsometryClass.continuous
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
{𝓕 : Type u_10}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
[FunLike 𝓕 E E₂]
[SemilinearIsometryClass 𝓕 σ₁₂ E E₂]
(f : 𝓕)
:
Continuous ⇑f
theorem
SemilinearIsometryClass.nnnorm_map
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
{𝓕 : Type u_10}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
[FunLike 𝓕 E E₂]
[SemilinearIsometryClass 𝓕 σ₁₂ E E₂]
(f : 𝓕)
(x : E)
:
theorem
SemilinearIsometryClass.lipschitz
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
{𝓕 : Type u_10}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
[FunLike 𝓕 E E₂]
[SemilinearIsometryClass 𝓕 σ₁₂ E E₂]
(f : 𝓕)
:
LipschitzWith 1 ⇑f
theorem
SemilinearIsometryClass.antilipschitz
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
{𝓕 : Type u_10}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
[FunLike 𝓕 E E₂]
[SemilinearIsometryClass 𝓕 σ₁₂ E E₂]
(f : 𝓕)
:
AntilipschitzWith 1 ⇑f
theorem
SemilinearIsometryClass.ediam_image
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
{𝓕 : Type u_10}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
[FunLike 𝓕 E E₂]
[SemilinearIsometryClass 𝓕 σ₁₂ E E₂]
(f : 𝓕)
(s : Set E)
:
EMetric.diam (⇑f '' s) = EMetric.diam s
theorem
SemilinearIsometryClass.ediam_range
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
{𝓕 : Type u_10}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
[FunLike 𝓕 E E₂]
[SemilinearIsometryClass 𝓕 σ₁₂ E E₂]
(f : 𝓕)
:
EMetric.diam (Set.range ⇑f) = EMetric.diam Set.univ
theorem
SemilinearIsometryClass.diam_image
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
{𝓕 : Type u_10}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
[FunLike 𝓕 E E₂]
[SemilinearIsometryClass 𝓕 σ₁₂ E E₂]
(f : 𝓕)
(s : Set E)
:
Metric.diam (⇑f '' s) = Metric.diam s
theorem
SemilinearIsometryClass.diam_range
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
{𝓕 : Type u_10}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
[FunLike 𝓕 E E₂]
[SemilinearIsometryClass 𝓕 σ₁₂ E E₂]
(f : 𝓕)
:
Metric.diam (Set.range ⇑f) = Metric.diam Set.univ
@[instance 100]
instance
SemilinearIsometryClass.toContinuousSemilinearMapClass
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
{𝓕 : Type u_10}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
[FunLike 𝓕 E E₂]
[SemilinearIsometryClass 𝓕 σ₁₂ E E₂]
:
ContinuousSemilinearMapClass 𝓕 σ₁₂ E E₂
Equations
- ⋯ = ⋯
theorem
LinearIsometry.toLinearMap_injective
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
:
Function.Injective LinearIsometry.toLinearMap
@[simp]
instance
LinearIsometry.instFunLike
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
:
instance
LinearIsometry.instSemilinearIsometryClass
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
:
SemilinearIsometryClass (E →ₛₗᵢ[σ₁₂] E₂) σ₁₂ E E₂
Equations
- ⋯ = ⋯
@[simp]
theorem
LinearIsometry.coe_mk
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(f : E →ₛₗ[σ₁₂] E₂)
(hf : ∀ (x : E), ‖f x‖ = ‖x‖)
:
⇑{ toLinearMap := f, norm_map' := hf } = ⇑f
theorem
LinearIsometry.coe_injective
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
:
Function.Injective fun (f : E →ₛₗᵢ[σ₁₂] E₂) => ⇑f
def
LinearIsometry.Simps.apply
{R : Type u_1}
{R₂ : Type u_2}
[Semiring R]
[Semiring R₂]
(σ₁₂ : R →+* R₂)
(E : Type u_11)
(E₂ : Type u_12)
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(h : E →ₛₗᵢ[σ₁₂] E₂)
:
E → E₂
See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.
Equations
- LinearIsometry.Simps.apply σ₁₂ E E₂ h = ⇑h
theorem
LinearIsometry.map_smul
{R : Type u_1}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R E₂]
(f : E →ₗᵢ[R] E₂)
(c : R)
(x : E)
:
theorem
LinearIsometry.isEmbedding
{R : Type u_1}
{R₂ : Type u_2}
{E₂ : Type u_6}
{F : Type u_9}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E₂]
[Module R₂ E₂]
[NormedAddCommGroup F]
[Module R F]
(f : F →ₛₗᵢ[σ₁₂] E₂)
:
@[deprecated LinearIsometry.isEmbedding]
theorem
LinearIsometry.embedding
{R : Type u_1}
{R₂ : Type u_2}
{E₂ : Type u_6}
{F : Type u_9}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E₂]
[Module R₂ E₂]
[NormedAddCommGroup F]
[Module R F]
(f : F →ₛₗᵢ[σ₁₂] E₂)
:
Alias of LinearIsometry.isEmbedding.
theorem
LinearIsometry.isComplete_image_iff
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
{𝓕 : Type u_10}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
[FunLike 𝓕 E E₂]
[SemilinearIsometryClass 𝓕 σ₁₂ E E₂]
(f : 𝓕)
{s : Set E}
:
IsComplete (⇑f '' s) ↔ IsComplete s
@[simp]
theorem
LinearIsometry.isComplete_image_iff'
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂)
{s : Set E}
:
IsComplete (⇑f '' s) ↔ IsComplete s
theorem
LinearIsometry.isComplete_map_iff
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂)
[RingHomSurjective σ₁₂]
{p : Submodule R E}
:
IsComplete ↑(Submodule.map f.toLinearMap p) ↔ IsComplete ↑p
theorem
LinearIsometry.isComplete_map_iff'
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
{𝓕 : Type u_10}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
[FunLike 𝓕 E E₂]
[SemilinearIsometryClass 𝓕 σ₁₂ E E₂]
(f : 𝓕)
[RingHomSurjective σ₁₂]
{p : Submodule R E}
:
IsComplete ↑(Submodule.map f p) ↔ IsComplete ↑p
instance
LinearIsometry.completeSpace_map
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
{𝓕 : Type u_10}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
[FunLike 𝓕 E E₂]
[SemilinearIsometryClass 𝓕 σ₁₂ E E₂]
(f : 𝓕)
[RingHomSurjective σ₁₂]
(p : Submodule R E)
[CompleteSpace ↥p]
:
CompleteSpace ↥(Submodule.map f p)
Equations
- ⋯ = ⋯
instance
LinearIsometry.completeSpace_map'
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂)
[RingHomSurjective σ₁₂]
(p : Submodule R E)
[CompleteSpace ↥p]
:
CompleteSpace ↥(Submodule.map f.toLinearMap p)
Equations
- ⋯ = ⋯
theorem
LinearIsometry.injective
{R : Type u_1}
{R₂ : Type u_2}
{E₂ : Type u_6}
{F : Type u_9}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E₂]
[Module R₂ E₂]
[NormedAddCommGroup F]
[Module R F]
(f₁ : F →ₛₗᵢ[σ₁₂] E₂)
:
theorem
LinearIsometry.lipschitz
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂)
:
LipschitzWith 1 ⇑f
theorem
LinearIsometry.antilipschitz
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂)
:
AntilipschitzWith 1 ⇑f
theorem
LinearIsometry.continuous
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂)
:
Continuous ⇑f
@[simp]
theorem
LinearIsometry.preimage_ball
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂)
(x : E)
(r : ℝ)
:
⇑f ⁻¹' Metric.ball (f x) r = Metric.ball x r
@[simp]
theorem
LinearIsometry.preimage_sphere
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂)
(x : E)
(r : ℝ)
:
⇑f ⁻¹' Metric.sphere (f x) r = Metric.sphere x r
@[simp]
theorem
LinearIsometry.preimage_closedBall
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂)
(x : E)
(r : ℝ)
:
⇑f ⁻¹' Metric.closedBall (f x) r = Metric.closedBall x r
theorem
LinearIsometry.ediam_image
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂)
(s : Set E)
:
EMetric.diam (⇑f '' s) = EMetric.diam s
theorem
LinearIsometry.ediam_range
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂)
:
EMetric.diam (Set.range ⇑f) = EMetric.diam Set.univ
theorem
LinearIsometry.diam_image
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂)
(s : Set E)
:
Metric.diam (⇑f '' s) = Metric.diam s
theorem
LinearIsometry.diam_range
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂)
:
Metric.diam (Set.range ⇑f) = Metric.diam Set.univ
def
LinearIsometry.toContinuousLinearMap
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂)
:
Interpret a linear isometry as a continuous linear map.
Equations
- f.toContinuousLinearMap = { toLinearMap := f.toLinearMap, cont := ⋯ }
theorem
LinearIsometry.toContinuousLinearMap_injective
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
:
Function.Injective LinearIsometry.toContinuousLinearMap
@[simp]
theorem
LinearIsometry.toContinuousLinearMap_inj
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
{f g : E →ₛₗᵢ[σ₁₂] E₂}
:
@[simp]
theorem
LinearIsometry.coe_toContinuousLinearMap
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂)
:
⇑f.toContinuousLinearMap = ⇑f
@[simp]
theorem
LinearIsometry.comp_continuous_iff
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂)
{α : Type u_11}
[TopologicalSpace α]
{g : α → E}
:
Continuous (⇑f ∘ g) ↔ Continuous g
def
LinearIsometry.id
{R : Type u_1}
{E : Type u_5}
[Semiring R]
[SeminormedAddCommGroup E]
[Module R E]
:
The identity linear isometry.
Equations
- LinearIsometry.id = { toLinearMap := LinearMap.id, norm_map' := ⋯ }
@[simp]
theorem
LinearIsometry.coe_id
{R : Type u_1}
{E : Type u_5}
[Semiring R]
[SeminormedAddCommGroup E]
[Module R E]
:
⇑LinearIsometry.id = id
@[simp]
theorem
LinearIsometry.id_apply
{R : Type u_1}
{E : Type u_5}
[Semiring R]
[SeminormedAddCommGroup E]
[Module R E]
(x : E)
:
LinearIsometry.id x = x
@[simp]
theorem
LinearIsometry.id_toLinearMap
{R : Type u_1}
{E : Type u_5}
[Semiring R]
[SeminormedAddCommGroup E]
[Module R E]
:
LinearIsometry.id.toLinearMap = LinearMap.id
@[simp]
theorem
LinearIsometry.id_toContinuousLinearMap
{R : Type u_1}
{E : Type u_5}
[Semiring R]
[SeminormedAddCommGroup E]
[Module R E]
:
LinearIsometry.id.toContinuousLinearMap = ContinuousLinearMap.id R E
def
LinearIsometry.comp
{R : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
{E : Type u_5}
{E₂ : Type u_6}
{E₃ : Type u_7}
[Semiring R]
[Semiring R₂]
[Semiring R₃]
{σ₁₂ : R →+* R₂}
{σ₁₃ : R →+* R₃}
{σ₂₃ : R₂ →+* R₃}
[RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[SeminormedAddCommGroup E₃]
[Module R E]
[Module R₂ E₂]
[Module R₃ E₃]
(g : E₂ →ₛₗᵢ[σ₂₃] E₃)
(f : E →ₛₗᵢ[σ₁₂] E₂)
:
Composition of linear isometries.
Equations
- g.comp f = { toLinearMap := g.comp f.toLinearMap, norm_map' := ⋯ }
@[simp]
theorem
LinearIsometry.coe_comp
{R : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
{E : Type u_5}
{E₂ : Type u_6}
{E₃ : Type u_7}
[Semiring R]
[Semiring R₂]
[Semiring R₃]
{σ₁₂ : R →+* R₂}
{σ₁₃ : R →+* R₃}
{σ₂₃ : R₂ →+* R₃}
[RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[SeminormedAddCommGroup E₃]
[Module R E]
[Module R₂ E₂]
[Module R₃ E₃]
(g : E₂ →ₛₗᵢ[σ₂₃] E₃)
(f : E →ₛₗᵢ[σ₁₂] E₂)
:
theorem
LinearIsometry.comp_assoc
{R : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
{R₄ : Type u_4}
{E : Type u_5}
{E₂ : Type u_6}
{E₃ : Type u_7}
{E₄ : Type u_8}
[Semiring R]
[Semiring R₂]
[Semiring R₃]
[Semiring R₄]
{σ₁₂ : R →+* R₂}
{σ₁₃ : R →+* R₃}
{σ₁₄ : R →+* R₄}
{σ₂₃ : R₂ →+* R₃}
{σ₂₄ : R₂ →+* R₄}
{σ₃₄ : R₃ →+* R₄}
[RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
[RingHomCompTriple σ₁₂ σ₂₄ σ₁₄]
[RingHomCompTriple σ₂₃ σ₃₄ σ₂₄]
[RingHomCompTriple σ₁₃ σ₃₄ σ₁₄]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[SeminormedAddCommGroup E₃]
[SeminormedAddCommGroup E₄]
[Module R E]
[Module R₂ E₂]
[Module R₃ E₃]
[Module R₄ E₄]
(f : E₃ →ₛₗᵢ[σ₃₄] E₄)
(g : E₂ →ₛₗᵢ[σ₂₃] E₃)
(h : E →ₛₗᵢ[σ₁₂] E₂)
:
(f.comp g).comp h = f.comp (g.comp h)
@[simp]
theorem
LinearIsometry.coe_one
{R : Type u_1}
{E : Type u_5}
[Semiring R]
[SeminormedAddCommGroup E]
[Module R E]
:
⇑1 = id
theorem
LinearIsometry.one_def
{R : Type u_1}
{E : Type u_5}
[Semiring R]
[SeminormedAddCommGroup E]
[Module R E]
:
1 = LinearIsometry.id
def
LinearMap.toLinearIsometry
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(f : E →ₛₗ[σ₁₂] E₂)
(hf : Isometry ⇑f)
:
Construct a LinearIsometry from a LinearMap satisfying Isometry.
Equations
- f.toLinearIsometry hf = { toLinearMap := f, norm_map' := ⋯ }
def
Submodule.subtypeₗᵢ
{E : Type u_5}
[SeminormedAddCommGroup E]
{R' : Type u_11}
[Ring R']
[Module R' E]
(p : Submodule R' E)
:
Submodule.subtype as a LinearIsometry.
Equations
- p.subtypeₗᵢ = { toLinearMap := p.subtype, norm_map' := ⋯ }
@[simp]
theorem
Submodule.coe_subtypeₗᵢ
{E : Type u_5}
[SeminormedAddCommGroup E]
{R' : Type u_11}
[Ring R']
[Module R' E]
(p : Submodule R' E)
:
⇑p.subtypeₗᵢ = ⇑p.subtype
@[simp]
theorem
Submodule.subtypeₗᵢ_toLinearMap
{E : Type u_5}
[SeminormedAddCommGroup E]
{R' : Type u_11}
[Ring R']
[Module R' E]
(p : Submodule R' E)
:
p.subtypeₗᵢ.toLinearMap = p.subtype
@[simp]
theorem
Submodule.subtypeₗᵢ_toContinuousLinearMap
{E : Type u_5}
[SeminormedAddCommGroup E]
{R' : Type u_11}
[Ring R']
[Module R' E]
(p : Submodule R' E)
:
p.subtypeₗᵢ.toContinuousLinearMap = p.subtypeL
structure
LinearIsometryEquiv
{R : Type u_1}
{R₂ : Type u_2}
[Semiring R]
[Semiring R₂]
(σ₁₂ : R →+* R₂)
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
(E : Type u_11)
(E₂ : Type u_12)
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
extends E ≃ₛₗ[σ₁₂] E₂ :
Type (max u_11 u_12)
A semilinear isometric equivalence between two normed vector spaces.
- toFun : E → E₂
- invFun : E₂ → E
- left_inv : Function.LeftInverse self.invFun (↑self.toLinearEquiv).toFun
- right_inv : Function.RightInverse self.invFun (↑self.toLinearEquiv).toFun
A semilinear isometric equivalence between two normed vector spaces.
Equations
- One or more equations did not get rendered due to their size.
A linear isometric equivalence between two normed vector spaces.
Equations
- One or more equations did not get rendered due to their size.
An antilinear isometric equivalence between two normed vector spaces.
Equations
- One or more equations did not get rendered due to their size.
class
SemilinearIsometryEquivClass
(𝓕 : Type u_11)
{R : outParam (Type u_12)}
{R₂ : outParam (Type u_13)}
[Semiring R]
[Semiring R₂]
(σ₁₂ : outParam (R →+* R₂))
{σ₂₁ : outParam (R₂ →+* R)}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
(E : outParam (Type u_14))
(E₂ : outParam (Type u_15))
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
[EquivLike 𝓕 E E₂]
extends SemilinearEquivClass 𝓕 σ₁₂ E E₂ :
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.
- map_smulₛₗ : ∀ (f : 𝓕) (r : R) (x : E), f (r • x) = σ₁₂ r • f x
@[reducible, inline]
abbrev
LinearIsometryEquivClass
(𝓕 : Type u_11)
(R : outParam (Type u_12))
(E : outParam (Type u_13))
(E₂ : outParam (Type u_14))
[Semiring R]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R E₂]
[EquivLike 𝓕 E E₂]
:
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₂.
Equations
- LinearIsometryEquivClass 𝓕 R E E₂ = SemilinearIsometryEquivClass 𝓕 (RingHom.id R) E E₂
@[instance 100]
instance
SemilinearIsometryEquivClass.toSemilinearIsometryClass
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
(𝓕 : Type u_10)
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
[EquivLike 𝓕 E E₂]
[s : SemilinearIsometryEquivClass 𝓕 σ₁₂ E E₂]
:
SemilinearIsometryClass 𝓕 σ₁₂ E E₂
Equations
- ⋯ = ⋯
theorem
LinearIsometryEquiv.toLinearEquiv_injective
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
:
Function.Injective LinearIsometryEquiv.toLinearEquiv
@[simp]
theorem
LinearIsometryEquiv.toLinearEquiv_inj
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
{f g : E ≃ₛₗᵢ[σ₁₂] E₂}
:
instance
LinearIsometryEquiv.instEquivLike
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
:
Equations
- One or more equations did not get rendered due to their size.
instance
LinearIsometryEquiv.instSemilinearIsometryEquivClass
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
:
SemilinearIsometryEquivClass (E ≃ₛₗᵢ[σ₁₂] E₂) σ₁₂ E E₂
Equations
- ⋯ = ⋯
instance
LinearIsometryEquiv.instCoeFun
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
:
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.)
Equations
- LinearIsometryEquiv.instCoeFun = { coe := DFunLike.coe }
theorem
LinearIsometryEquiv.coe_injective
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
:
Function.Injective DFunLike.coe
@[simp]
theorem
LinearIsometryEquiv.coe_mk
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗ[σ₁₂] E₂)
(he : ∀ (x : E), ‖e x‖ = ‖x‖)
:
⇑{ toLinearEquiv := e, norm_map' := he } = ⇑e
@[simp]
theorem
LinearIsometryEquiv.coe_toLinearEquiv
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
:
⇑e.toLinearEquiv = ⇑e
theorem
LinearIsometryEquiv.ext
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
{e e' : E ≃ₛₗᵢ[σ₁₂] E₂}
(h : ∀ (x : E), e x = e' x)
:
e = e'
theorem
LinearIsometryEquiv.congr_arg
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
{f : E ≃ₛₗᵢ[σ₁₂] E₂}
{x x' : E}
:
theorem
LinearIsometryEquiv.congr_fun
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
{f g : E ≃ₛₗᵢ[σ₁₂] E₂}
(h : f = g)
(x : E)
:
f x = g x
def
LinearIsometryEquiv.ofBounds
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗ[σ₁₂] E₂)
(h₁ : ∀ (x : E), ‖e x‖ ≤ ‖x‖)
(h₂ : ∀ (y : E₂), ‖e.symm y‖ ≤ ‖y‖)
:
Construct a LinearIsometryEquiv from a LinearEquiv and two inequalities:
∀ x, ‖e x‖ ≤ ‖x‖ and ∀ y, ‖e.symm y‖ ≤ ‖y‖.
Equations
- LinearIsometryEquiv.ofBounds e h₁ h₂ = { toLinearEquiv := e, norm_map' := ⋯ }
@[simp]
theorem
LinearIsometryEquiv.norm_map
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(x : E)
:
def
LinearIsometryEquiv.toLinearIsometry
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
:
Reinterpret a LinearIsometryEquiv as a LinearIsometry.
Equations
- e.toLinearIsometry = { toLinearMap := ↑e.toLinearEquiv, norm_map' := ⋯ }
theorem
LinearIsometryEquiv.toLinearIsometry_injective
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
:
Function.Injective LinearIsometryEquiv.toLinearIsometry
@[simp]
theorem
LinearIsometryEquiv.toLinearIsometry_inj
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
{f g : E ≃ₛₗᵢ[σ₁₂] E₂}
:
@[simp]
theorem
LinearIsometryEquiv.coe_toLinearIsometry
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
:
⇑e.toLinearIsometry = ⇑e
theorem
LinearIsometryEquiv.isometry
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
:
Isometry ⇑e
def
LinearIsometryEquiv.toIsometryEquiv
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
:
E ≃ᵢ E₂
Reinterpret a LinearIsometryEquiv as an IsometryEquiv.
Equations
- e.toIsometryEquiv = { toEquiv := e.toEquiv, isometry_toFun := ⋯ }
theorem
LinearIsometryEquiv.toIsometryEquiv_injective
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
:
Function.Injective LinearIsometryEquiv.toIsometryEquiv
@[simp]
theorem
LinearIsometryEquiv.toIsometryEquiv_inj
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
{f g : E ≃ₛₗᵢ[σ₁₂] E₂}
:
@[simp]
theorem
LinearIsometryEquiv.coe_toIsometryEquiv
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
:
⇑e.toIsometryEquiv = ⇑e
theorem
LinearIsometryEquiv.range_eq_univ
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
:
def
LinearIsometryEquiv.toHomeomorph
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
:
E ≃ₜ E₂
Reinterpret a LinearIsometryEquiv as a Homeomorph.
Equations
- e.toHomeomorph = e.toIsometryEquiv.toHomeomorph
theorem
LinearIsometryEquiv.toHomeomorph_injective
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
:
Function.Injective LinearIsometryEquiv.toHomeomorph
@[simp]
theorem
LinearIsometryEquiv.toHomeomorph_inj
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
{f g : E ≃ₛₗᵢ[σ₁₂] E₂}
:
@[simp]
theorem
LinearIsometryEquiv.coe_toHomeomorph
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
:
⇑e.toHomeomorph = ⇑e
theorem
LinearIsometryEquiv.continuous
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
:
Continuous ⇑e
theorem
LinearIsometryEquiv.continuousAt
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
{x : E}
:
ContinuousAt (⇑e) x
theorem
LinearIsometryEquiv.continuousOn
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
{s : Set E}
:
ContinuousOn (⇑e) s
theorem
LinearIsometryEquiv.continuousWithinAt
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
{s : Set E}
{x : E}
:
ContinuousWithinAt (⇑e) s x
def
LinearIsometryEquiv.toContinuousLinearEquiv
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
:
Interpret a LinearIsometryEquiv as a ContinuousLinearEquiv.
Equations
- One or more equations did not get rendered due to their size.
theorem
LinearIsometryEquiv.toContinuousLinearEquiv_injective
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
:
Function.Injective LinearIsometryEquiv.toContinuousLinearEquiv
@[simp]
theorem
LinearIsometryEquiv.toContinuousLinearEquiv_inj
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
{f g : E ≃ₛₗᵢ[σ₁₂] E₂}
:
@[simp]
theorem
LinearIsometryEquiv.coe_toContinuousLinearEquiv
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
:
⇑e.toContinuousLinearEquiv = ⇑e
def
LinearIsometryEquiv.refl
(R : Type u_1)
(E : Type u_5)
[Semiring R]
[SeminormedAddCommGroup E]
[Module R E]
:
Identity map as a LinearIsometryEquiv.
Equations
- LinearIsometryEquiv.refl R E = { toLinearEquiv := LinearEquiv.refl R E, norm_map' := ⋯ }
def
LinearIsometryEquiv.ulift
(R : Type u_1)
(E : Type u_5)
[Semiring R]
[SeminormedAddCommGroup E]
[Module R E]
:
ULift.{u_11, u_5} E ≃ₗᵢ[R] E
Linear isometry equiv between a space and its lift to another universe.
Equations
- LinearIsometryEquiv.ulift R E = { toLinearEquiv := ContinuousLinearEquiv.ulift.toLinearEquiv, norm_map' := ⋯ }
instance
LinearIsometryEquiv.instInhabited
{R : Type u_1}
{E : Type u_5}
[Semiring R]
[SeminormedAddCommGroup E]
[Module R E]
:
Equations
- LinearIsometryEquiv.instInhabited = { default := LinearIsometryEquiv.refl R E }
@[simp]
theorem
LinearIsometryEquiv.coe_refl
{R : Type u_1}
{E : Type u_5}
[Semiring R]
[SeminormedAddCommGroup E]
[Module R E]
:
⇑(LinearIsometryEquiv.refl R E) = id
def
LinearIsometryEquiv.symm
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
:
The inverse LinearIsometryEquiv.
Equations
- e.symm = { toLinearEquiv := e.symm, norm_map' := ⋯ }
@[simp]
theorem
LinearIsometryEquiv.apply_symm_apply
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(x : E₂)
:
e (e.symm x) = x
@[simp]
theorem
LinearIsometryEquiv.symm_apply_apply
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(x : E)
:
e.symm (e x) = x
theorem
LinearIsometryEquiv.map_eq_zero_iff
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
{x : E}
:
@[simp]
theorem
LinearIsometryEquiv.symm_symm
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
:
e.symm.symm = e
@[simp]
theorem
LinearIsometryEquiv.toLinearEquiv_symm
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
:
e.symm = e.symm.toLinearEquiv
@[simp]
theorem
LinearIsometryEquiv.toIsometryEquiv_symm
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
:
e.toIsometryEquiv.symm = e.symm.toIsometryEquiv
@[simp]
theorem
LinearIsometryEquiv.toHomeomorph_symm
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
:
e.toHomeomorph.symm = e.symm.toHomeomorph
def
LinearIsometryEquiv.Simps.apply
{R : Type u_1}
{R₂ : Type u_2}
[Semiring R]
[Semiring R₂]
(σ₁₂ : R →+* R₂)
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
(E : Type u_11)
(E₂ : Type u_12)
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(h : E ≃ₛₗᵢ[σ₁₂] E₂)
:
E → E₂
See Note [custom simps projection]. We need to specify this projection explicitly in this case, because it is a composition of multiple projections.
Equations
- LinearIsometryEquiv.Simps.apply σ₁₂ E E₂ h = ⇑h
def
LinearIsometryEquiv.Simps.symm_apply
{R : Type u_1}
{R₂ : Type u_2}
[Semiring R]
[Semiring R₂]
(σ₁₂ : R →+* R₂)
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
(E : Type u_11)
(E₂ : Type u_12)
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(h : E ≃ₛₗᵢ[σ₁₂] E₂)
:
E₂ → E
See Note [custom simps projection]
Equations
- LinearIsometryEquiv.Simps.symm_apply σ₁₂ E E₂ h = ⇑h.symm
def
LinearIsometryEquiv.trans
{R : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
{E : Type u_5}
{E₂ : Type u_6}
{E₃ : Type u_7}
[Semiring R]
[Semiring R₂]
[Semiring R₃]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
{σ₁₃ : R →+* R₃}
{σ₃₁ : R₃ →+* R}
{σ₂₃ : R₂ →+* R₃}
{σ₃₂ : R₃ →+* R₂}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[RingHomInvPair σ₁₃ σ₃₁]
[RingHomInvPair σ₃₁ σ₁₃]
[RingHomInvPair σ₂₃ σ₃₂]
[RingHomInvPair σ₃₂ σ₂₃]
[RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
[RingHomCompTriple σ₃₂ σ₂₁ σ₃₁]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[SeminormedAddCommGroup E₃]
[Module R E]
[Module R₂ E₂]
[Module R₃ E₃]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(e' : E₂ ≃ₛₗᵢ[σ₂₃] E₃)
:
Composition of LinearIsometryEquivs as a LinearIsometryEquiv.
Equations
- e.trans e' = { toLinearEquiv := e.trans e'.toLinearEquiv, norm_map' := ⋯ }
@[simp]
theorem
LinearIsometryEquiv.coe_trans
{R : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
{E : Type u_5}
{E₂ : Type u_6}
{E₃ : Type u_7}
[Semiring R]
[Semiring R₂]
[Semiring R₃]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
{σ₁₃ : R →+* R₃}
{σ₃₁ : R₃ →+* R}
{σ₂₃ : R₂ →+* R₃}
{σ₃₂ : R₃ →+* R₂}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[RingHomInvPair σ₁₃ σ₃₁]
[RingHomInvPair σ₃₁ σ₁₃]
[RingHomInvPair σ₂₃ σ₃₂]
[RingHomInvPair σ₃₂ σ₂₃]
[RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
[RingHomCompTriple σ₃₂ σ₂₁ σ₃₁]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[SeminormedAddCommGroup E₃]
[Module R E]
[Module R₂ E₂]
[Module R₃ E₃]
(e₁ : E ≃ₛₗᵢ[σ₁₂] E₂)
(e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃)
:
@[simp]
theorem
LinearIsometryEquiv.trans_apply
{R : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
{E : Type u_5}
{E₂ : Type u_6}
{E₃ : Type u_7}
[Semiring R]
[Semiring R₂]
[Semiring R₃]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
{σ₁₃ : R →+* R₃}
{σ₃₁ : R₃ →+* R}
{σ₂₃ : R₂ →+* R₃}
{σ₃₂ : R₃ →+* R₂}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[RingHomInvPair σ₁₃ σ₃₁]
[RingHomInvPair σ₃₁ σ₁₃]
[RingHomInvPair σ₂₃ σ₃₂]
[RingHomInvPair σ₃₂ σ₂₃]
[RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
[RingHomCompTriple σ₃₂ σ₂₁ σ₃₁]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[SeminormedAddCommGroup E₃]
[Module R E]
[Module R₂ E₂]
[Module R₃ E₃]
(e₁ : E ≃ₛₗᵢ[σ₁₂] E₂)
(e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃)
(c : E)
:
(e₁.trans e₂) c = e₂ (e₁ c)
@[simp]
theorem
LinearIsometryEquiv.toLinearEquiv_trans
{R : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
{E : Type u_5}
{E₂ : Type u_6}
{E₃ : Type u_7}
[Semiring R]
[Semiring R₂]
[Semiring R₃]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
{σ₁₃ : R →+* R₃}
{σ₃₁ : R₃ →+* R}
{σ₂₃ : R₂ →+* R₃}
{σ₃₂ : R₃ →+* R₂}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[RingHomInvPair σ₁₃ σ₃₁]
[RingHomInvPair σ₃₁ σ₁₃]
[RingHomInvPair σ₂₃ σ₃₂]
[RingHomInvPair σ₃₂ σ₂₃]
[RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
[RingHomCompTriple σ₃₂ σ₂₁ σ₃₁]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[SeminormedAddCommGroup E₃]
[Module R E]
[Module R₂ E₂]
[Module R₃ E₃]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(e' : E₂ ≃ₛₗᵢ[σ₂₃] E₃)
:
(e.trans e').toLinearEquiv = e.trans e'.toLinearEquiv
@[simp]
theorem
LinearIsometryEquiv.trans_refl
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
:
e.trans (LinearIsometryEquiv.refl R₂ E₂) = e
@[simp]
theorem
LinearIsometryEquiv.refl_trans
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
:
(LinearIsometryEquiv.refl R E).trans e = e
@[simp]
theorem
LinearIsometryEquiv.self_trans_symm
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
:
e.trans e.symm = LinearIsometryEquiv.refl R E
@[simp]
theorem
LinearIsometryEquiv.symm_trans_self
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
:
e.symm.trans e = LinearIsometryEquiv.refl R₂ E₂
@[simp]
theorem
LinearIsometryEquiv.symm_comp_self
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
:
@[simp]
theorem
LinearIsometryEquiv.self_comp_symm
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
:
@[simp]
theorem
LinearIsometryEquiv.symm_trans
{R : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
{E : Type u_5}
{E₂ : Type u_6}
{E₃ : Type u_7}
[Semiring R]
[Semiring R₂]
[Semiring R₃]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
{σ₁₃ : R →+* R₃}
{σ₃₁ : R₃ →+* R}
{σ₂₃ : R₂ →+* R₃}
{σ₃₂ : R₃ →+* R₂}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[RingHomInvPair σ₁₃ σ₃₁]
[RingHomInvPair σ₃₁ σ₁₃]
[RingHomInvPair σ₂₃ σ₃₂]
[RingHomInvPair σ₃₂ σ₂₃]
[RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
[RingHomCompTriple σ₃₂ σ₂₁ σ₃₁]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[SeminormedAddCommGroup E₃]
[Module R E]
[Module R₂ E₂]
[Module R₃ E₃]
(e₁ : E ≃ₛₗᵢ[σ₁₂] E₂)
(e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃)
:
(e₁.trans e₂).symm = e₂.symm.trans e₁.symm
theorem
LinearIsometryEquiv.coe_symm_trans
{R : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
{E : Type u_5}
{E₂ : Type u_6}
{E₃ : Type u_7}
[Semiring R]
[Semiring R₂]
[Semiring R₃]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
{σ₁₃ : R →+* R₃}
{σ₃₁ : R₃ →+* R}
{σ₂₃ : R₂ →+* R₃}
{σ₃₂ : R₃ →+* R₂}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[RingHomInvPair σ₁₃ σ₃₁]
[RingHomInvPair σ₃₁ σ₁₃]
[RingHomInvPair σ₂₃ σ₃₂]
[RingHomInvPair σ₃₂ σ₂₃]
[RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
[RingHomCompTriple σ₃₂ σ₂₁ σ₃₁]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[SeminormedAddCommGroup E₃]
[Module R E]
[Module R₂ E₂]
[Module R₃ E₃]
(e₁ : E ≃ₛₗᵢ[σ₁₂] E₂)
(e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃)
:
theorem
LinearIsometryEquiv.trans_assoc
{R : Type u_1}
{R₂ : Type u_2}
{R₃ : Type u_3}
{R₄ : Type u_4}
{E : Type u_5}
{E₂ : Type u_6}
{E₃ : Type u_7}
{E₄ : Type u_8}
[Semiring R]
[Semiring R₂]
[Semiring R₃]
[Semiring R₄]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
{σ₁₃ : R →+* R₃}
{σ₃₁ : R₃ →+* R}
{σ₁₄ : R →+* R₄}
{σ₄₁ : R₄ →+* R}
{σ₂₃ : R₂ →+* R₃}
{σ₃₂ : R₃ →+* R₂}
{σ₂₄ : R₂ →+* R₄}
{σ₄₂ : R₄ →+* R₂}
{σ₃₄ : R₃ →+* R₄}
{σ₄₃ : R₄ →+* R₃}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[RingHomInvPair σ₁₃ σ₃₁]
[RingHomInvPair σ₃₁ σ₁₃]
[RingHomInvPair σ₂₃ σ₃₂]
[RingHomInvPair σ₃₂ σ₂₃]
[RingHomInvPair σ₁₄ σ₄₁]
[RingHomInvPair σ₄₁ σ₁₄]
[RingHomInvPair σ₂₄ σ₄₂]
[RingHomInvPair σ₄₂ σ₂₄]
[RingHomInvPair σ₃₄ σ₄₃]
[RingHomInvPair σ₄₃ σ₃₄]
[RingHomCompTriple σ₁₂ σ₂₃ σ₁₃]
[RingHomCompTriple σ₁₂ σ₂₄ σ₁₄]
[RingHomCompTriple σ₂₃ σ₃₄ σ₂₄]
[RingHomCompTriple σ₁₃ σ₃₄ σ₁₄]
[RingHomCompTriple σ₃₂ σ₂₁ σ₃₁]
[RingHomCompTriple σ₄₂ σ₂₁ σ₄₁]
[RingHomCompTriple σ₄₃ σ₃₂ σ₄₂]
[RingHomCompTriple σ₄₃ σ₃₁ σ₄₁]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[SeminormedAddCommGroup E₃]
[SeminormedAddCommGroup E₄]
[Module R E]
[Module R₂ E₂]
[Module R₃ E₃]
[Module R₄ E₄]
(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₄
@[simp]
theorem
LinearIsometryEquiv.coe_one
{R : Type u_1}
{E : Type u_5}
[Semiring R]
[SeminormedAddCommGroup E]
[Module R E]
:
⇑1 = id
theorem
LinearIsometryEquiv.one_def
{R : Type u_1}
{E : Type u_5}
[Semiring R]
[SeminormedAddCommGroup E]
[Module R E]
:
1 = LinearIsometryEquiv.refl R E
Lemmas about mixing the group structure with definitions. Because we have multiple ways to
express LinearIsometryEquiv.refl, LinearIsometryEquiv.symm, and
LinearIsometryEquiv.trans, we want simp lemmas for every combination.
The assumption made here is that if you're using the group structure, you want to preserve it
after simp.
This copies the approach used by the lemmas near Equiv.Perm.trans_one.
@[simp]
theorem
LinearIsometryEquiv.trans_one
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
:
e.trans 1 = e
@[simp]
theorem
LinearIsometryEquiv.one_trans
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
:
LinearIsometryEquiv.trans 1 e = e
@[simp]
theorem
LinearIsometryEquiv.refl_mul
{R : Type u_1}
{E : Type u_5}
[Semiring R]
[SeminormedAddCommGroup E]
[Module R E]
(e : E ≃ₗᵢ[R] E)
:
LinearIsometryEquiv.refl R E * e = e
@[simp]
theorem
LinearIsometryEquiv.mul_refl
{R : Type u_1}
{E : Type u_5}
[Semiring R]
[SeminormedAddCommGroup E]
[Module R E]
(e : E ≃ₗᵢ[R] E)
:
e * LinearIsometryEquiv.refl R E = e
instance
LinearIsometryEquiv.instCoeTCContinuousLinearEquiv
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
:
Reinterpret a LinearIsometryEquiv as a ContinuousLinearEquiv.
instance
LinearIsometryEquiv.instCoeTCContinuousLinearMap
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
:
@[simp]
theorem
LinearIsometryEquiv.coe_coe
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
:
⇑{ toLinearEquiv := e.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ } = ⇑e
@[simp]
theorem
LinearIsometryEquiv.coe_coe''
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
:
⇑↑{ toLinearEquiv := e.toLinearEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ } = ⇑e
theorem
LinearIsometryEquiv.map_zero
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
:
e 0 = 0
theorem
LinearIsometryEquiv.map_add
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(x y : E)
:
theorem
LinearIsometryEquiv.map_sub
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(x y : E)
:
theorem
LinearIsometryEquiv.map_smulₛₗ
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(c : R)
(x : E)
:
theorem
LinearIsometryEquiv.map_smul
{R : Type u_1}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R E₂]
{e : E ≃ₗᵢ[R] E₂}
(c : R)
(x : E)
:
@[simp]
theorem
LinearIsometryEquiv.nnnorm_map
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(x : E)
:
@[simp]
theorem
LinearIsometryEquiv.dist_map
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(x y : E)
:
@[simp]
theorem
LinearIsometryEquiv.edist_map
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(x y : E)
:
theorem
LinearIsometryEquiv.bijective
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
:
theorem
LinearIsometryEquiv.injective
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
:
theorem
LinearIsometryEquiv.surjective
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
:
theorem
LinearIsometryEquiv.map_eq_iff
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
{x y : E}
:
theorem
LinearIsometryEquiv.map_ne
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
{x y : E}
(h : x ≠ y)
:
e x ≠ e y
theorem
LinearIsometryEquiv.lipschitz
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
:
LipschitzWith 1 ⇑e
theorem
LinearIsometryEquiv.antilipschitz
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
:
AntilipschitzWith 1 ⇑e
theorem
LinearIsometryEquiv.image_eq_preimage
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(s : Set E)
:
@[simp]
theorem
LinearIsometryEquiv.ediam_image
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(s : Set E)
:
EMetric.diam (⇑e '' s) = EMetric.diam s
@[simp]
theorem
LinearIsometryEquiv.diam_image
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(s : Set E)
:
Metric.diam (⇑e '' s) = Metric.diam s
@[simp]
theorem
LinearIsometryEquiv.preimage_ball
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(x : E₂)
(r : ℝ)
:
⇑e ⁻¹' Metric.ball x r = Metric.ball (e.symm x) r
@[simp]
theorem
LinearIsometryEquiv.preimage_sphere
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(x : E₂)
(r : ℝ)
:
⇑e ⁻¹' Metric.sphere x r = Metric.sphere (e.symm x) r
@[simp]
theorem
LinearIsometryEquiv.preimage_closedBall
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(x : E₂)
(r : ℝ)
:
⇑e ⁻¹' Metric.closedBall x r = Metric.closedBall (e.symm x) r
@[simp]
theorem
LinearIsometryEquiv.image_ball
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(x : E)
(r : ℝ)
:
⇑e '' Metric.ball x r = Metric.ball (e x) r
@[simp]
theorem
LinearIsometryEquiv.image_sphere
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(x : E)
(r : ℝ)
:
⇑e '' Metric.sphere x r = Metric.sphere (e x) r
@[simp]
theorem
LinearIsometryEquiv.image_closedBall
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(x : E)
(r : ℝ)
:
⇑e '' Metric.closedBall x r = Metric.closedBall (e x) r
@[simp]
theorem
LinearIsometryEquiv.comp_continuousOn_iff
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
{α : Type u_11}
[TopologicalSpace α]
{f : α → E}
{s : Set α}
:
ContinuousOn (⇑e ∘ f) s ↔ ContinuousOn f s
@[simp]
theorem
LinearIsometryEquiv.comp_continuous_iff
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
{α : Type u_11}
[TopologicalSpace α]
{f : α → E}
:
Continuous (⇑e ∘ f) ↔ Continuous f
instance
LinearIsometryEquiv.completeSpace_map
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(p : Submodule R E)
[CompleteSpace ↥p]
:
CompleteSpace ↥(Submodule.map (↑e.toLinearEquiv) p)
Equations
- ⋯ = ⋯
noncomputable def
LinearIsometryEquiv.ofSurjective
{R : Type u_1}
{R₂ : Type u_2}
{E₂ : Type u_6}
{F : Type u_9}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E₂]
[Module R₂ E₂]
[NormedAddCommGroup F]
[Module R F]
(f : F →ₛₗᵢ[σ₁₂] E₂)
(hfr : Function.Surjective ⇑f)
:
Construct a linear isometry equiv from a surjective linear isometry.
Equations
- LinearIsometryEquiv.ofSurjective f hfr = { toLinearEquiv := LinearEquiv.ofBijective f.toLinearMap ⋯, norm_map' := ⋯ }
@[simp]
theorem
LinearIsometryEquiv.coe_ofSurjective
{R : Type u_1}
{R₂ : Type u_2}
{E₂ : Type u_6}
{F : Type u_9}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E₂]
[Module R₂ E₂]
[NormedAddCommGroup F]
[Module R F]
(f : F →ₛₗᵢ[σ₁₂] E₂)
(hfr : Function.Surjective ⇑f)
:
⇑(LinearIsometryEquiv.ofSurjective f hfr) = ⇑f
def
LinearIsometryEquiv.ofLinearIsometry
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂)
(g : E₂ →ₛₗ[σ₂₁] E)
(h₁ : f.comp g = LinearMap.id)
(h₂ : g.comp f.toLinearMap = LinearMap.id)
:
If a linear isometry has an inverse, it is a linear isometric equivalence.
Equations
- LinearIsometryEquiv.ofLinearIsometry f g h₁ h₂ = { toLinearEquiv := LinearEquiv.ofLinear f.toLinearMap g h₁ h₂, norm_map' := ⋯ }
@[simp]
theorem
LinearIsometryEquiv.coe_ofLinearIsometry
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂)
(g : E₂ →ₛₗ[σ₂₁] E)
(h₁ : f.comp g = LinearMap.id)
(h₂ : g.comp f.toLinearMap = LinearMap.id)
:
⇑(LinearIsometryEquiv.ofLinearIsometry f g h₁ h₂) = ⇑f
@[simp]
theorem
LinearIsometryEquiv.coe_ofLinearIsometry_symm
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂)
(g : E₂ →ₛₗ[σ₂₁] E)
(h₁ : f.comp g = LinearMap.id)
(h₂ : g.comp f.toLinearMap = LinearMap.id)
:
⇑(LinearIsometryEquiv.ofLinearIsometry f g h₁ h₂).symm = ⇑g
def
LinearIsometryEquiv.neg
(R : Type u_1)
{E : Type u_5}
[Semiring R]
[SeminormedAddCommGroup E]
[Module R E]
:
The negation operation on a normed space E, considered as a linear isometry equivalence.
Equations
- LinearIsometryEquiv.neg R = { toLinearEquiv := LinearEquiv.neg R, norm_map' := ⋯ }
@[simp]
theorem
LinearIsometryEquiv.coe_neg
{R : Type u_1}
{E : Type u_5}
[Semiring R]
[SeminormedAddCommGroup E]
[Module R E]
:
⇑(LinearIsometryEquiv.neg R) = fun (x : E) => -x
@[simp]
theorem
LinearIsometryEquiv.symm_neg
{R : Type u_1}
{E : Type u_5}
[Semiring R]
[SeminormedAddCommGroup E]
[Module R E]
:
(LinearIsometryEquiv.neg R).symm = LinearIsometryEquiv.neg R
def
LinearIsometryEquiv.prodAssoc
(R : Type u_1)
(E : Type u_5)
(E₂ : Type u_6)
(E₃ : Type u_7)
[Semiring R]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[SeminormedAddCommGroup E₃]
[Module R E]
[Module R E₂]
[Module R E₃]
:
The natural equivalence (E × E₂) × E₃ ≃ E × (E₂ × E₃) is a linear isometry.
Equations
- LinearIsometryEquiv.prodAssoc R E E₂ E₃ = { toLinearEquiv := LinearEquiv.prodAssoc R E E₂ E₃, norm_map' := ⋯ }
@[simp]
theorem
LinearIsometryEquiv.coe_prodAssoc
(R : Type u_1)
(E : Type u_5)
(E₂ : Type u_6)
(E₃ : Type u_7)
[Semiring R]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[SeminormedAddCommGroup E₃]
[Module R E]
[Module R E₂]
[Module R E₃]
:
⇑(LinearIsometryEquiv.prodAssoc R E E₂ E₃) = ⇑(Equiv.prodAssoc E E₂ E₃)
@[simp]
theorem
LinearIsometryEquiv.coe_prodAssoc_symm
(R : Type u_1)
(E : Type u_5)
(E₂ : Type u_6)
(E₃ : Type u_7)
[Semiring R]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[SeminormedAddCommGroup E₃]
[Module R E]
[Module R E₂]
[Module R E₃]
:
⇑(LinearIsometryEquiv.prodAssoc R E E₂ E₃).symm = ⇑(Equiv.prodAssoc E E₂ E₃).symm
def
LinearIsometryEquiv.ofTop
(E : Type u_5)
[SeminormedAddCommGroup E]
{R : Type u_12}
[Ring R]
[Module R E]
(p : Submodule R E)
(hp : p = ⊤)
:
If p is a submodule that is equal to ⊤, then LinearIsometryEquiv.ofTop p hp is the
"identity" equivalence between p and E.
Equations
- LinearIsometryEquiv.ofTop E p hp = { toLinearEquiv := LinearEquiv.ofTop p hp, norm_map' := ⋯ }
@[simp]
theorem
LinearIsometryEquiv.ofTop_apply
(E : Type u_5)
[SeminormedAddCommGroup E]
{R : Type u_12}
[Ring R]
[Module R E]
(p : Submodule R E)
(hp : p = ⊤)
(self : ↥p)
:
(LinearIsometryEquiv.ofTop E p hp) self = ↑self
@[simp]
theorem
LinearIsometryEquiv.ofTop_symm_apply_coe
(E : Type u_5)
[SeminormedAddCommGroup E]
{R : Type u_12}
[Ring R]
[Module R E]
(p : Submodule R E)
(hp : p = ⊤)
(x : E)
:
↑((LinearIsometryEquiv.ofTop E p hp).symm x) = x
@[simp]
theorem
LinearIsometryEquiv.ofTop_toLinearEquiv
(E : Type u_5)
[SeminormedAddCommGroup E]
{R : Type u_12}
[Ring R]
[Module R E]
(p : Submodule R E)
(hp : p = ⊤)
:
(LinearIsometryEquiv.ofTop E p hp).toLinearEquiv = LinearEquiv.ofTop p hp
def
LinearIsometryEquiv.ofEq
{E : Type u_5}
[SeminormedAddCommGroup E]
{R' : Type u_12}
[Ring R']
[Module R' E]
(p q : Submodule R' E)
(hpq : p = q)
:
LinearEquiv.ofEq as a LinearIsometryEquiv.
Equations
- LinearIsometryEquiv.ofEq p q hpq = { toLinearEquiv := LinearEquiv.ofEq p q hpq, norm_map' := ⋯ }
@[simp]
theorem
LinearIsometryEquiv.coe_ofEq_apply
{E : Type u_5}
[SeminormedAddCommGroup E]
{R' : Type u_12}
[Ring R']
[Module R' E]
{p q : Submodule R' E}
(h : p = q)
(x : ↥p)
:
↑((LinearIsometryEquiv.ofEq p q h) x) = ↑x
@[simp]
theorem
LinearIsometryEquiv.ofEq_symm
{E : Type u_5}
[SeminormedAddCommGroup E]
{R' : Type u_12}
[Ring R']
[Module R' E]
{p q : Submodule R' E}
(h : p = q)
:
(LinearIsometryEquiv.ofEq p q h).symm = LinearIsometryEquiv.ofEq q p ⋯
@[simp]
theorem
LinearIsometryEquiv.ofEq_rfl
{E : Type u_5}
[SeminormedAddCommGroup E]
{R' : Type u_12}
[Ring R']
[Module R' E]
{p : Submodule R' E}
:
LinearIsometryEquiv.ofEq p p ⋯ = LinearIsometryEquiv.refl R' ↥p
theorem
Basis.ext_linearIsometry
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
{ι : Type u_11}
(b : Basis ι R E)
{f₁ f₂ : E →ₛₗᵢ[σ₁₂] E₂}
(h : ∀ (i : ι), f₁ (b i) = f₂ (b i))
:
f₁ = f₂
Two linear isometries are equal if they are equal on basis vectors.
theorem
Basis.ext_linearIsometryEquiv
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[Semiring R]
[Semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
[SeminormedAddCommGroup E]
[SeminormedAddCommGroup E₂]
[Module R E]
[Module R₂ E₂]
{ι : Type u_11}
(b : Basis ι R E)
{f₁ f₂ : E ≃ₛₗᵢ[σ₁₂] E₂}
(h : ∀ (i : ι), f₁ (b i) = f₂ (b i))
:
f₁ = f₂
Two linear isometric equivalences are equal if they are equal on basis vectors.
noncomputable def
LinearIsometry.equivRange
{E : Type u_5}
{F : Type u_9}
[SeminormedAddCommGroup E]
[NormedAddCommGroup F]
{R : Type u_11}
{S : Type u_12}
[Semiring R]
[Ring S]
[Module S E]
[Module R F]
{σ₁₂ : R →+* S}
{σ₂₁ : S →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
(f : F →ₛₗᵢ[σ₁₂] E)
:
F ≃ₛₗᵢ[σ₁₂] ↥(LinearMap.range f.toLinearMap)
Reinterpret a LinearIsometry as a LinearIsometryEquiv to the range.
Equations
- f.equivRange = { toLinearEquiv := LinearEquiv.ofInjective f.toLinearMap ⋯, norm_map' := ⋯ }
@[simp]
theorem
LinearIsometry.equivRange_apply_coe
{E : Type u_5}
{F : Type u_9}
[SeminormedAddCommGroup E]
[NormedAddCommGroup F]
{R : Type u_11}
{S : Type u_12}
[Semiring R]
[Ring S]
[Module S E]
[Module R F]
{σ₁₂ : R →+* S}
{σ₂₁ : S →+* R}
[RingHomInvPair σ₁₂ σ₂₁]
[RingHomInvPair σ₂₁ σ₁₂]
(f : F →ₛₗᵢ[σ₁₂] E)
(a : F)
:
↑(f.equivRange a) = f a