Documentation

TauCeti.LinearAlgebra.BilinearForm.Isometry.OrthogonalExtension

Extending isometries of a nondegenerate subspace by the identity #

Let ι : W → V be an isometric embedding of a finite-dimensional bilinear space (W, B') into a bilinear space (V, B), and suppose that B' is nondegenerate. Then V is the orthogonal sum of the image of ι and its orthogonal complement. The projection onto the first summand, read in W, is ι.orthogonalProjection: the vector π v is characterized by B' (π v) w = B v (ι w) for every w.

If moreover B is symmetric, every isometry g of B' extends to the isometry v ↦ v + ι (g (π v) - π v) of B, which acts as g on the image of ι and as the identity on its orthogonal complement. The extensions form an injective group homomorphism ι.isometryGroupExtend : Aut(W, B') →* Aut(V, B).

For an integral lattice this is how isometries of a sublattice spanning a nondegenerate rational subspace become rational isometries of the whole lattice; a congruence condition then makes them preserve the lattice itself.

Main definitions #

Main results #

The orthogonal projection #

source
noncomputable def LinearMap.BilinForm.Isometry.orthogonalProjection {K : Type u_1} {V : Type u_2} {W : Type u_3} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W] [FiniteDimensional K W] {B : LinearMap.BilinForm K V} {B' : LinearMap.BilinForm K W} (ι : B' →bᵢ B) (hB' : B'.Nondegenerate) :
V →ₗ[K] W

The orthogonal projection onto the image of an isometric embedding ι of a nondegenerate finite-dimensional bilinear space, read in the source: π v is the unique vector with B' (π v) w = B v (ι w) for every w.

Instances For
    source
    @[simp]
    theorem LinearMap.BilinForm.Isometry.apply_orthogonalProjection {K : Type u_1} {V : Type u_2} {W : Type u_3} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W] [FiniteDimensional K W] {B : LinearMap.BilinForm K V} {B' : LinearMap.BilinForm K W} (ι : B' →bᵢ B) (hB' : B'.Nondegenerate) (v : V) (w : W) :
    (B' ((ι.orthogonalProjection hB') v)) w = (B v) (ι w)

    The defining property of the orthogonal projection.

    source
    theorem LinearMap.BilinForm.Isometry.eq_orthogonalProjection_iff {K : Type u_1} {V : Type u_2} {W : Type u_3} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W] [FiniteDimensional K W] {B : LinearMap.BilinForm K V} {B' : LinearMap.BilinForm K W} (ι : B' →bᵢ B) (hB' : B'.Nondegenerate) (v : V) (x : W) :
    x = (ι.orthogonalProjection hB') v ↔ ∀ (w : W), (B' x) w = (B v) (ι w)

    The orthogonal projection is the unique map with its defining property.

    source
    @[simp]
    theorem LinearMap.BilinForm.Isometry.orthogonalProjection_apply_left {K : Type u_1} {V : Type u_2} {W : Type u_3} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W] [FiniteDimensional K W] {B : LinearMap.BilinForm K V} {B' : LinearMap.BilinForm K W} (ι : B' →bᵢ B) (hB' : B'.Nondegenerate) (w : W) :
    (ι.orthogonalProjection hB') (ι w) = w

    The orthogonal projection is a left inverse of the embedding.

    source
    theorem LinearMap.BilinForm.Isometry.orthogonalProjection_eq_zero_iff {K : Type u_1} {V : Type u_2} {W : Type u_3} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W] [FiniteDimensional K W] {B : LinearMap.BilinForm K V} {B' : LinearMap.BilinForm K W} (ι : B' →bᵢ B) (hB' : B'.Nondegenerate) (v : V) :
    (ι.orthogonalProjection hB') v = 0 ↔ ∀ (w : W), (B v) (ι w) = 0

    The orthogonal projection vanishes exactly on the orthogonal complement of the image.

    The extension #

    source
    noncomputable def LinearMap.BilinForm.Isometry.isometryGroupExtend {K : Type u_1} {V : Type u_2} {W : Type u_3} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W] [FiniteDimensional K W] {B : LinearMap.BilinForm K V} {B' : LinearMap.BilinForm K W} (ι : B' →bᵢ B) (hB : B.IsSymm) (hB' : B'.Nondegenerate) :
    ↥B'.isometryGroup →* ↥B.isometryGroup

    Extension of isometries by the identity. For an isometric embedding ι of a nondegenerate finite-dimensional bilinear space (W, B') into a symmetric bilinear space (V, B), the isometry g of B' extends to the isometry of B acting as g on the image of ι and as the identity on its orthogonal complement.

    Instances For
      source
      theorem LinearMap.BilinForm.Isometry.isometryGroupExtend_apply {K : Type u_1} {V : Type u_2} {W : Type u_3} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W] [FiniteDimensional K W] {B : LinearMap.BilinForm K V} {B' : LinearMap.BilinForm K W} (ι : B' →bᵢ B) (hB : B.IsSymm) (hB' : B'.Nondegenerate) (g : ↥B'.isometryGroup) (v : V) :
      ↑((ι.isometryGroupExtend hB hB') g) v = v + ι (↑g ((ι.orthogonalProjection hB') v) - (ι.orthogonalProjection hB') v)

      The extension acts by v ↦ v + ι (g (π v) - π v).

      source
      @[simp]
      theorem LinearMap.BilinForm.Isometry.isometryGroupExtend_apply_left {K : Type u_1} {V : Type u_2} {W : Type u_3} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W] [FiniteDimensional K W] {B : LinearMap.BilinForm K V} {B' : LinearMap.BilinForm K W} (ι : B' →bᵢ B) (hB : B.IsSymm) (hB' : B'.Nondegenerate) (g : ↥B'.isometryGroup) (w : W) :
      ↑((ι.isometryGroupExtend hB hB') g) (ι w) = ι (↑g w)

      On the image of ι, the extension of g acts as g.

      source
      theorem LinearMap.BilinForm.Isometry.isometryGroupExtend_apply_of_forall_eq_zero {K : Type u_1} {V : Type u_2} {W : Type u_3} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W] [FiniteDimensional K W] {B : LinearMap.BilinForm K V} {B' : LinearMap.BilinForm K W} (ι : B' →bᵢ B) (hB : B.IsSymm) (hB' : B'.Nondegenerate) (g : ↥B'.isometryGroup) {v : V} (hv : ∀ (w : W), (B v) (ι w) = 0) :
      ↑((ι.isometryGroupExtend hB hB') g) v = v

      On the orthogonal complement of the image of ι, the extension of g is the identity.

      source
      theorem LinearMap.BilinForm.Isometry.isometryGroupExtend_injective {K : Type u_1} {V : Type u_2} {W : Type u_3} [Field K] [AddCommGroup V] [Module K V] [AddCommGroup W] [Module K W] [FiniteDimensional K W] {B : LinearMap.BilinForm K V} {B' : LinearMap.BilinForm K W} (ι : B' →bᵢ B) (hB : B.IsSymm) (hB' : B'.Nondegenerate) :
      Function.Injective ⇑(ι.isometryGroupExtend hB hB')

      Distinct isometries of B' have distinct extensions.