The isometry group of a bilinear form

An endomorphism f of a module M is an isometry of a bilinear form B when B (f x) (f y) = B x y. Starting from the predicate TauCeti.BilinForm.IsIsometry defined in the dependency-light module TauCeti.LinearAlgebra.BilinearForm.Isometry.Basic, this file builds the group it cuts out inside the linear automorphisms of M, TauCeti.BilinForm.isometryGroup B, together with the API a consumer of the group needs: a Gram-matrix criterion, the resulting constraint (det f) ^ 2 = 1, functoriality in the module and in the base ring, and stability of orthogonal complements.

Mathlib bundles the same notion twice — as a map, B₁ →bᵢ B₂, and as an equivalence, LinearMap.BilinForm.IsometryEquiv B₁ B₂. The bridge to the former (TauCeti.BilinForm.IsIsometry.toIsometry, TauCeti.BilinForm.isIsometry_toLinearMap) lives with the predicate; the bridge to the latter is TauCeti.BilinForm.isometryGroupEquivIsometryEquiv here, an equivalence of types between the subgroup and B.IsometryEquiv B. What is new is the unbundled predicate, which is what lets "preserves B" be a side condition on an endomorphism one already has — the hypothesis of the automatic-invertibility theorem below, and the membership condition of a subgroup — and the group structure, needed as soon as one wants subgroups of it, group homomorphisms into it, or a group action, none of which a bare type of bundled equivalences provides.

Two statements are worth singling out.

• Over an integral domain, isometries of a left-separating form on a finite free module are automatically invertible, so they already form elements of the group (TauCeti.BilinForm.IsIsometry.toIsometryGroup, TauCeti.BilinForm.IsIsometry.bijective): preserving B forces (det f) ^ 2 = 1, so det f is a unit. For a ℤ-lattice this says that a form-preserving endomorphism of the lattice already lies in the arithmetic group Aut(V, Q), which is how such an automorphism usually presents itself — as an integer matrix satisfying Aᵀ * G * A = G.
• Base change along an algebra R → A is a group homomorphism Aut(M, B) →* Aut(A ⊗[R] M, B_A) (TauCeti.BilinForm.isometryGroupBaseChange). For R = ℤ and A = ℂ this is the action of Aut(V, Q) on the complexification of the lattice. When Q is preserved by monodromy, the monodromy of a variation of Hodge structure acts through this map.

Main definitions

• TauCeti.BilinForm.isometryGroup: the isometry group Aut(M, B) ≤ M ≃ₗ[R] M.
• TauCeti.BilinForm.isometryGroupEquivIsometryEquiv: the isometry group as a type, equivalent to Mathlib's self-isometries B.IsometryEquiv B.
• Module.Basis.isometryEquivOfToMatrixEq: two bilinear forms with the same matrix in some bases are isometric.
• LinearMap.BilinForm.specialIsometryGroup: the determinant-one isometry group of B.
• LinearMap.BilinForm.isometryDet: the determinant of an isometry, as a homomorphism to Rˣ.
• TauCeti.BilinForm.IsIsometry.toIsometryGroup: an isometry of a left-separating form on a finite free module over an integral domain, as an element of the isometry group.
• TauCeti.BilinForm.isometryGroupBaseChange: base change of isometries, as a group homomorphism.
• LinearMap.BilinForm.specialIsometryGroupBaseChange: base change of determinant-one isometries.
• TauCeti.BilinForm.isometryGroupCongr: transport of the isometry group along a linear equivalence.
• LinearMap.BilinForm.specialIsometryGroupCongr: the corresponding transport of its determinant-one subgroup.

Main results

