Isometric endomorphisms of a bilinear form

This file defines the predicate that an endomorphism preserves a bilinear form and provides its elementary API, including the bridge to Mathlib's bundled isometric maps. The isometry group and the determinant, base-change, and orthogonal-complement API are developed in TauCeti.LinearAlgebra.BilinearForm.Isometry.

def TauCeti.BilinForm.IsIsometry {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) (f : M →ₗ[R] M) : Prop

An endomorphism f of M is an isometry of the bilinear form B when it preserves B, that is, when B (f x) (f y) = B x y for all x and y.

Isometric endomorphisms form a monoid, not a group: for the zero form on ℤ ^ 2 every endomorphism is one. For a finite free ℤ-module V and a left-separating integral form Q an isometric endomorphism is automatically invertible (TauCeti.BilinForm.IsIsometry.toIsometryGroup), and the resulting automorphisms are the arithmetic group Aut(V, Q); see TauCeti.BilinForm.isometryGroup.

Equations

• TauCeti.BilinForm.IsIsometry B f = ∀ (x y : M), (B (f x)) (f y) = (B x) y

theorem TauCeti.BilinForm.isIsometry_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {f : M →ₗ[R] M} : IsIsometry B f ↔ ∀ (x y : M), (B (f x)) (f y) = (B x) y

An endomorphism is an isometry of B exactly when it preserves B pointwise.

theorem TauCeti.BilinForm.isIsometry_iff_comp {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {f : M →ₗ[R] M} : IsIsometry B f ↔ B.comp f f = B

An endomorphism is an isometry of B exactly when precomposing B with it on both sides returns B.

theorem TauCeti.BilinForm.isIsometry_toLinearMap {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} (φ : B →bᵢ B) : IsIsometry B φ.toLinearMap

The underlying map of one of Mathlib's isometric maps B →bᵢ B is an isometry.

theorem TauCeti.BilinForm.IsIsometry.apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {f : M →ₗ[R] M} (hf : IsIsometry B f) (x y : M) : (B (f x)) (f y) = (B x) y

An isometry takes the same value under B after applying the endomorphism to both inputs.

def TauCeti.BilinForm.IsIsometry.toIsometry {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {f : M →ₗ[R] M} (hf : IsIsometry B f) : B →bᵢ B

An isometry, bundled as one of Mathlib's isometric maps B →bᵢ B.

Equations

• hf.toIsometry = { toLinearMap := f, map_app' := hf }

@[simp]

theorem TauCeti.BilinForm.IsIsometry.toIsometry_apply {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {f : M →ₗ[R] M} (hf : IsIsometry B f) (x : M) : hf.toIsometry x = f x

@[simp]

theorem TauCeti.BilinForm.IsIsometry.toIsometry_toLinearMap {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {f : M →ₗ[R] M} (hf : IsIsometry B f) : hf.toIsometry.toLinearMap = f

theorem TauCeti.BilinForm.IsIsometry.id {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} : IsIsometry B LinearMap.id

theorem TauCeti.BilinForm.IsIsometry.comp {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {f g : M →ₗ[R] M} (hf : IsIsometry B f) (hg : IsIsometry B g) : IsIsometry B (f ∘ₗ g)