(Semi-)linear isometries #
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 semi_normed_group
and we specialize to normed_group
when needed.
A σ₁₂
-semilinear isometric embedding of a normed R
-module into an R₂
-module.
Instances for linear_isometry
- linear_isometry.has_sizeof_inst
- linear_isometry.add_monoid_hom_class
- linear_isometry.has_coe_to_fun
- linear_isometry.inhabited
- linear_isometry.monoid
Equations
- linear_isometry.add_monoid_hom_class = {coe := λ (e : E →ₛₗᵢ[σ₁₂] E₂), e.to_linear_map.to_fun, coe_injective' := _, map_add := _, map_zero := _}
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}
Interpret a linear isometry as a continuous linear map.
Equations
- f.to_continuous_linear_map = {to_linear_map := f.to_linear_map, cont := _}
The identity linear isometry.
Equations
- linear_isometry.id = {to_linear_map := linear_map.id _inst_29, norm_map' := _}
Equations
- linear_isometry.inhabited = {default := linear_isometry.id _inst_29}
Composition of linear isometries.
Equations
- g.comp f = {to_linear_map := g.to_linear_map.comp f.to_linear_map, norm_map' := _}
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' := _}
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' := _}
submodule.subtype
as a continuous_linear_map
.
Equations
A semilinear isometric equivalence between two normed vector spaces.
Instances for linear_isometry_equiv
Equations
- linear_isometry_equiv.add_monoid_hom_class = {coe := λ (e : E ≃ₛₗᵢ[σ₁₂] E₂), e.to_linear_equiv.to_fun, coe_injective' := _, map_add := _, map_zero := _}
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}
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' := _}
Reinterpret a linear_isometry_equiv
as a linear_isometry
.
Equations
- e.to_linear_isometry = {to_linear_map := ↑(e.to_linear_equiv), norm_map' := _}
Reinterpret a linear_isometry_equiv
as an isometric
.
Equations
- e.to_isometric = {to_equiv := e.to_linear_equiv.to_equiv, isometry_to_fun := _}
Reinterpret a linear_isometry_equiv
as an homeomorph
.
Equations
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 := _}
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' := _}
Equations
- linear_isometry_equiv.inhabited = {default := linear_isometry_equiv.refl R E _inst_29}
The inverse linear_isometry_equiv
.
Equations
- e.symm = {to_linear_equiv := e.to_linear_equiv.symm, norm_map' := _}
Composition of linear_isometry_equiv
s as a linear_isometry_equiv
.
Equations
- e.trans e' = {to_linear_equiv := e.to_linear_equiv.trans e'.to_linear_equiv, norm_map' := _}
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 := _}
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
.
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 := _}}
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 _ hfr).to_fun, map_add' := _, map_smul' := _, inv_fun := (linear_equiv.of_bijective f.to_linear_map _ hfr).inv_fun, left_inv := _, right_inv := _}, norm_map' := _}
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' := _}
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' := _}
Two linear isometries are equal if they are equal on basis vectors.
Two linear isometric equivalences are equal if they are equal on basis vectors.