• TauCeti.BilinForm.isIsometry_iff_toMatrix: the Gram-matrix criterion Aᵀ * G * A = G.
• TauCeti.BilinForm.IsIsometry.det_sq_eq_one: (det f) ^ 2 = 1 for an isometry of a form whose Gram determinant is a non-zero-divisor.
• TauCeti.BilinForm.IsIsometry.bijective: over an integral domain, an isometry of a left-separating form on a finite free module is bijective.
• TauCeti.BilinForm.IsIsometry.map_orthogonal: a surjective isometry carries B-orthogonal complements to B-orthogonal complements.

Implementation notes

The API is laid out by hypothesis strength: the imported predicate and elementary bridge to Mathlib, the group, transport along a linear equivalence, the Gram-matrix criterion, and base change need only a CommSemiring and additive monoids, which is where every Mathlib ingredient they consume is stated; injectivity needs subtraction in M; the determinant results need M to be an additive group over a CommRing; the automatic invertibility of an isometry of a left-separating form needs an integral domain and a finite free module.

This is the bilinear-form counterpart of TauCeti.QuadraticMap.orthogonalGroup in TauCeti/LinearAlgebra/QuadraticForm/OrthogonalGroup/Basic.lean, whose API it follows; for a quadratic form Q over a ring in which 2 is a regular scalar the orthogonal group of Q is the isometry group of Q.polarBilin, TauCeti.QuadraticMap.orthogonalGroup_eq_isometryGroup_polarBilin.

