(Semi-)linear isometries #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we define linear_isometry σ₁₂ E E₂ (notation: E →ₛₗᵢ[σ₁₂] E₂) to be a semilinear
isometric embedding of E into E₂ and linear_isometry_equiv (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 seminormed_add_comm_group and we specialize to normed_add_comm_group when needed.
structure
linear_isometry
{R : Type u_1}
{R₂ : Type u_2}
[semiring R]
[semiring R₂]
(σ₁₂ : R →+* R₂)
(E : Type u_11)
(E₂ : Type u_12)
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂] :
Type (max u_11 u_12)
A σ₁₂-semilinear isometric embedding of a normed R-module into an R₂-module.
Instances for linear_isometry
- linear_isometry.has_sizeof_inst
- linear_isometry.semilinear_isometry_class
- linear_isometry.has_coe_to_fun
- linear_isometry.inhabited
- linear_isometry.monoid
@[instance]
def
semilinear_isometry_class.to_semilinear_map_class
(𝓕 : Type u_11)
{R : out_param (Type u_12)}
{R₂ : out_param (Type u_13)}
[semiring R]
[semiring R₂]
(σ₁₂ : out_param (R →+* R₂))
(E : out_param (Type u_14))
(E₂ : out_param (Type u_15))
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
[self : semilinear_isometry_class 𝓕 σ₁₂ E E₂] :
semilinear_map_class 𝓕 σ₁₂ E E₂
@[class]
structure
semilinear_isometry_class
(𝓕 : Type u_11)
{R : out_param (Type u_12)}
{R₂ : out_param (Type u_13)}
[semiring R]
[semiring R₂]
(σ₁₂ : out_param (R →+* R₂))
(E : out_param (Type u_14))
(E₂ : out_param (Type u_15))
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂] :
Type (max u_11 u_14 u_15)
- coe : 𝓕 → Π (a : E), (λ (_x : E), E₂) a
- coe_injective' : function.injective semilinear_isometry_class.coe
- map_add : ∀ (f : 𝓕) (x y : E), ⇑f (x + y) = ⇑f x + ⇑f y
- map_smulₛₗ : ∀ (f : 𝓕) (r : R) (x : E), ⇑f (r • x) = ⇑σ₁₂ r • ⇑f x
- norm_map : ∀ (f : 𝓕) (x : E), ‖⇑f x‖ = ‖x‖
semilinear_isometry_class F σ E E₂ asserts F is a type of bundled σ-semilinear isometries
E → E₂.
See also linear_isometry_class 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.
Instances of this typeclass
Instances of other typeclasses for semilinear_isometry_class
- semilinear_isometry_class.has_sizeof_inst
@[reducible]
def
linear_isometry_class
(𝓕 : Type u_1)
(R : out_param (Type u_2))
(E : out_param (Type u_3))
(E₂ : out_param (Type u_4))
[semiring R]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R E₂] :
Type (max u_1 u_3 u_4)
linear_isometry_class F R E E₂ asserts F is a type of bundled R-linear isometries
M → M₂.
This is an abbreviation for semilinear_isometry_class F (ring_hom.id R) E E₂.
@[protected]
theorem
semilinear_isometry_class.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₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
[semilinear_isometry_class 𝓕 σ₁₂ E E₂]
(f : 𝓕) :
@[protected, continuity]
theorem
semilinear_isometry_class.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₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
[semilinear_isometry_class 𝓕 σ₁₂ E E₂]
(f : 𝓕) :
@[simp]
theorem
semilinear_isometry_class.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₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
[semilinear_isometry_class 𝓕 σ₁₂ E E₂]
(f : 𝓕)
(x : E) :
@[protected]
theorem
semilinear_isometry_class.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₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
[semilinear_isometry_class 𝓕 σ₁₂ E E₂]
(f : 𝓕) :
lipschitz_with 1 ⇑f
@[protected]
theorem
semilinear_isometry_class.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₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
[semilinear_isometry_class 𝓕 σ₁₂ E E₂]
(f : 𝓕) :
theorem
semilinear_isometry_class.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₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
[semilinear_isometry_class 𝓕 σ₁₂ E E₂]
(f : 𝓕)
(s : set E) :
emetric.diam (⇑f '' s) = emetric.diam s
theorem
semilinear_isometry_class.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₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
[semilinear_isometry_class 𝓕 σ₁₂ E E₂]
(f : 𝓕) :
theorem
semilinear_isometry_class.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₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
[semilinear_isometry_class 𝓕 σ₁₂ E E₂]
(f : 𝓕)
(s : set E) :
metric.diam (⇑f '' s) = metric.diam s
theorem
semilinear_isometry_class.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₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
[semilinear_isometry_class 𝓕 σ₁₂ E E₂]
(f : 𝓕) :
@[protected, instance]
def
semilinear_isometry_class.continuous_semilinear_map_class
{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₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
[s : semilinear_isometry_class 𝓕 σ₁₂ E E₂] :
continuous_semilinear_map_class 𝓕 σ₁₂ E E₂
Equations
- semilinear_isometry_class.continuous_semilinear_map_class = {coe := semilinear_isometry_class.coe s, coe_injective' := _, map_add := _, map_smulₛₗ := _, map_continuous := _}
theorem
linear_isometry.to_linear_map_injective
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂] :
@[simp]
theorem
linear_isometry.to_linear_map_inj
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
{f g : E →ₛₗᵢ[σ₁₂] E₂} :
f.to_linear_map = g.to_linear_map ↔ f = g
@[protected, instance]
def
linear_isometry.semilinear_isometry_class
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂] :
semilinear_isometry_class (E →ₛₗᵢ[σ₁₂] E₂) σ₁₂ E E₂
Equations
- linear_isometry.semilinear_isometry_class = {coe := λ (f : E →ₛₗᵢ[σ₁₂] E₂), f.to_linear_map.to_fun, coe_injective' := _, map_add := _, map_smulₛₗ := _, norm_map := _}
@[protected, instance]
def
linear_isometry.has_coe_to_fun
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂] :
Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun
directly.
Equations
- linear_isometry.has_coe_to_fun = {coe := λ (f : E →ₛₗᵢ[σ₁₂] E₂), f.to_linear_map.to_fun}
@[simp]
theorem
linear_isometry.coe_to_linear_map
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂) :
⇑(f.to_linear_map) = ⇑f
theorem
linear_isometry.coe_injective
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂] :
def
linear_isometry.simps.apply
{R : Type u_1}
{R₂ : Type u_2}
[semiring R]
[semiring R₂]
(σ₁₂ : R →+* R₂)
(E : Type u_3)
(E₂ : Type u_4)
[seminormed_add_comm_group E]
[seminormed_add_comm_group 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
- linear_isometry.simps.apply σ₁₂ E E₂ h = ⇑h
@[protected]
theorem
linear_isometry.congr_arg
{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₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
[semilinear_isometry_class 𝓕 σ₁₂ E E₂]
{f : 𝓕}
{x x' : E} :
@[protected]
theorem
linear_isometry.congr_fun
{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₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
[semilinear_isometry_class 𝓕 σ₁₂ E E₂]
{f g : 𝓕}
(h : f = g)
(x : E) :
@[protected, simp]
@[protected, simp]
@[protected, simp]
@[simp]
theorem
linear_isometry.is_complete_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₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
[semilinear_isometry_class 𝓕 σ₁₂ E E₂]
(f : 𝓕)
{s : set E} :
is_complete (⇑f '' s) ↔ is_complete s
theorem
linear_isometry.is_complete_map_iff
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂)
[ring_hom_surjective σ₁₂]
{p : submodule R E} :
theorem
linear_isometry.is_complete_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₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
[semilinear_isometry_class 𝓕 σ₁₂ E E₂]
(f : 𝓕)
[ring_hom_surjective σ₁₂]
{p : submodule R E} :
is_complete ↑(submodule.map f p) ↔ is_complete ↑p
@[protected, instance]
def
linear_isometry.complete_space_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₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
[semilinear_isometry_class 𝓕 σ₁₂ E E₂]
(f : 𝓕)
[ring_hom_surjective σ₁₂]
(p : submodule R E)
[complete_space ↥p] :
complete_space ↥(submodule.map f p)
@[protected, instance]
def
linear_isometry.complete_space_map'
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂)
[ring_hom_surjective σ₁₂]
(p : submodule R E)
[complete_space ↥p] :
@[simp]
theorem
linear_isometry.dist_map
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂)
(x y : E) :
has_dist.dist (⇑f x) (⇑f y) = has_dist.dist x y
@[simp]
theorem
linear_isometry.edist_map
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂)
(x y : E) :
has_edist.edist (⇑f x) (⇑f y) = has_edist.edist x y
@[protected]
theorem
linear_isometry.injective
{R : Type u_1}
{R₂ : Type u_2}
{E₂ : Type u_6}
{F : Type u_9}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[seminormed_add_comm_group E₂]
[module R₂ E₂]
[normed_add_comm_group F]
[module R F]
(f₁ : F →ₛₗᵢ[σ₁₂] E₂) :
@[protected]
theorem
linear_isometry.lipschitz
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂) :
lipschitz_with 1 ⇑f
@[protected]
theorem
linear_isometry.antilipschitz
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂) :
@[protected, continuity]
theorem
linear_isometry.continuous
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂) :
@[simp]
theorem
linear_isometry.preimage_ball
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group 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
linear_isometry.preimage_sphere
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group 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
linear_isometry.preimage_closed_ball
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂)
(x : E)
(r : ℝ) :
⇑f ⁻¹' metric.closed_ball (⇑f x) r = metric.closed_ball x r
theorem
linear_isometry.ediam_image
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂)
(s : set E) :
emetric.diam (⇑f '' s) = emetric.diam s
theorem
linear_isometry.ediam_range
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂) :
theorem
linear_isometry.diam_image
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂)
(s : set E) :
metric.diam (⇑f '' s) = metric.diam s
theorem
linear_isometry.diam_range
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂) :
def
linear_isometry.to_continuous_linear_map
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂) :
Interpret a linear isometry as a continuous linear map.
Equations
- f.to_continuous_linear_map = {to_linear_map := f.to_linear_map, cont := _}
theorem
linear_isometry.to_continuous_linear_map_injective
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂] :
@[simp]
theorem
linear_isometry.to_continuous_linear_map_inj
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
{f g : E →ₛₗᵢ[σ₁₂] E₂} :
@[simp]
theorem
linear_isometry.coe_to_continuous_linear_map
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂) :
⇑(f.to_continuous_linear_map) = ⇑f
@[simp]
theorem
linear_isometry.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₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂)
{α : Type u_3}
[topological_space α]
{g : α → E} :
continuous (⇑f ∘ g) ↔ continuous g
def
linear_isometry.id
{R : Type u_1}
{E : Type u_5}
[semiring R]
[seminormed_add_comm_group E]
[module R E] :
The identity linear isometry.
Equations
- linear_isometry.id = {to_linear_map := linear_map.id _inst_29, norm_map' := _}
@[simp]
theorem
linear_isometry.coe_id
{R : Type u_1}
{E : Type u_5}
[semiring R]
[seminormed_add_comm_group E]
[module R E] :
@[simp]
theorem
linear_isometry.id_apply
{R : Type u_1}
{E : Type u_5}
[semiring R]
[seminormed_add_comm_group E]
[module R E]
(x : E) :
⇑linear_isometry.id x = x
@[simp]
theorem
linear_isometry.id_to_linear_map
{R : Type u_1}
{E : Type u_5}
[semiring R]
[seminormed_add_comm_group E]
[module R E] :
@[simp]
theorem
linear_isometry.id_to_continuous_linear_map
{R : Type u_1}
{E : Type u_5}
[semiring R]
[seminormed_add_comm_group E]
[module R E] :
@[protected, instance]
def
linear_isometry.inhabited
{R : Type u_1}
{E : Type u_5}
[semiring R]
[seminormed_add_comm_group E]
[module R E] :
Equations
- linear_isometry.inhabited = {default := linear_isometry.id _inst_29}
def
linear_isometry.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₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[seminormed_add_comm_group E₃]
[module R E]
[module R₂ E₂]
[module R₃ E₃]
(g : E₂ →ₛₗᵢ[σ₂₃] E₃)
(f : E →ₛₗᵢ[σ₁₂] E₂) :
Composition of linear isometries.
Equations
- g.comp f = {to_linear_map := g.to_linear_map.comp f.to_linear_map, norm_map' := _}
@[simp]
theorem
linear_isometry.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₃}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[seminormed_add_comm_group E₃]
[module R E]
[module R₂ E₂]
[module R₃ E₃]
(g : E₂ →ₛₗᵢ[σ₂₃] E₃)
(f : E →ₛₗᵢ[σ₁₂] E₂) :
@[simp]
theorem
linear_isometry.id_comp
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂) :
linear_isometry.id.comp f = f
@[simp]
theorem
linear_isometry.comp_id
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂) :
f.comp linear_isometry.id = f
theorem
linear_isometry.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₄}
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[ring_hom_comp_triple σ₁₂ σ₂₄ σ₁₄]
[ring_hom_comp_triple σ₂₃ σ₃₄ σ₂₄]
[ring_hom_comp_triple σ₁₃ σ₃₄ σ₁₄]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[seminormed_add_comm_group E₃]
[seminormed_add_comm_group E₄]
[module R E]
[module R₂ E₂]
[module R₃ E₃]
[module R₄ E₄]
(f : E₃ →ₛₗᵢ[σ₃₄] E₄)
(g : E₂ →ₛₗᵢ[σ₂₃] E₃)
(h : E →ₛₗᵢ[σ₁₂] E₂) :
@[protected, instance]
def
linear_isometry.monoid
{R : Type u_1}
{E : Type u_5}
[semiring R]
[seminormed_add_comm_group E]
[module R E] :
Equations
- linear_isometry.monoid = {mul := linear_isometry.comp _inst_29, mul_assoc := _, one := linear_isometry.id _inst_29, one_mul := _, mul_one := _, npow := npow_rec (mul_one_class.to_has_mul (E →ₗᵢ[R] E)), npow_zero' := _, npow_succ' := _}
@[simp]
theorem
linear_isometry.coe_one
{R : Type u_1}
{E : Type u_5}
[semiring R]
[seminormed_add_comm_group E]
[module R E] :
theorem
linear_isometry.one_def
{R : Type u_1}
{E : Type u_5}
[semiring R]
[seminormed_add_comm_group E]
[module R E] :
def
linear_map.to_linear_isometry
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(f : E →ₛₗ[σ₁₂] E₂)
(hf : isometry ⇑f) :
Construct a linear_isometry from a linear_map satisfying isometry.
Equations
- f.to_linear_isometry hf = {to_linear_map := {to_fun := f.to_fun, map_add' := _, map_smul' := _}, norm_map' := _}
def
submodule.subtypeₗᵢ
{E : Type u_5}
[seminormed_add_comm_group E]
{R' : Type u_11}
[ring R']
[module R' E]
(p : submodule R' E) :
@[simp]
theorem
submodule.subtypeₗᵢ_to_linear_map
{E : Type u_5}
[seminormed_add_comm_group E]
{R' : Type u_11}
[ring R']
[module R' E]
(p : submodule R' E) :
@[simp]
theorem
submodule.subtypeₗᵢ_to_continuous_linear_map
{E : Type u_5}
[seminormed_add_comm_group E]
{R' : Type u_11}
[ring R']
[module R' E]
(p : submodule R' E) :
structure
linear_isometry_equiv
{R : Type u_1}
{R₂ : Type u_2}
[semiring R]
[semiring R₂]
(σ₁₂ : R →+* R₂)
{σ₂₁ : R₂ →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
(E : Type u_11)
(E₂ : Type u_12)
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂] :
Type (max u_11 u_12)
A semilinear isometric equivalence between two normed vector spaces.
Instances for linear_isometry_equiv
@[instance]
def
semilinear_isometry_equiv_class.to_semilinear_equiv_class
(𝓕 : Type u_11)
{R : out_param (Type u_12)}
{R₂ : out_param (Type u_13)}
[semiring R]
[semiring R₂]
(σ₁₂ : out_param (R →+* R₂))
{σ₂₁ : out_param (R₂ →+* R)}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
(E : out_param (Type u_14))
(E₂ : out_param (Type u_15))
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
[self : semilinear_isometry_equiv_class 𝓕 σ₁₂ E E₂] :
semilinear_equiv_class 𝓕 σ₁₂ E E₂
@[class]
structure
semilinear_isometry_equiv_class
(𝓕 : Type u_11)
{R : out_param (Type u_12)}
{R₂ : out_param (Type u_13)}
[semiring R]
[semiring R₂]
(σ₁₂ : out_param (R →+* R₂))
{σ₂₁ : out_param (R₂ →+* R)}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
(E : out_param (Type u_14))
(E₂ : out_param (Type u_15))
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂] :
Type (max u_11 u_14 u_15)
- coe : 𝓕 → E → E₂
- inv : 𝓕 → E₂ → E
- left_inv : ∀ (e : 𝓕), function.left_inverse (semilinear_isometry_equiv_class.inv e) (semilinear_isometry_equiv_class.coe e)
- right_inv : ∀ (e : 𝓕), function.right_inverse (semilinear_isometry_equiv_class.inv e) (semilinear_isometry_equiv_class.coe e)
- coe_injective' : ∀ (e g : 𝓕), semilinear_isometry_equiv_class.coe e = semilinear_isometry_equiv_class.coe g → semilinear_isometry_equiv_class.inv e = semilinear_isometry_equiv_class.inv g → e = g
- map_add : ∀ (f : 𝓕) (a b : E), ⇑f (a + b) = ⇑f a + ⇑f b
- map_smulₛₗ : ∀ (f : 𝓕) (r : R) (x : E), ⇑f (r • x) = ⇑σ₁₂ r • ⇑f x
- norm_map : ∀ (f : 𝓕) (x : E), ‖⇑f x‖ = ‖x‖
semilinear_isometry_equiv_class F σ E E₂ asserts F is a type of bundled σ-semilinear
isometric equivs E → E₂.
See also linear_isometry_equiv_class 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.
Instances of this typeclass
Instances of other typeclasses for semilinear_isometry_equiv_class
- semilinear_isometry_equiv_class.has_sizeof_inst
@[reducible]
def
linear_isometry_equiv_class
(𝓕 : Type u_1)
(R : out_param (Type u_2))
(E : out_param (Type u_3))
(E₂ : out_param (Type u_4))
[semiring R]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R E₂] :
Type (max u_1 u_3 u_4)
linear_isometry_equiv_class F R E E₂ asserts F is a type of bundled R-linear isometries
M → M₂.
This is an abbreviation for semilinear_isometry_equiv_class F (ring_hom.id R) E E₂.
@[protected, nolint, instance]
def
semilinear_isometry_equiv_class.semilinear_isometry_class
{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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
[s : semilinear_isometry_equiv_class 𝓕 σ₁₂ E E₂] :
semilinear_isometry_class 𝓕 σ₁₂ E E₂
Equations
- semilinear_isometry_equiv_class.semilinear_isometry_class 𝓕 = {coe := semilinear_isometry_equiv_class.coe s, coe_injective' := _, map_add := _, map_smulₛₗ := _, norm_map := _}
theorem
linear_isometry_equiv.to_linear_equiv_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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂] :
@[simp]
theorem
linear_isometry_equiv.to_linear_equiv_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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
{f g : E ≃ₛₗᵢ[σ₁₂] E₂} :
f.to_linear_equiv = g.to_linear_equiv ↔ f = g
@[protected, instance]
def
linear_isometry_equiv.semilinear_isometry_equiv_class
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂] :
semilinear_isometry_equiv_class (E ≃ₛₗᵢ[σ₁₂] E₂) σ₁₂ E E₂
Equations
- linear_isometry_equiv.semilinear_isometry_equiv_class = {coe := λ (e : E ≃ₛₗᵢ[σ₁₂] E₂), e.to_linear_equiv.to_fun, inv := λ (e : E ≃ₛₗᵢ[σ₁₂] E₂), e.to_linear_equiv.inv_fun, left_inv := _, right_inv := _, coe_injective' := _, map_add := _, map_smulₛₗ := _, norm_map := _}
@[protected, instance]
def
linear_isometry_equiv.has_coe_to_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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂] :
Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun
directly.
Equations
- linear_isometry_equiv.has_coe_to_fun = {coe := λ (f : E ≃ₛₗᵢ[σ₁₂] E₂), f.to_linear_equiv.to_fun}
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂] :
@[simp]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗ[σ₁₂] E₂)
(he : ∀ (x : E), ‖⇑e x‖ = ‖x‖) :
@[simp]
theorem
linear_isometry_equiv.coe_to_linear_equiv
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂) :
⇑(e.to_linear_equiv) = ⇑e
@[ext]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
{e e' : E ≃ₛₗᵢ[σ₁₂] E₂}
(h : ∀ (x : E), ⇑e x = ⇑e' x) :
e = e'
@[protected]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
{f : E ≃ₛₗᵢ[σ₁₂] E₂}
{x x' : E} :
@[protected]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
{f g : E ≃ₛₗᵢ[σ₁₂] E₂}
(h : f = g)
(x : E) :
def
linear_isometry_equiv.of_bounds
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group 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 linear_isometry_equiv from a linear_equiv and two inequalities:
∀ x, ‖e x‖ ≤ ‖x‖ and ∀ y, ‖e.symm y‖ ≤ ‖y‖.
Equations
- linear_isometry_equiv.of_bounds e h₁ h₂ = {to_linear_equiv := e, norm_map' := _}
@[simp]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(x : E) :
def
linear_isometry_equiv.to_linear_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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂) :
Reinterpret a linear_isometry_equiv as a linear_isometry.
Equations
- e.to_linear_isometry = {to_linear_map := ↑(e.to_linear_equiv), norm_map' := _}
theorem
linear_isometry_equiv.to_linear_isometry_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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂] :
@[simp]
theorem
linear_isometry_equiv.to_linear_isometry_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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
{f g : E ≃ₛₗᵢ[σ₁₂] E₂} :
f.to_linear_isometry = g.to_linear_isometry ↔ f = g
@[simp]
theorem
linear_isometry_equiv.coe_to_linear_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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂) :
⇑(e.to_linear_isometry) = ⇑e
@[protected]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂) :
def
linear_isometry_equiv.to_isometry_equiv
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂) :
E ≃ᵢ E₂
Reinterpret a linear_isometry_equiv as an isometry_equiv.
Equations
- e.to_isometry_equiv = {to_equiv := e.to_linear_equiv.to_equiv, isometry_to_fun := _}
theorem
linear_isometry_equiv.to_isometry_equiv_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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂] :
@[simp]
theorem
linear_isometry_equiv.to_isometry_equiv_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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
{f g : E ≃ₛₗᵢ[σ₁₂] E₂} :
f.to_isometry_equiv = g.to_isometry_equiv ↔ f = g
@[simp]
theorem
linear_isometry_equiv.coe_to_isometry_equiv
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂) :
⇑(e.to_isometry_equiv) = ⇑e
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂) :
def
linear_isometry_equiv.to_homeomorph
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂) :
E ≃ₜ E₂
Reinterpret a linear_isometry_equiv as an homeomorph.
Equations
theorem
linear_isometry_equiv.to_homeomorph_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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂] :
@[simp]
theorem
linear_isometry_equiv.to_homeomorph_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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
{f g : E ≃ₛₗᵢ[σ₁₂] E₂} :
f.to_homeomorph = g.to_homeomorph ↔ f = g
@[simp]
theorem
linear_isometry_equiv.coe_to_homeomorph
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂) :
⇑(e.to_homeomorph) = ⇑e
@[protected]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂) :
@[protected]
theorem
linear_isometry_equiv.continuous_at
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
{x : E} :
continuous_at ⇑e x
@[protected]
theorem
linear_isometry_equiv.continuous_on
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
{s : set E} :
continuous_on ⇑e s
@[protected]
theorem
linear_isometry_equiv.continuous_within_at
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
{s : set E}
{x : E} :
continuous_within_at ⇑e s x
def
linear_isometry_equiv.to_continuous_linear_equiv
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂) :
Interpret a linear_isometry_equiv as a continuous linear equiv.
Equations
- e.to_continuous_linear_equiv = {to_linear_equiv := {to_fun := e.to_linear_isometry.to_continuous_linear_map.to_linear_map.to_fun, map_add' := _, map_smul' := _, inv_fun := e.to_homeomorph.to_equiv.inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
theorem
linear_isometry_equiv.to_continuous_linear_equiv_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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂] :
@[simp]
theorem
linear_isometry_equiv.to_continuous_linear_equiv_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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
{f g : E ≃ₛₗᵢ[σ₁₂] E₂} :
@[simp]
theorem
linear_isometry_equiv.coe_to_continuous_linear_equiv
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂) :
def
linear_isometry_equiv.refl
(R : Type u_1)
(E : Type u_5)
[semiring R]
[seminormed_add_comm_group E]
[module R E] :
Identity map as a linear_isometry_equiv.
Equations
- linear_isometry_equiv.refl R E = {to_linear_equiv := linear_equiv.refl R E _inst_29, norm_map' := _}
def
linear_isometry_equiv.ulift
(R : Type u_1)
(E : Type u_5)
[semiring R]
[seminormed_add_comm_group E]
[module R E] :
Linear isometry equiv between a space and its lift to another universe.
Equations
@[protected, instance]
def
linear_isometry_equiv.inhabited
{R : Type u_1}
{E : Type u_5}
[semiring R]
[seminormed_add_comm_group E]
[module R E] :
Equations
- linear_isometry_equiv.inhabited = {default := linear_isometry_equiv.refl R E _inst_29}
@[simp]
theorem
linear_isometry_equiv.coe_refl
{R : Type u_1}
{E : Type u_5}
[semiring R]
[seminormed_add_comm_group E]
[module R E] :
⇑(linear_isometry_equiv.refl R E) = id
def
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂) :
The inverse linear_isometry_equiv.
Equations
- e.symm = {to_linear_equiv := e.to_linear_equiv.symm, norm_map' := _}
@[simp]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(x : E₂) :
@[simp]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(x : E) :
@[simp]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
{x : E} :
@[simp]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂) :
@[simp]
theorem
linear_isometry_equiv.to_linear_equiv_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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂) :
@[simp]
theorem
linear_isometry_equiv.to_isometry_equiv_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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂) :
@[simp]
theorem
linear_isometry_equiv.to_homeomorph_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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂) :
def
linear_isometry_equiv.simps.apply
{R : Type u_1}
{R₂ : Type u_2}
[semiring R]
[semiring R₂]
(σ₁₂ : R →+* R₂)
{σ₂₁ : R₂ →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
(E : Type u_3)
(E₂ : Type u_4)
[seminormed_add_comm_group E]
[seminormed_add_comm_group 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
- linear_isometry_equiv.simps.apply σ₁₂ E E₂ h = ⇑h
def
linear_isometry_equiv.simps.symm_apply
{R : Type u_1}
{R₂ : Type u_2}
[semiring R]
[semiring R₂]
(σ₁₂ : R →+* R₂)
{σ₂₁ : R₂ →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
(E : Type u_3)
(E₂ : Type u_4)
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(h : E ≃ₛₗᵢ[σ₁₂] E₂) :
E₂ → E
See Note [custom simps projection]
Equations
- linear_isometry_equiv.simps.symm_apply σ₁₂ E E₂ h = ⇑(h.symm)
def
linear_isometry_equiv.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₂}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[ring_hom_inv_pair σ₁₃ σ₃₁]
[ring_hom_inv_pair σ₃₁ σ₁₃]
[ring_hom_inv_pair σ₂₃ σ₃₂]
[ring_hom_inv_pair σ₃₂ σ₂₃]
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[seminormed_add_comm_group E₃]
[module R E]
[module R₂ E₂]
[module R₃ E₃]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(e' : E₂ ≃ₛₗᵢ[σ₂₃] E₃) :
Composition of linear_isometry_equivs as a linear_isometry_equiv.
Equations
- e.trans e' = {to_linear_equiv := e.to_linear_equiv.trans e'.to_linear_equiv, norm_map' := _}
@[simp]
theorem
linear_isometry_equiv.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₂}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[ring_hom_inv_pair σ₁₃ σ₃₁]
[ring_hom_inv_pair σ₃₁ σ₁₃]
[ring_hom_inv_pair σ₂₃ σ₃₂]
[ring_hom_inv_pair σ₃₂ σ₂₃]
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[seminormed_add_comm_group E₃]
[module R E]
[module R₂ E₂]
[module R₃ E₃]
(e₁ : E ≃ₛₗᵢ[σ₁₂] E₂)
(e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃) :
@[simp]
theorem
linear_isometry_equiv.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₂}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[ring_hom_inv_pair σ₁₃ σ₃₁]
[ring_hom_inv_pair σ₃₁ σ₁₃]
[ring_hom_inv_pair σ₂₃ σ₃₂]
[ring_hom_inv_pair σ₃₂ σ₂₃]
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[seminormed_add_comm_group E₃]
[module R E]
[module R₂ E₂]
[module R₃ E₃]
(e₁ : E ≃ₛₗᵢ[σ₁₂] E₂)
(e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃)
(c : E) :
@[simp]
theorem
linear_isometry_equiv.to_linear_equiv_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₂}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[ring_hom_inv_pair σ₁₃ σ₃₁]
[ring_hom_inv_pair σ₃₁ σ₁₃]
[ring_hom_inv_pair σ₂₃ σ₃₂]
[ring_hom_inv_pair σ₃₂ σ₂₃]
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[seminormed_add_comm_group E₃]
[module R E]
[module R₂ E₂]
[module R₃ E₃]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(e' : E₂ ≃ₛₗᵢ[σ₂₃] E₃) :
(e.trans e').to_linear_equiv = e.to_linear_equiv.trans e'.to_linear_equiv
@[simp]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂) :
e.trans (linear_isometry_equiv.refl R₂ E₂) = e
@[simp]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂) :
(linear_isometry_equiv.refl R E).trans e = e
@[simp]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂) :
e.trans e.symm = linear_isometry_equiv.refl R E
@[simp]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂) :
e.symm.trans e = linear_isometry_equiv.refl R₂ E₂
@[simp]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂) :
@[simp]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂) :
@[simp]
theorem
linear_isometry_equiv.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₂}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[ring_hom_inv_pair σ₁₃ σ₃₁]
[ring_hom_inv_pair σ₃₁ σ₁₃]
[ring_hom_inv_pair σ₂₃ σ₃₂]
[ring_hom_inv_pair σ₃₂ σ₂₃]
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[seminormed_add_comm_group E₃]
[module R E]
[module R₂ E₂]
[module R₃ E₃]
(e₁ : E ≃ₛₗᵢ[σ₁₂] E₂)
(e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃) :
theorem
linear_isometry_equiv.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₂}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[ring_hom_inv_pair σ₁₃ σ₃₁]
[ring_hom_inv_pair σ₃₁ σ₁₃]
[ring_hom_inv_pair σ₂₃ σ₃₂]
[ring_hom_inv_pair σ₃₂ σ₂₃]
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[seminormed_add_comm_group E₃]
[module R E]
[module R₂ E₂]
[module R₃ E₃]
(e₁ : E ≃ₛₗᵢ[σ₁₂] E₂)
(e₂ : E₂ ≃ₛₗᵢ[σ₂₃] E₃) :
theorem
linear_isometry_equiv.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₃}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[ring_hom_inv_pair σ₁₃ σ₃₁]
[ring_hom_inv_pair σ₃₁ σ₁₃]
[ring_hom_inv_pair σ₂₃ σ₃₂]
[ring_hom_inv_pair σ₃₂ σ₂₃]
[ring_hom_inv_pair σ₁₄ σ₄₁]
[ring_hom_inv_pair σ₄₁ σ₁₄]
[ring_hom_inv_pair σ₂₄ σ₄₂]
[ring_hom_inv_pair σ₄₂ σ₂₄]
[ring_hom_inv_pair σ₃₄ σ₄₃]
[ring_hom_inv_pair σ₄₃ σ₃₄]
[ring_hom_comp_triple σ₁₂ σ₂₃ σ₁₃]
[ring_hom_comp_triple σ₁₂ σ₂₄ σ₁₄]
[ring_hom_comp_triple σ₂₃ σ₃₄ σ₂₄]
[ring_hom_comp_triple σ₁₃ σ₃₄ σ₁₄]
[ring_hom_comp_triple σ₃₂ σ₂₁ σ₃₁]
[ring_hom_comp_triple σ₄₂ σ₂₁ σ₄₁]
[ring_hom_comp_triple σ₄₃ σ₃₂ σ₄₂]
[ring_hom_comp_triple σ₄₃ σ₃₁ σ₄₁]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[seminormed_add_comm_group E₃]
[seminormed_add_comm_group E₄]
[module R E]
[module R₂ E₂]
[module R₃ E₃]
[module R₄ E₄]
(eEE₂ : E ≃ₛₗᵢ[σ₁₂] E₂)
(eE₂E₃ : E₂ ≃ₛₗᵢ[σ₂₃] E₃)
(eE₃E₄ : E₃ ≃ₛₗᵢ[σ₃₄] E₄) :
@[protected, instance]
def
linear_isometry_equiv.group
{R : Type u_1}
{E : Type u_5}
[semiring R]
[seminormed_add_comm_group E]
[module R E] :
Equations
- linear_isometry_equiv.group = {mul := λ (e₁ e₂ : E ≃ₗᵢ[R] E), e₂.trans e₁, mul_assoc := _, one := linear_isometry_equiv.refl R E _inst_29, one_mul := _, mul_one := _, npow := div_inv_monoid.npow._default (linear_isometry_equiv.refl R E) (λ (e₁ e₂ : E ≃ₗᵢ[R] E), e₂.trans e₁) linear_isometry_equiv.group._proof_6 linear_isometry_equiv.group._proof_7, npow_zero' := _, npow_succ' := _, inv := linear_isometry_equiv.symm _inst_29, div := div_inv_monoid.div._default (λ (e₁ e₂ : E ≃ₗᵢ[R] E), e₂.trans e₁) linear_isometry_equiv.group._proof_10 (linear_isometry_equiv.refl R E) linear_isometry_equiv.group._proof_11 linear_isometry_equiv.group._proof_12 (div_inv_monoid.npow._default (linear_isometry_equiv.refl R E) (λ (e₁ e₂ : E ≃ₗᵢ[R] E), e₂.trans e₁) linear_isometry_equiv.group._proof_6 linear_isometry_equiv.group._proof_7) linear_isometry_equiv.group._proof_13 linear_isometry_equiv.group._proof_14 linear_isometry_equiv.symm, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default (λ (e₁ e₂ : E ≃ₗᵢ[R] E), e₂.trans e₁) linear_isometry_equiv.group._proof_16 (linear_isometry_equiv.refl R E) linear_isometry_equiv.group._proof_17 linear_isometry_equiv.group._proof_18 (div_inv_monoid.npow._default (linear_isometry_equiv.refl R E) (λ (e₁ e₂ : E ≃ₗᵢ[R] E), e₂.trans e₁) linear_isometry_equiv.group._proof_6 linear_isometry_equiv.group._proof_7) linear_isometry_equiv.group._proof_19 linear_isometry_equiv.group._proof_20 linear_isometry_equiv.symm, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _}
@[simp]
theorem
linear_isometry_equiv.coe_one
{R : Type u_1}
{E : Type u_5}
[semiring R]
[seminormed_add_comm_group E]
[module R E] :
theorem
linear_isometry_equiv.one_def
{R : Type u_1}
{E : Type u_5}
[semiring R]
[seminormed_add_comm_group E]
[module R E] :
1 = linear_isometry_equiv.refl R E
Lemmas about mixing the group structure with definitions. Because we have multiple ways to
express linear_isometry_equiv.refl, linear_isometry_equiv.symm, and
linear_isometry_equiv.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
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂) :
@[simp]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂) :
@[simp]
theorem
linear_isometry_equiv.refl_mul
{R : Type u_1}
{E : Type u_5}
[semiring R]
[seminormed_add_comm_group E]
[module R E]
(e : E ≃ₗᵢ[R] E) :
linear_isometry_equiv.refl R E * e = e
@[simp]
theorem
linear_isometry_equiv.mul_refl
{R : Type u_1}
{E : Type u_5}
[semiring R]
[seminormed_add_comm_group E]
[module R E]
(e : E ≃ₗᵢ[R] E) :
e * linear_isometry_equiv.refl R E = e
@[protected, instance]
def
linear_isometry_equiv.continuous_linear_equiv.has_coe_t
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂] :
Reinterpret a linear_isometry_equiv as a continuous_linear_equiv.
Equations
- linear_isometry_equiv.continuous_linear_equiv.has_coe_t = {coe := λ (e : E ≃ₛₗᵢ[σ₁₂] E₂), {to_linear_equiv := e.to_linear_equiv, continuous_to_fun := _, continuous_inv_fun := _}}
@[protected, instance]
def
linear_isometry_equiv.continuous_linear_map.has_coe_t
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂] :
@[simp]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂) :
@[simp]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂) :
@[simp]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂) :
@[simp]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂) :
@[simp]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(x y : E) :
@[simp]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(x y : E) :
@[simp]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(c : R)
(x : E) :
@[simp]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(x : E) :
@[simp]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(x y : E) :
has_dist.dist (⇑e x) (⇑e y) = has_dist.dist x y
@[simp]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(x y : E) :
has_edist.edist (⇑e x) (⇑e y) = has_edist.edist x y
@[protected]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂) :
@[protected]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂) :
@[protected]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂) :
@[simp]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
{x y : E} :
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
{x y : E}
(h : x ≠ y) :
@[protected]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂) :
lipschitz_with 1 ⇑e
@[protected]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂) :
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(s : set E) :
@[simp]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(s : set E) :
emetric.diam (⇑e '' s) = emetric.diam s
@[simp]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(s : set E) :
metric.diam (⇑e '' s) = metric.diam s
@[simp]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group 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
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group 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
linear_isometry_equiv.preimage_closed_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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(x : E₂)
(r : ℝ) :
⇑e ⁻¹' metric.closed_ball x r = metric.closed_ball (⇑(e.symm) x) r
@[simp]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group 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
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group 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
linear_isometry_equiv.image_closed_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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(x : E)
(r : ℝ) :
⇑e '' metric.closed_ball x r = metric.closed_ball (⇑e x) r
@[simp]
theorem
linear_isometry_equiv.comp_continuous_on_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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
{α : Type u_11}
[topological_space α]
{f : α → E}
{s : set α} :
continuous_on (⇑e ∘ f) s ↔ continuous_on f s
@[simp]
theorem
linear_isometry_equiv.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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
{α : Type u_11}
[topological_space α]
{f : α → E} :
continuous (⇑e ∘ f) ↔ continuous f
@[protected, instance]
def
linear_isometry_equiv.complete_space_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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(e : E ≃ₛₗᵢ[σ₁₂] E₂)
(p : submodule R E)
[complete_space ↥p] :
noncomputable
def
linear_isometry_equiv.of_surjective
{R : Type u_1}
{R₂ : Type u_2}
{E₂ : Type u_6}
{F : Type u_9}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E₂]
[module R₂ E₂]
[normed_add_comm_group F]
[module R F]
(f : F →ₛₗᵢ[σ₁₂] E₂)
(hfr : function.surjective ⇑f) :
Construct a linear isometry equiv from a surjective linear isometry.
Equations
- linear_isometry_equiv.of_surjective f hfr = {to_linear_equiv := {to_fun := (linear_equiv.of_bijective f.to_linear_map _).to_fun, map_add' := _, map_smul' := _, inv_fun := (linear_equiv.of_bijective f.to_linear_map _).inv_fun, left_inv := _, right_inv := _}, norm_map' := _}
@[simp]
theorem
linear_isometry_equiv.coe_of_surjective
{R : Type u_1}
{R₂ : Type u_2}
{E₂ : Type u_6}
{F : Type u_9}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E₂]
[module R₂ E₂]
[normed_add_comm_group F]
[module R F]
(f : F →ₛₗᵢ[σ₁₂] E₂)
(hfr : function.surjective ⇑f) :
⇑(linear_isometry_equiv.of_surjective f hfr) = ⇑f
def
linear_isometry_equiv.of_linear_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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂)
(g : E₂ →ₛₗ[σ₂₁] E)
(h₁ : f.to_linear_map.comp g = linear_map.id)
(h₂ : g.comp f.to_linear_map = linear_map.id) :
If a linear isometry has an inverse, it is a linear isometric equivalence.
Equations
- linear_isometry_equiv.of_linear_isometry f g h₁ h₂ = {to_linear_equiv := {to_fun := (linear_equiv.of_linear f.to_linear_map g h₁ h₂).to_fun, map_add' := _, map_smul' := _, inv_fun := (linear_equiv.of_linear f.to_linear_map g h₁ h₂).inv_fun, left_inv := _, right_inv := _}, norm_map' := _}
@[simp]
theorem
linear_isometry_equiv.coe_of_linear_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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂)
(g : E₂ →ₛₗ[σ₂₁] E)
(h₁ : f.to_linear_map.comp g = linear_map.id)
(h₂ : g.comp f.to_linear_map = linear_map.id) :
⇑(linear_isometry_equiv.of_linear_isometry f g h₁ h₂) = ⇑f
@[simp]
theorem
linear_isometry_equiv.coe_of_linear_isometry_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}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
(f : E →ₛₗᵢ[σ₁₂] E₂)
(g : E₂ →ₛₗ[σ₂₁] E)
(h₁ : f.to_linear_map.comp g = linear_map.id)
(h₂ : g.comp f.to_linear_map = linear_map.id) :
⇑((linear_isometry_equiv.of_linear_isometry f g h₁ h₂).symm) = ⇑g
def
linear_isometry_equiv.neg
(R : Type u_1)
{E : Type u_5}
[semiring R]
[seminormed_add_comm_group E]
[module R E] :
The negation operation on a normed space E, considered as a linear isometry equivalence.
Equations
- linear_isometry_equiv.neg R = {to_linear_equiv := {to_fun := (linear_equiv.neg R).to_fun, map_add' := _, map_smul' := _, inv_fun := (linear_equiv.neg R).inv_fun, left_inv := _, right_inv := _}, norm_map' := _}
@[simp]
theorem
linear_isometry_equiv.coe_neg
{R : Type u_1}
{E : Type u_5}
[semiring R]
[seminormed_add_comm_group E]
[module R E] :
⇑(linear_isometry_equiv.neg R) = λ (x : E), -x
@[simp]
theorem
linear_isometry_equiv.symm_neg
{R : Type u_1}
{E : Type u_5}
[semiring R]
[seminormed_add_comm_group E]
[module R E] :
def
linear_isometry_equiv.prod_assoc
(R : Type u_1)
(E : Type u_5)
(E₂ : Type u_6)
(E₃ : Type u_7)
[semiring R]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[seminormed_add_comm_group E₃]
[module R E]
[module R E₂]
[module R E₃] :
The natural equivalence (E × E₂) × E₃ ≃ E × (E₂ × E₃) is a linear isometry.
Equations
- linear_isometry_equiv.prod_assoc R E E₂ E₃ = {to_linear_equiv := {to_fun := ⇑(equiv.prod_assoc E E₂ E₃), map_add' := _, map_smul' := _, inv_fun := ⇑((equiv.prod_assoc E E₂ E₃).symm), left_inv := _, right_inv := _}, norm_map' := _}
@[simp]
theorem
linear_isometry_equiv.coe_prod_assoc
(R : Type u_1)
(E : Type u_5)
(E₂ : Type u_6)
(E₃ : Type u_7)
[semiring R]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[seminormed_add_comm_group E₃]
[module R E]
[module R E₂]
[module R E₃] :
⇑(linear_isometry_equiv.prod_assoc R E E₂ E₃) = ⇑(equiv.prod_assoc E E₂ E₃)
@[simp]
theorem
linear_isometry_equiv.coe_prod_assoc_symm
(R : Type u_1)
(E : Type u_5)
(E₂ : Type u_6)
(E₃ : Type u_7)
[semiring R]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[seminormed_add_comm_group E₃]
[module R E]
[module R E₂]
[module R E₃] :
⇑((linear_isometry_equiv.prod_assoc R E E₂ E₃).symm) = ⇑((equiv.prod_assoc E E₂ E₃).symm)
@[simp]
theorem
linear_isometry_equiv.of_top_apply
(E : Type u_5)
[seminormed_add_comm_group E]
{R : Type u_1}
[ring R]
[module R E]
(p : submodule R E)
(hp : p = ⊤)
(ᾰ : ↥p) :
⇑(linear_isometry_equiv.of_top E p hp) ᾰ = ↑ᾰ
@[simp]
theorem
linear_isometry_equiv.of_top_to_linear_equiv
(E : Type u_5)
[seminormed_add_comm_group E]
{R : Type u_1}
[ring R]
[module R E]
(p : submodule R E)
(hp : p = ⊤) :
(linear_isometry_equiv.of_top E p hp).to_linear_equiv = linear_equiv.of_top p hp
@[simp]
theorem
linear_isometry_equiv.of_top_symm_apply_coe
(E : Type u_5)
[seminormed_add_comm_group E]
{R : Type u_1}
[ring R]
[module R E]
(p : submodule R E)
(hp : p = ⊤)
(x : E) :
↑(⇑((linear_isometry_equiv.of_top E p hp).symm) x) = x
def
linear_isometry_equiv.of_top
(E : Type u_5)
[seminormed_add_comm_group E]
{R : Type u_1}
[ring R]
[module R E]
(p : submodule R E)
(hp : p = ⊤) :
If p is a submodule that is equal to ⊤, then linear_isometry_equiv.of_top p hp is the
"identity" equivalence between p and E.
Equations
- linear_isometry_equiv.of_top E p hp = {to_linear_equiv := linear_equiv.of_top p hp, norm_map' := _}
def
linear_isometry_equiv.of_eq
{E : Type u_5}
[seminormed_add_comm_group E]
{R' : Type u_12}
[ring R']
[module R' E]
(p q : submodule R' E)
(hpq : p = q) :
linear_equiv.of_eq as a linear_isometry_equiv.
Equations
- linear_isometry_equiv.of_eq p q hpq = {to_linear_equiv := {to_fun := (linear_equiv.of_eq p q hpq).to_fun, map_add' := _, map_smul' := _, inv_fun := (linear_equiv.of_eq p q hpq).inv_fun, left_inv := _, right_inv := _}, norm_map' := _}
@[simp]
theorem
linear_isometry_equiv.coe_of_eq_apply
{E : Type u_5}
[seminormed_add_comm_group E]
{R' : Type u_12}
[ring R']
[module R' E]
{p q : submodule R' E}
(h : p = q)
(x : ↥p) :
↑(⇑(linear_isometry_equiv.of_eq p q h) x) = ↑x
@[simp]
theorem
linear_isometry_equiv.of_eq_symm
{E : Type u_5}
[seminormed_add_comm_group E]
{R' : Type u_12}
[ring R']
[module R' E]
{p q : submodule R' E}
(h : p = q) :
(linear_isometry_equiv.of_eq p q h).symm = linear_isometry_equiv.of_eq q p _
@[simp]
theorem
linear_isometry_equiv.of_eq_rfl
{E : Type u_5}
[seminormed_add_comm_group E]
{R' : Type u_12}
[ring R']
[module R' E]
{p : submodule R' E} :
theorem
basis.ext_linear_isometry
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
{ι : Type u_3}
(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_linear_isometry_equiv
{R : Type u_1}
{R₂ : Type u_2}
{E : Type u_5}
{E₂ : Type u_6}
[semiring R]
[semiring R₂]
{σ₁₂ : R →+* R₂}
{σ₂₁ : R₂ →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
[seminormed_add_comm_group E]
[seminormed_add_comm_group E₂]
[module R E]
[module R₂ E₂]
{ι : Type u_3}
(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.
@[simp]
theorem
linear_isometry.equiv_range_apply_coe
{E : Type u_5}
{F : Type u_9}
[seminormed_add_comm_group E]
[normed_add_comm_group F]
{R : Type u_1}
{S : Type u_2}
[semiring R]
[ring S]
[module S E]
[module R F]
{σ₁₂ : R →+* S}
{σ₂₁ : S →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
(f : F →ₛₗᵢ[σ₁₂] E)
(ᾰ : F) :
↑(⇑(f.equiv_range) ᾰ) = ⇑f ᾰ
noncomputable
def
linear_isometry.equiv_range
{E : Type u_5}
{F : Type u_9}
[seminormed_add_comm_group E]
[normed_add_comm_group F]
{R : Type u_1}
{S : Type u_2}
[semiring R]
[ring S]
[module S E]
[module R F]
{σ₁₂ : R →+* S}
{σ₂₁ : S →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
(f : F →ₛₗᵢ[σ₁₂] E) :
F ≃ₛₗᵢ[σ₁₂] ↥(linear_map.range f.to_linear_map)
Reinterpret a linear_isometry as a linear_isometry_equiv to the range.
Equations
- f.equiv_range = {to_linear_equiv := linear_equiv.of_injective f.to_linear_map _, norm_map' := _}
@[simp]
theorem
linear_isometry.equiv_range_to_linear_equiv
{E : Type u_5}
{F : Type u_9}
[seminormed_add_comm_group E]
[normed_add_comm_group F]
{R : Type u_1}
{S : Type u_2}
[semiring R]
[ring S]
[module S E]
[module R F]
{σ₁₂ : R →+* S}
{σ₂₁ : S →+* R}
[ring_hom_inv_pair σ₁₂ σ₂₁]
[ring_hom_inv_pair σ₂₁ σ₁₂]
(f : F →ₛₗᵢ[σ₁₂] E) :