theorem TauCeti.BilinForm.IsIsometry.restrict {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {f : M →ₗ[R] M} {N : Submodule R M} (hf : IsIsometry B f) (hN : ∀ x ∈ N, f x ∈ N) : IsIsometry (B.restrict N) (f.restrict hN)

An isometry preserving a submodule restricts to an isometry of the restricted form.

theorem TauCeti.BilinForm.IsIsometry.map_orthogonal_le {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) (N : Submodule R M) : Submodule.map f (B.orthogonal N) ≤ B.orthogonal (Submodule.map f N)

An isometry maps the B-orthogonal complement of N into the B-orthogonal complement of the image of N.

theorem TauCeti.BilinForm.IsIsometry.map_orthogonal {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) (hsurj : Function.Surjective ⇑f) (N : Submodule R M) : Submodule.map f (B.orthogonal N) = B.orthogonal (Submodule.map f N)

A surjective isometry carries B-orthogonal complements to B-orthogonal complements.

def TauCeti.BilinForm.isometryGroup {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) : Subgroup (M ≃ₗ[R] M)

The isometry group Aut(M, B) of a bilinear form B on M: the linear automorphisms of M that preserve B.

For a finite free ℤ-module V carrying an integral form Q this is the arithmetic group Aut(V, Q); when Q is preserved by monodromy, a variation of Hodge structure has its monodromy representation land in this group and act on the complexification through TauCeti.BilinForm.isometryGroupBaseChange.

Equations

• TauCeti.BilinForm.isometryGroup B = { carrier := {e : M ≃ₗ[R] M | TauCeti.BilinForm.IsIsometry B ↑e}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

theorem TauCeti.BilinForm.mem_isometryGroup {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {e : M ≃ₗ[R] M} : e ∈ isometryGroup B ↔ IsIsometry B ↑e

Membership in the isometry group is the isometry predicate.

@[simp]

theorem TauCeti.BilinForm.mem_isometryGroup_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {e : M ≃ₗ[R] M} : e ∈ isometryGroup B ↔ ∀ (x y : M), (B (e x)) (e y) = (B x) y

def TauCeti.BilinForm.isometryGroupEquivIsometryEquiv {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) : ↥(isometryGroup B) ≃ B.IsometryEquiv B

Membership in Aut(M, B) is exactly Mathlib's notion of a self-isometry of B: the subgroup TauCeti.BilinForm.isometryGroup B and the type LinearMap.BilinForm.IsometryEquiv B B carry the same data, the subgroup adding the group structure.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.BilinForm.coe_isometryGroupEquivIsometryEquiv {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) (e : ↥(isometryGroup B)) : ⇑((isometryGroupEquivIsometryEquiv B) e) = ⇑↑e

@[simp]

theorem TauCeti.BilinForm.coe_isometryGroupEquivIsometryEquiv_symm {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (B : LinearMap.BilinForm R M) (e : B.IsometryEquiv B) : ⇑↑((isometryGroupEquivIsometryEquiv B).symm e) = ⇑e

def TauCeti.BilinForm.isometryGroupCongr {R : Type u_1} {M : Type u_2} {M' : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (B : LinearMap.BilinForm R M) (e : M ≃ₗ[R] M') : ↥(isometryGroup B) ≃* ↥(isometryGroup ((LinearMap.BilinForm.congr e) B))

Transporting a bilinear form along a linear equivalence transports its isometry group: conjugation by e : M ≃ₗ[R] M' carries Aut(M, B) onto Aut(M', B ∘ e⁻¹).

Equations

• TauCeti.BilinForm.isometryGroupCongr B e = (e.autCongr.subgroupMap (TauCeti.BilinForm.isometryGroup B)).trans (MulEquiv.subgroupCongr ⋯)

@[simp]

theorem TauCeti.BilinForm.coe_isometryGroupCongr_apply {R : Type u_1} {M : Type u_2} {M' : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (B : LinearMap.BilinForm R M) (e : M ≃ₗ[R] M') (a : ↥(isometryGroup B)) (x : M') : ↑((isometryGroupCongr B e) a) x = e (↑a (e.symm x))

@[simp]

theorem TauCeti.BilinForm.coe_isometryGroupCongr_symm_apply {R : Type u_1} {M : Type u_2} {M' : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] (B : LinearMap.BilinForm R M) (e : M ≃ₗ[R] M') (a : ↥(isometryGroup ((LinearMap.BilinForm.congr e) B))) (x : M) : ↑((isometryGroupCongr B e).symm a) x = e.symm (↑a (e x))

The Gram-matrix criterion

noncomputable def Module.Basis.isometryEquivOfToMatrixEq {R : Type u_1} {M : Type u_2} {M' : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] {B : LinearMap.BilinForm R M} {ι : Type u_4} [Fintype ι] [DecidableEq ι] {B' : LinearMap.BilinForm R M'} (v : Basis ι R M) (w : Basis ι R M') (h : (LinearMap.BilinForm.toMatrix v) B = (LinearMap.BilinForm.toMatrix w) B') : B.IsometryEquiv B'

Two bilinear forms with the same matrix in bases v and w are isometric, through the linear equivalence v.equiv w (Equiv.refl ι) carrying v to w.

Equations

• v.isometryEquivOfToMatrixEq w h = { toLinearEquiv := v.equiv w (Equiv.refl ι), map_app' := ⋯ }

@[simp]

theorem Module.Basis.toLinearEquiv_isometryEquivOfToMatrixEq {R : Type u_1} {M : Type u_2} {M' : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] {B : LinearMap.BilinForm R M} {ι : Type u_4} [Fintype ι] [DecidableEq ι] {B' : LinearMap.BilinForm R M'} (v : Basis ι R M) (w : Basis ι R M') (h : (LinearMap.BilinForm.toMatrix v) B = (LinearMap.BilinForm.toMatrix w) B') : (v.isometryEquivOfToMatrixEq w h).toLinearEquiv = v.equiv w (Equiv.refl ι)

@[simp]

theorem Module.Basis.isometryEquivOfToMatrixEq_apply {R : Type u_1} {M : Type u_2} {M' : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] {B : LinearMap.BilinForm R M} {ι : Type u_4} [Fintype ι] [DecidableEq ι] {B' : LinearMap.BilinForm R M'} (v : Basis ι R M) (w : Basis ι R M') (h : (LinearMap.BilinForm.toMatrix v) B = (LinearMap.BilinForm.toMatrix w) B') (x : M) : (v.isometryEquivOfToMatrixEq w h) x = (v.equiv w (Equiv.refl ι)) x

theorem Module.Basis.isometryEquivOfToMatrixEq_apply_basis {R : Type u_1} {M : Type u_2} {M' : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid M'] [Module R M'] {B : LinearMap.BilinForm R M} {ι : Type u_4} [Fintype ι] [DecidableEq ι] {B' : LinearMap.BilinForm R M'} (v : Basis ι R M) (w : Basis ι R M') (h : (LinearMap.BilinForm.toMatrix v) B = (LinearMap.BilinForm.toMatrix w) B') (i : ι) : (v.isometryEquivOfToMatrixEq w h) (v i) = w i

The isometry attached to an equality of matrices carries the basis v to the basis w.

theorem TauCeti.BilinForm.isIsometry_iff_toMatrix {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {f : M →ₗ[R] M} {ι : Type u_4} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι R M) : IsIsometry B f ↔ ((LinearMap.toMatrix b b) f).transpose * (LinearMap.BilinForm.toMatrix b) B * (LinearMap.toMatrix b b) f = (LinearMap.BilinForm.toMatrix b) B

An endomorphism is an isometry of B exactly when its matrix A in a basis b satisfies Aᵀ * G * A = G for the Gram matrix G of B in b.

Base change

theorem TauCeti.BilinForm.IsIsometry.baseChange {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {B : LinearMap.BilinForm R M} {f : M →ₗ[R] M} (A : Type u_4) [CommSemiring A] [Algebra R A] (hf : IsIsometry B f) : IsIsometry (LinearMap.BilinForm.baseChange A B) (LinearMap.baseChange A f)

Base change along an R-algebra A carries an isometry of B to an isometry of the base-changed form.

def TauCeti.BilinForm.isometryGroupBaseChange {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (A : Type u_4) [CommSemiring A] [Algebra R A] (B : LinearMap.BilinForm R M) : ↥(isometryGroup B) →* ↥(isometryGroup (LinearMap.BilinForm.baseChange A B))

Base change along an R-algebra A is a group homomorphism Aut(M, B) →* Aut(A ⊗[R] M, B_A). For R = ℤ and A = ℂ this is the action of the arithmetic group Aut(V, Q) on the complexification of the lattice, through which monodromy acts when it preserves Q.

Equations

• TauCeti.BilinForm.isometryGroupBaseChange A B = { toFun := fun (e : ↥(TauCeti.BilinForm.isometryGroup B)) => ⟨LinearEquiv.baseChange R A M M ↑e, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.BilinForm.coe_isometryGroupBaseChange {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (A : Type u_4) [CommSemiring A] [Algebra R A] (B : LinearMap.BilinForm R M) (e : ↥(isometryGroup B)) : ↑((isometryGroupBaseChange A B) e) = LinearEquiv.baseChange R A M M ↑e

theorem TauCeti.BilinForm.IsIsometry.injective {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {f : M →ₗ[R] M} (hB : LinearMap.SeparatingLeft B) (hf : IsIsometry B f) : Function.Injective ⇑f

An isometry of a left-separating form is injective: it cannot collapse a vector that pairs nontrivially with something.

Determinants

theorem TauCeti.BilinForm.IsIsometry.det_sq_mul_det_toMatrix_self {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {f : M →ₗ[R] M} {ι : Type u_3} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι R M) (hf : IsIsometry B f) : LinearMap.det f ^ 2 * ((LinearMap.BilinForm.toMatrix b) B).det = ((LinearMap.BilinForm.toMatrix b) B).det

For an isometry f of B, the Gram determinant det G of B in any basis satisfies (det f) ^ 2 * det G = det G.

theorem TauCeti.BilinForm.IsIsometry.det_sq_eq_one {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {f : M →ₗ[R] M} {ι : Type u_3} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι R M) (hG : ((LinearMap.BilinForm.toMatrix b) B).det ∈ nonZeroDivisors R) (hf : IsIsometry B f) : LinearMap.det f ^ 2 = 1

An isometry of a bilinear form whose Gram determinant is a non-zero-divisor has determinant squaring to 1; over ℤ this says its determinant is ±1.

theorem TauCeti.BilinForm.IsIsometry.isUnit_det {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {f : M →ₗ[R] M} {ι : Type u_3} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι R M) (hG : ((LinearMap.BilinForm.toMatrix b) B).det ∈ nonZeroDivisors R) (hf : IsIsometry B f) : IsUnit (LinearMap.det f)

An isometry of a bilinear form whose Gram determinant is a non-zero-divisor has unit determinant, its square being 1.

noncomputable def TauCeti.BilinForm.IsIsometry.toIsometryGroupOfIsUnitDet {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {f : M →ₗ[R] M} [Module.Free R M] [Module.Finite R M] (hf : IsIsometry B f) (hdet : IsUnit (LinearMap.det f)) : ↥(isometryGroup B)

An isometry whose underlying endomorphism has unit determinant, as an element of the isometry group.

Equations

• hf.toIsometryGroupOfIsUnitDet hdet = ⟨LinearMap.equivOfIsUnitDet hdet, ⋯⟩

@[simp]

theorem TauCeti.BilinForm.IsIsometry.coe_toIsometryGroupOfIsUnitDet {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {f : M →ₗ[R] M} [Module.Free R M] [Module.Finite R M] (hf : IsIsometry B f) (hdet : IsUnit (LinearMap.det f)) : ↑↑(hf.toIsometryGroupOfIsUnitDet hdet) = f

@[simp]

theorem TauCeti.BilinForm.IsIsometry.toIsometryGroupOfIsUnitDet_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {f : M →ₗ[R] M} [Module.Free R M] [Module.Finite R M] (hf : IsIsometry B f) (hdet : IsUnit (LinearMap.det f)) (x : M) : ↑(hf.toIsometryGroupOfIsUnitDet hdet) x = f x

theorem TauCeti.BilinForm.IsIsometry.isUnit_det_of_separatingLeft {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {f : M →ₗ[R] M} [IsDomain R] [Module.Free R M] [Module.Finite R M] (hB : LinearMap.SeparatingLeft B) (hf : IsIsometry B f) : IsUnit (LinearMap.det f)

An isometry of a left-separating form on a finite free module over an integral domain has unit determinant.

noncomputable def TauCeti.BilinForm.IsIsometry.toIsometryGroup {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {f : M →ₗ[R] M} [IsDomain R] [Module.Free R M] [Module.Finite R M] (hB : LinearMap.SeparatingLeft B) (hf : IsIsometry B f) : ↥(isometryGroup B)

Over an integral domain, an endomorphism of a finite free module preserving a left-separating bilinear form is automatically invertible, hence an element of the isometry group. This is how an element of Aut(V, Q) usually presents itself: as an endomorphism of the lattice V preserving Q, with invertibility a consequence rather than a hypothesis.

Equations

• TauCeti.BilinForm.IsIsometry.toIsometryGroup hB hf = hf.toIsometryGroupOfIsUnitDet ⋯

@[simp]

theorem TauCeti.BilinForm.IsIsometry.coe_toIsometryGroup {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {f : M →ₗ[R] M} [IsDomain R] [Module.Free R M] [Module.Finite R M] (hB : LinearMap.SeparatingLeft B) (hf : IsIsometry B f) : ↑↑(toIsometryGroup hB hf) = f

@[simp]

theorem TauCeti.BilinForm.IsIsometry.toIsometryGroup_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {f : M →ₗ[R] M} [IsDomain R] [Module.Free R M] [Module.Finite R M] (hB : LinearMap.SeparatingLeft B) (hf : IsIsometry B f) (x : M) : ↑(toIsometryGroup hB hf) x = f x

theorem TauCeti.BilinForm.IsIsometry.bijective {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {f : M →ₗ[R] M} [IsDomain R] [Module.Free R M] [Module.Finite R M] (hB : LinearMap.SeparatingLeft B) (hf : IsIsometry B f) : Function.Bijective ⇑f

Over an integral domain, an endomorphism of a finite free module preserving a left-separating bilinear form is automatically bijective.

The determinant-one isometry group

These declarations live in Mathlib's LinearMap.BilinForm namespace so that dot notation such as B.specialIsometryGroup works on a bilinear form B.

noncomputable def LinearMap.BilinForm.specialIsometryGroup {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) : Subgroup (M ≃ₗ[R] M)

The determinant-one isometry group of a bilinear form.

The determinant is Mathlib's LinearEquiv.det, which is 1 by convention on a module that is not finite free; on such a module this subgroup is therefore all of isometryGroup B.

Equations

• B.specialIsometryGroup = TauCeti.BilinForm.isometryGroup B ⊓ LinearEquiv.det.ker

@[simp]

theorem LinearMap.BilinForm.mem_specialIsometryGroup_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {e : M ≃ₗ[R] M} : e ∈ B.specialIsometryGroup ↔ e ∈ TauCeti.BilinForm.isometryGroup B ∧ LinearEquiv.det e = 1

theorem LinearMap.BilinForm.specialIsometryGroup_le_isometryGroup {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) : B.specialIsometryGroup ≤ TauCeti.BilinForm.isometryGroup B

Every determinant-one isometry is an isometry.

instance LinearMap.BilinForm.specialIsometryGroup_normal {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) : (B.specialIsometryGroup.subgroupOf (TauCeti.BilinForm.isometryGroup B)).Normal

The determinant-one isometry group is normal in the full isometry group.

noncomputable def LinearMap.BilinForm.isometryDet {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) : ↥(TauCeti.BilinForm.isometryGroup B) →* Rˣ

The determinant of an isometry, as a homomorphism to the units of the base ring.

Equations

• B.isometryDet = LinearEquiv.det.comp (TauCeti.BilinForm.isometryGroup B).subtype

@[simp]

theorem LinearMap.BilinForm.isometryDet_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} (g : ↥(TauCeti.BilinForm.isometryGroup B)) : B.isometryDet g = LinearEquiv.det ↑g

noncomputable def LinearMap.BilinForm.specialIsometryWithin {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) : Subgroup ↥(TauCeti.BilinForm.isometryGroup B)

The determinant-one subgroup regarded as a subgroup of the full isometry group.

Equations

• B.specialIsometryWithin = B.isometryDet.ker

@[simp]

theorem LinearMap.BilinForm.mem_specialIsometryWithin_iff {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} {g : ↥(TauCeti.BilinForm.isometryGroup B)} : g ∈ B.specialIsometryWithin ↔ LinearEquiv.det ↑g = 1

theorem LinearMap.BilinForm.specialIsometryWithin_eq_subgroupOf {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} : B.specialIsometryWithin = B.specialIsometryGroup.subgroupOf (TauCeti.BilinForm.isometryGroup B)

The two ambient-group presentations of the determinant-one isometry group agree.

noncomputable def LinearMap.BilinForm.specialIsometryToIsometry {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) : ↥B.specialIsometryGroup →* ↥(TauCeti.BilinForm.isometryGroup B)

The inclusion from determinant-one isometries to all isometries.

Equations

• B.specialIsometryToIsometry = Subgroup.inclusion ⋯

@[simp]

theorem LinearMap.BilinForm.coe_specialIsometryToIsometry {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} (g : ↥B.specialIsometryGroup) : ↑(B.specialIsometryToIsometry g) = ↑g

@[simp]

theorem LinearMap.BilinForm.det_coe_specialIsometryGroup {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} (g : ↥B.specialIsometryGroup) : LinearEquiv.det ↑g = 1

The determinant of a determinant-one isometry is one.

theorem LinearMap.BilinForm.specialIsometryToIsometry_injective {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} : Function.Injective ⇑B.specialIsometryToIsometry

Inclusion of determinant-one isometries into all isometries is injective.

@[simp]

theorem LinearMap.BilinForm.range_specialIsometryToIsometry {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} : B.specialIsometryToIsometry.range = B.specialIsometryWithin

The image of the determinant-one isometry group in the full isometry group is the determinant kernel.

noncomputable def LinearMap.BilinForm.specialIsometryWithinEquiv {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (B : LinearMap.BilinForm R M) : ↥B.specialIsometryWithin ≃* ↥B.specialIsometryGroup

The determinant kernel inside the isometry group is canonically isomorphic to the determinant-one subgroup of the ambient linear automorphism group.

Equations

• B.specialIsometryWithinEquiv = (MulEquiv.subgroupCongr ⋯).trans (Subgroup.subgroupOfEquivOfLe ⋯)

@[simp]

theorem LinearMap.BilinForm.coe_specialIsometryWithinEquiv_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} (g : ↥B.specialIsometryWithin) : ↑(B.specialIsometryWithinEquiv g) = ↑↑g

@[simp]

theorem LinearMap.BilinForm.coe_specialIsometryWithinEquiv_symm_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} (g : ↥B.specialIsometryGroup) : ↑(B.specialIsometryWithinEquiv.symm g) = B.specialIsometryToIsometry g

theorem LinearMap.BilinForm.specialIsometryWithin_eq_top {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {B : LinearMap.BilinForm R M} [Subsingleton M] : B.specialIsometryWithin = ⊤

On a subsingleton module every isometry has determinant one.

noncomputable def LinearMap.BilinForm.specialIsometryGroupCongr {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {M' : Type u_3} [AddCommGroup M'] [Module R M'] (B : LinearMap.BilinForm R M) (e : M ≃ₗ[R] M') : ↥B.specialIsometryGroup ≃* ↥((congr e) B).specialIsometryGroup

Transporting a bilinear form along a linear equivalence transports its determinant-one isometry group.

Equations

• B.specialIsometryGroupCongr e = (e.autCongr.subgroupMap B.specialIsometryGroup).trans (MulEquiv.subgroupCongr ⋯)

@[simp]

theorem LinearMap.BilinForm.coe_specialIsometryGroupCongr_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {M' : Type u_3} [AddCommGroup M'] [Module R M'] (B : LinearMap.BilinForm R M) (e : M ≃ₗ[R] M') (g : ↥B.specialIsometryGroup) : ↑((B.specialIsometryGroupCongr e) g) = e.symm ≪≫ₗ ↑g ≪≫ₗ e

@[simp]

theorem LinearMap.BilinForm.coe_specialIsometryGroupCongr_symm_apply {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {M' : Type u_3} [AddCommGroup M'] [Module R M'] (B : LinearMap.BilinForm R M) (e : M ≃ₗ[R] M') (g : ↥((congr e) B).specialIsometryGroup) : ↑((B.specialIsometryGroupCongr e).symm g) = e ≪≫ₗ ↑g ≪≫ₗ e.symm

noncomputable def LinearMap.BilinForm.specialIsometryGroupBaseChange {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (A : Type u_3) [CommRing A] [Algebra R A] [Module.Free R M] [Module.Finite R M] (B : LinearMap.BilinForm R M) : ↥B.specialIsometryGroup →* ↥(BilinForm.baseChange A B).specialIsometryGroup

Base change preserves determinant-one isometries.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LinearMap.BilinForm.coe_specialIsometryGroupBaseChange {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (A : Type u_3) [CommRing A] [Algebra R A] [Module.Free R M] [Module.Finite R M] (B : LinearMap.BilinForm R M) (g : ↥B.specialIsometryGroup) : ↑((specialIsometryGroupBaseChange A B) g) = LinearEquiv.baseChange R A M M ↑g