The orthogonal group of a quadratic form

Mathlib knows the orthogonal group only in matrix form: Matrix.orthogonalGroup n R is the group of matrices A with Aᵀ * A = 1 (Matrix.mem_orthogonalGroup_iff'). Such matrices preserve the standard form x ↦ ∑ i, x i ^ 2 on n → R, and, as soon as 2 is not a zero divisor in R, they are exactly its isometries: evaluating Q (A x) = Q x at the basis vectors and their pairwise sums says that Aᵀ * A has unit diagonal and that twice each off-diagonal entry vanishes. In characteristic two the two notions part company, since there the standard form no longer sees the off-diagonal entries at all. For an abstract quadratic map Q : QuadraticMap R M N the corresponding group is missing, even though Mathlib does have the individual isometries as QuadraticMap.IsometryEquiv Q Q: what it lacks is the observation that they form a subgroup of the linear automorphism group M ≃ₗ[R] M, and hence a group to act with.

This file supplies that subgroup, together with its determinant-one subgroup and the reflections in vectors of invertible norm, which fix the kernel of polar Q v (the hyperplane v ^ ⊥ when 2 is invertible). The orthogonal group is the target of the twisted-conjugation homomorphism out of the Pin group, so it is the object the Pin/Spin double covers are stated against, and the reflections are the generators into which the Cartan-Dieudonné theorem TauCeti.QuadraticMap.exists_reflectionOrthogonal_list_prod_eq factors an orthogonal automorphism. The structural declarations and reflections defined using an invertible norm hold over an arbitrary commutative ring. The coefficient-spelling lemmas assume a field, and the second spelling also requires 2 ≠ 0. The equal-norm dichotomy, Witt transitivity and the fixed-subspace correction assume a field in which 2 is nonzero. The characteristic restriction is not incidental: in characteristic two polar Q v v = 2 • Q v vanishes, so v lies in the kernel of polar Q v, reflection Q v fixes v, and it is not a reflection in a complement of v. Over a field it is a transvection when polar Q v ≠ 0 and the identity when polar Q v = 0; over a general ring it can be the identity in other cases too.

Main definitions

• TauCeti.QuadraticMap.orthogonalGroup Q: the Q-preserving linear automorphisms of M, as a subgroup of M ≃ₗ[R] M.
• TauCeti.QuadraticMap.specialOrthogonalGroup Q: its determinant-one subgroup.
• QuadraticMap.orthogonalDet Q: the determinant O(Q) →* Rˣ.
• QuadraticMap.specialOrthogonalWithin Q: its kernel, the determinant-one subgroup regarded as a subgroup of orthogonalGroup Q rather than of M ≃ₗ[R] M, with QuadraticMap.specialOrthogonalToOrthogonal Q : SO(Q) →* O(Q) and QuadraticMap.specialOrthogonalWithinEquiv Q relating the two spellings.
• QuadraticMap.specialOrthogonalToGeneralLinear Q: the faithful coordinate inclusion of a special orthogonal group into matrix GL.
• QuadraticMap.orthogonalToGeneralLinear Q: the corresponding faithful coordinate inclusion of the full orthogonal group into matrix GL.
• TauCeti.QuadraticMap.reflection Q v: the reflection in a vector v with Q v invertible, built from Mathlib's Module.reflection; it is the reflection in the hyperplane v ^ ⊥ when 2 is invertible.
• TauCeti.QuadraticMap.reflectionOrthogonal Q v: the same reflection bundled as an element of orthogonalGroup Q, so that statements about products of reflections and about the ranges of the Pin and Spin actions can name it. TauCeti.QuadraticMap.reflectionOrthogonal_mul_self and TauCeti.QuadraticMap.reflectionOrthogonal_inv are its group-level involution facts.
• QuadraticMap.negOrthogonal Q: the isometry x ↦ -x, as an element of orthogonalGroup Q.

Main results

• TauCeti.QuadraticMap.polar_apply_of_mem_orthogonalGroup: an orthogonal automorphism preserves polarization and the orthogonality relation (isOrtho_iff_of_mem_orthogonalGroup). As soon as 2 acts injectively on the target the converse holds, TauCeti.QuadraticMap.mem_orthogonalGroup_iff_polar, which is the usual identification of the isometries of a quadratic form with the isometries of its polar bilinear form. At the level of groups this is TauCeti.QuadraticMap.orthogonalGroup_eq_isometryGroup_polarBilin: O(Q) is the isometry group TauCeti.BilinForm.isometryGroup of Q.polarBilin, so the bilinear-form API applies to it. Its determinant-one counterpart is TauCeti.QuadraticMap.specialOrthogonalGroupEquivSpecialIsometryGroupPolarBilin.
• TauCeti.QuadraticMap.orthogonalGroupEquivIsometryEquiv: the underlying set of the orthogonal group is Mathlib's type of self-isometries Q.IsometryEquiv Q. This is the compatibility with the Mathlib vocabulary; the point of orthogonalGroup is the group structure, which QuadraticMap.IsometryEquiv does not carry.
• QuadraticMap.IsometryEquiv.orthogonalGroupCongr: isometric quadratic maps have isomorphic orthogonal groups. Over an algebraically closed field this is what makes O(Q) of a nondegenerate form depend only on the rank of Q. The transport respects identity, composition, and inverses (QuadraticMap.IsometryEquiv.orthogonalGroupCongr_refl, QuadraticMap.IsometryEquiv.orthogonalGroupCongr_trans, QuadraticMap.IsometryEquiv.orthogonalGroupCongr_symm) and preserves the determinant (QuadraticMap.IsometryEquiv.orthogonalDet_orthogonalGroupCongr).
• QuadraticMap.IsometryEquiv.specialOrthogonalGroupCongr: isometric quadratic maps have isomorphic special orthogonal groups as well, functorially and compatibly with the inclusion into the full orthogonal group.
• TauCeti.QuadraticMap.reflection_mem_orthogonalGroup: the reflection in a vector of invertible norm is orthogonal; TauCeti.QuadraticMap.reflection_mul_self says it is an involution, and TauCeti.QuadraticMap.reflection_apply_of_isOrtho that it fixes every vector orthogonal to v, TauCeti.QuadraticMap.reflection_smul_eq that rescaling by an invertible scalar does not change it, and TauCeti.QuadraticMap.det_reflection computes its determinant on a finite free module. These are the factors in the Cartan-Dieudonné theorem TauCeti.QuadraticMap.exists_reflectionOrthogonal_list_prod_eq (a field of characteristic not two, a nondegenerate form, finite dimension; none of that is assumed here), and the image of the Pin group's generating vectors under twisted conjugation.
• TauCeti.QuadraticMap.reflection_map and TauCeti.QuadraticMap.orthogonalGroupCongr_reflectionOrthogonal: an isometric equivalence e carries the reflection in v to the reflection in e v; inside O(Q) this is the conjugation law g τ_v g⁻¹ = τ_{g v}, TauCeti.QuadraticMap.mul_reflectionOrthogonal_mul_inv.
• QuadraticForm.polar_div_eq_two_mul_polar_div_polar: over a field with 2 ≠ 0, the reflection coefficient polar Q v x / Q v equals 2 * polar Q v x / polar Q v v, so the two spellings of the reflection in the literature (TauCeti.QuadraticMap.reflection_apply_eq_sub_div and TauCeti.QuadraticMap.reflection_apply_eq_sub_two_mul_div) are the same map.
• QuadraticMap.exists_isometryEquiv_apply_eq_of_map_eq: Witt transitivity, the orthogonal group acts transitively on the vectors of a fixed nonzero value, by reflecting in x - y or in x + y.
• TauCeti.QuadraticMap.exists_reflectionOrthogonal_list_prod_mul_eqOn_sup_span_singleton: at most two anisotropic reflections supply the one-step fixed-subspace correction used by Cartan--Dieudonne induction.
• TauCeti.QuadraticMap.specialOrthogonalGroup_normal: SO(Q) is normal in O(Q), being the kernel of the determinant restricted there.
• TauCeti.QuadraticMap.orthogonalDet_sq: if the polar form is left-separating on a finite free module over a domain, every orthogonal automorphism has determinant squaring to one.
• TauCeti.QuadraticMap.finiteIndex_specialOrthogonalWithin: under the same hypotheses, SO(Q) has finite index in O(Q).
• TauCeti.QuadraticMap.range_orthogonalDet and TauCeti.QuadraticMap.index_specialOrthogonalWithin: for a nondegenerate form on a nonzero finite-dimensional space over a field of characteristic not two, the determinant takes exactly the values ±1, so SO(Q) has index two in O(Q); on the zero space the two coincide, QuadraticMap.specialOrthogonalWithin_eq_top.
• TauCeti.QuadraticMap.range_orthogonalGroup_toLinearMap: on a finite free module over a domain, if the polar form separates points, the underlying maps of O(Q) are exactly the endomorphisms preserving Q; exists_orthogonalGroup_toLinearMap_eq gives the lift.

Implementation notes

orthogonalGroup is defined for a QuadraticMap R M N valued in an arbitrary module N, since preserving Q makes sense at that generality. The file is therefore laid out by hypothesis strength: the group itself, its identification with IsometryEquiv, and its transport along an isometric equivalence need only a CommSemiring and additive monoids; the polarization needs subtraction in M and N, since QuadraticMap.polar is stated for [AddCommGroup M] [AddCommGroup N], but still no more than a CommSemiring; the determinant needs M to be an additive group over a CommRing, and the reflections need to divide by Q v and so are stated for a QuadraticForm R M, that is, for N = R. The ReflectionField section divides by Q v over a field; its second coefficient spelling also assumes 2 ≠ 0. The fixed-subspace correction assumes a field and 2 ≠ 0; the closing Cartan--Dieudonne dichotomy assumes a field, a nonzero common quadratic value, and 2 ≠ 0. The determinant's square needs a separating polar form on a finite free module over a domain, and its range and index a nondegenerate form on a nonzero finite-dimensional space over a field in which 2 ≠ 0. The endomorphism characterization needs a separating polar form on a finite free module over a domain.

References

• J.-P. Serre, A Course in Arithmetic (1973), Chapter IV.
• H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I §2.
• E. Artin, Geometric Algebra (1957), Chapter III.
• O. T. O'Meara, Introduction to Quadratic Forms (1963), §43. The endomorphism characterization below is the algebraic observation in this section.

def TauCeti.QuadraticMap.orthogonalGroup {R : Type u} {M : Type v} {N : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (Q : QuadraticMap R M N) : Subgroup (M ≃ₗ[R] M)

The orthogonal group of a quadratic map: the linear automorphisms of M that preserve Q.

Mathlib's Matrix.orthogonalGroup n R is a coordinate version of this for the standard form on n → R: its matrices preserve x ↦ ∑ i, x i ^ 2, and are all of its isometries as soon as 2 is not a zero divisor in R. QuadraticMap.IsometryEquiv Q Q is the same underlying set as orthogonalGroup Q (see orthogonalGroupEquivIsometryEquiv) but carries no group structure.

Equations

• TauCeti.QuadraticMap.orthogonalGroup Q = { carrier := {f : M ≃ₗ[R] M | ∀ (m : M), Q (f m) = Q m}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

@[simp]

theorem TauCeti.QuadraticMap.mem_orthogonalGroup_iff {R : Type u} {M : Type v} {N : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {Q : QuadraticMap R M N} {f : M ≃ₗ[R] M} : f ∈ orthogonalGroup Q ↔ ∀ (m : M), Q (f m) = Q m

theorem TauCeti.QuadraticMap.map_app_of_mem_orthogonalGroup {R : Type u} {M : Type v} {N : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {Q : QuadraticMap R M N} {f : M ≃ₗ[R] M} (hf : f ∈ orthogonalGroup Q) (m : M) : Q (f m) = Q m

The defining property of an orthogonal automorphism, in the form in which it rewrites.

This is deliberately not a simp lemma: its left-hand side Q (f m) matches every application of every quadratic map to every linear equivalence, and discharging the side goal f ∈ orthogonalGroup Q unfolds through mem_orthogonalGroup_iff to ∀ m, Q (f m) = Q m, which this lemma applies to again. Name it explicitly in the simp calls that want it.

@[simp]

theorem TauCeti.QuadraticMap.isOrtho_iff_of_mem_orthogonalGroup {R : Type u} {M : Type v} {N : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {Q : QuadraticMap R M N} {f : M ≃ₗ[R] M} (hf : f ∈ orthogonalGroup Q) (x y : M) : Q.IsOrtho (f x) (f y) ↔ Q.IsOrtho x y

An orthogonal automorphism preserves orthogonality of vectors.

def TauCeti.QuadraticMap.orthogonalGroupEquivIsometryEquiv {R : Type u} {M : Type v} {N : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (Q : QuadraticMap R M N) : ↥(orthogonalGroup Q) ≃ Q.IsometryEquiv Q

The orthogonal group of Q, as a set, is Mathlib's type of self-isometries of Q. The content of orthogonalGroup is the group structure, which QuadraticMap.IsometryEquiv does not carry.

Equations

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

@[simp]

theorem TauCeti.QuadraticMap.coe_orthogonalGroupEquivIsometryEquiv {R : Type u} {M : Type v} {N : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (Q : QuadraticMap R M N) (f : ↥(orthogonalGroup Q)) : ⇑((orthogonalGroupEquivIsometryEquiv Q) f) = ⇑↑f

@[simp]

theorem TauCeti.QuadraticMap.coe_orthogonalGroupEquivIsometryEquiv_symm {R : Type u} {M : Type v} {N : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (Q : QuadraticMap R M N) (e : Q.IsometryEquiv Q) : ⇑↑((orthogonalGroupEquivIsometryEquiv Q).symm e) = ⇑e

@[simp]

theorem TauCeti.toLinearEquiv_orthogonalGroupEquivIsometryEquiv {R : Type u} {M : Type v} {N : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (Q : QuadraticMap R M N) (f : ↥(QuadraticMap.orthogonalGroup Q)) : ((QuadraticMap.orthogonalGroupEquivIsometryEquiv Q) f).toLinearEquiv = ↑f

def QuadraticMap.IsometryEquiv.orthogonalGroupCongr {R : Type u} {M₁ : Type u_1} {M₂ : Type u_2} {N : Type w} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid N] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (e : Q₁.IsometryEquiv Q₂) : ↥(TauCeti.QuadraticMap.orthogonalGroup Q₁) ≃* ↥(TauCeti.QuadraticMap.orthogonalGroup Q₂)

Isometric quadratic maps have isomorphic orthogonal groups: conjugation by an isometric equivalence e : Q₁.IsometryEquiv Q₂ carries O(Q₁) onto O(Q₂).

Over an algebraically closed field every nondegenerate quadratic form of a given rank is isometric to every other, so this is what makes O(Q) depend on the rank alone.

Equations

• e.orthogonalGroupCongr = (e.autCongr.subgroupMap (TauCeti.QuadraticMap.orthogonalGroup Q₁)).trans (MulEquiv.subgroupCongr ⋯)

@[simp]

theorem QuadraticMap.IsometryEquiv.coe_orthogonalGroupCongr_apply {R : Type u} {M₁ : Type u_1} {M₂ : Type u_2} {N : Type w} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid N] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (e : Q₁.IsometryEquiv Q₂) (f : ↥(TauCeti.QuadraticMap.orthogonalGroup Q₁)) (m : M₂) : ↑(e.orthogonalGroupCongr f) m = e.toLinearEquiv (↑f (e.symm m))

@[simp]

theorem QuadraticMap.IsometryEquiv.coe_orthogonalGroupCongr_symm_apply {R : Type u} {M₁ : Type u_1} {M₂ : Type u_2} {N : Type w} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid N] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (e : Q₁.IsometryEquiv Q₂) (g : ↥(TauCeti.QuadraticMap.orthogonalGroup Q₂)) (m : M₁) : ↑(e.orthogonalGroupCongr.symm g) m = e.symm (↑g (e.toLinearEquiv m))

@[simp]

theorem QuadraticMap.IsometryEquiv.orthogonalGroupCongr_refl {R : Type u} {M₁ : Type u_1} {N : Type w} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid N] [Module R N] {Q₁ : QuadraticMap R M₁ N} : (refl Q₁).orthogonalGroupCongr = MulEquiv.refl ↥(TauCeti.QuadraticMap.orthogonalGroup Q₁)

Transporting the orthogonal group along the identity isometry is the identity equivalence.

@[simp]

theorem QuadraticMap.IsometryEquiv.orthogonalGroupCongr_trans {R : Type u} {M₁ : Type u_1} {M₂ : Type u_2} {M₃ : Type u_3} {N : Type w} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid M₃] [Module R M₃] [AddCommMonoid N] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} {Q₃ : QuadraticMap R M₃ N} (e₁₂ : Q₁.IsometryEquiv Q₂) (e₂₃ : Q₂.IsometryEquiv Q₃) : (e₁₂.trans e₂₃).orthogonalGroupCongr = e₁₂.orthogonalGroupCongr.trans e₂₃.orthogonalGroupCongr

Orthogonal-group transport respects composition of isometries.

theorem QuadraticMap.IsometryEquiv.orthogonalGroupCongr_symm {R : Type u} {M₁ : Type u_1} {M₂ : Type u_2} {N : Type w} [CommSemiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid N] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (e : Q₁.IsometryEquiv Q₂) : e.orthogonalGroupCongr.symm = e.symm.orthogonalGroupCongr

Inverting orthogonal-group transport is transport along the inverse isometry.

@[simp]

theorem TauCeti.QuadraticMap.polar_apply_of_mem_orthogonalGroup {R : Type u} {M : Type v} {N : Type w} [CommSemiring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {Q : QuadraticMap R M N} {f : M ≃ₗ[R] M} (hf : f ∈ orthogonalGroup Q) (x y : M) : QuadraticMap.polar (⇑Q) (f x) (f y) = QuadraticMap.polar (⇑Q) x y

An orthogonal automorphism preserves the polarization of Q, because the polarization is built from Q and the additive structure alone.

theorem TauCeti.QuadraticMap.mem_orthogonalGroup_iff_polar {R : Type u} {M : Type v} {N : Type w} [CommSemiring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {Q : QuadraticMap R M N} (h2 : IsSMulRegular N 2) {f : M ≃ₗ[R] M} : f ∈ orthogonalGroup Q ↔ ∀ (x y : M), QuadraticMap.polar (⇑Q) (f x) (f y) = QuadraticMap.polar (⇑Q) x y

As soon as 2 acts injectively on the target, preserving the polarization is the same as preserving the quadratic map: an automorphism is orthogonal exactly when it is an isometry of the polar bilinear form.

Only injectivity is needed, not invertibility of 2, so this covers integral forms as well: over ℤ, or more generally whenever N is 2-torsion-free, 2 is not a unit but the polarization still determines Q. When 2 is invertible in R the hypothesis is (isUnit_of_invertible (2 : R)).isSMulRegular N. Some such hypothesis is needed: in characteristic two the polarization forgets Q entirely on the diagonal.

theorem TauCeti.QuadraticMap.orthogonalGroup_eq_isometryGroup_polarBilin {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (h2 : IsSMulRegular R 2) (Q : QuadraticForm R M) : orthogonalGroup Q = BilinForm.isometryGroup (QuadraticMap.polarBilin Q)

The orthogonal group of a quadratic form is the isometry group of its polar bilinear form, as soon as 2 is a regular scalar: orthogonalGroup Q and TauCeti.BilinForm.isometryGroup Q.polarBilin are then two names for the same subgroup of M ≃ₗ[R] M, and the bilinear-form API — the Gram-matrix criterion, det ^ 2 = 1, base change — applies to O(Q) through it. Some such hypothesis is needed: in characteristic two the polarization forgets Q on the diagonal.

noncomputable def TauCeti.QuadraticMap.specialOrthogonalGroup {R : Type u} {M : Type v} {N : Type w} [CommRing R] [AddCommGroup M] [Module R M] [AddCommMonoid N] [Module R N] (Q : QuadraticMap R M N) : Subgroup (M ≃ₗ[R] M)

The special orthogonal group: the orthogonal automorphisms of determinant one.

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 orthogonalGroup Q.

Equations

• TauCeti.QuadraticMap.specialOrthogonalGroup Q = TauCeti.QuadraticMap.orthogonalGroup Q ⊓ LinearEquiv.det.ker

@[simp]

theorem TauCeti.QuadraticMap.mem_specialOrthogonalGroup_iff {R : Type u} {M : Type v} {N : Type w} [CommRing R] [AddCommGroup M] [Module R M] [AddCommMonoid N] [Module R N] {Q : QuadraticMap R M N} {f : M ≃ₗ[R] M} : f ∈ specialOrthogonalGroup Q ↔ f ∈ orthogonalGroup Q ∧ LinearEquiv.det f = 1

@[simp]

theorem TauCeti.QuadraticMap.det_coe_specialOrthogonalGroup {R : Type u} {M : Type v} {N : Type w} [CommRing R] [AddCommGroup M] [Module R M] [AddCommMonoid N] [Module R N] {Q : QuadraticMap R M N} (g : ↥(specialOrthogonalGroup Q)) : LinearEquiv.det ↑g = 1

The determinant of an element of SO(Q) is one.

theorem TauCeti.QuadraticMap.specialOrthogonalGroup_le_orthogonalGroup {R : Type u} {M : Type v} {N : Type w} [CommRing R] [AddCommGroup M] [Module R M] [AddCommMonoid N] [Module R N] (Q : QuadraticMap R M N) : specialOrthogonalGroup Q ≤ orthogonalGroup Q

instance TauCeti.QuadraticMap.specialOrthogonalGroup_normal {R : Type u} {M : Type v} {N : Type w} [CommRing R] [AddCommGroup M] [Module R M] [AddCommMonoid N] [Module R N] (Q : QuadraticMap R M N) : ((specialOrthogonalGroup Q).subgroupOf (orthogonalGroup Q)).Normal

SO(Q) is normal in O(Q): inside the orthogonal group it is the kernel of the determinant.

theorem TauCeti.QuadraticMap.specialOrthogonalGroup_eq_specialIsometryGroup_polarBilin {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (h2 : IsSMulRegular R 2) : specialOrthogonalGroup Q = LinearMap.BilinForm.specialIsometryGroup (QuadraticMap.polarBilin Q)

When multiplication by two is injective, the special orthogonal group of a quadratic form is the determinant-one isometry group of its polar bilinear form. This is the determinant-one counterpart of orthogonalGroup_eq_isometryGroup_polarBilin.

noncomputable def TauCeti.QuadraticMap.specialOrthogonalGroupEquivSpecialIsometryGroupPolarBilin {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (h2 : IsSMulRegular R 2) : ↥(specialOrthogonalGroup Q) ≃* ↥(LinearMap.BilinForm.specialIsometryGroup (QuadraticMap.polarBilin Q))

The canonical group isomorphism between SO(Q) and the determinant-one isometry group of the polar bilinear form.

Equations

• TauCeti.QuadraticMap.specialOrthogonalGroupEquivSpecialIsometryGroupPolarBilin Q h2 = MulEquiv.subgroupCongr ⋯

@[simp]

theorem TauCeti.QuadraticMap.coe_specialOrthogonalGroupEquivSpecialIsometryGroupPolarBilin_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (h2 : IsSMulRegular R 2) (g : ↥(specialOrthogonalGroup Q)) : ↑((specialOrthogonalGroupEquivSpecialIsometryGroupPolarBilin Q h2) g) = ↑g

@[simp]

theorem TauCeti.QuadraticMap.coe_specialOrthogonalGroupEquivSpecialIsometryGroupPolarBilin_symm_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (h2 : IsSMulRegular R 2) (g : ↥(LinearMap.BilinForm.specialIsometryGroup (QuadraticMap.polarBilin Q))) : ↑((specialOrthogonalGroupEquivSpecialIsometryGroupPolarBilin Q h2).symm g) = ↑g

theorem QuadraticMap.neg_mem_orthogonalGroup {R : Type u} {M : Type v} {N : Type w} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (Q : QuadraticMap R M N) : LinearEquiv.neg R ∈ TauCeti.QuadraticMap.orthogonalGroup Q

Negation x ↦ -x preserves every quadratic map.

def QuadraticMap.negOrthogonal {R : Type u} {M : Type v} {N : Type w} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (Q : QuadraticMap R M N) : ↥(TauCeti.QuadraticMap.orthogonalGroup Q)

The isometry x ↦ -x, as an element of the orthogonal group. On a free module of rank one over a domain, it and 1 are the only isometries of a nonzero quadratic map valued in a torsion-free module (TauCeti.QuadraticMap.eq_one_or_eq_negOrthogonal_of_finrank_eq_one), and it differs from 1 when 2 ≠ 0. There it is also the reflection in every vector of invertible norm (QuadraticMap.reflectionOrthogonal_eq_negOrthogonal_of_finrank_eq_one).

Equations

• Q.negOrthogonal = ⟨LinearEquiv.neg R, ⋯⟩

@[simp]

theorem QuadraticMap.coe_negOrthogonal {R : Type u} {M : Type v} {N : Type w} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (Q : QuadraticMap R M N) : ↑Q.negOrthogonal = LinearEquiv.neg R

@[simp]

theorem QuadraticMap.negOrthogonal_mul_self {R : Type u} {M : Type v} {N : Type w} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (Q : QuadraticMap R M N) : Q.negOrthogonal * Q.negOrthogonal = 1

Negation is an involution of the orthogonal group.

@[simp]

theorem QuadraticMap.negOrthogonal_inv {R : Type u} {M : Type v} {N : Type w} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (Q : QuadraticMap R M N) : Q.negOrthogonal⁻¹ = Q.negOrthogonal

noncomputable def QuadraticMap.orthogonalDet {R : Type u} {M : Type v} {N : Type w} [CommRing R] [AddCommGroup M] [Module R M] [AddCommMonoid N] [Module R N] (Q : QuadraticMap R M N) : ↥(TauCeti.QuadraticMap.orthogonalGroup Q) →* Rˣ

The determinant of an orthogonal automorphism, as a homomorphism O(Q) →* Rˣ.

Equations

• Q.orthogonalDet = LinearEquiv.det.comp (TauCeti.QuadraticMap.orthogonalGroup Q).subtype

@[simp]

theorem QuadraticMap.orthogonalDet_apply {R : Type u} {M : Type v} {N : Type w} [CommRing R] [AddCommGroup M] [Module R M] [AddCommMonoid N] [Module R N] {Q : QuadraticMap R M N} (g : ↥(TauCeti.QuadraticMap.orthogonalGroup Q)) : Q.orthogonalDet g = LinearEquiv.det ↑g

noncomputable def QuadraticMap.specialOrthogonalWithin {R : Type u} {M : Type v} {N : Type w} [CommRing R] [AddCommGroup M] [Module R M] [AddCommMonoid N] [Module R N] (Q : QuadraticMap R M N) : Subgroup ↥(TauCeti.QuadraticMap.orthogonalGroup Q)

The determinant-one subgroup of O(Q), as a subgroup of orthogonalGroup Q: the kernel of orthogonalDet Q. By contrast specialOrthogonalGroup Q is a subgroup of M ≃ₗ[R] M; the two are identified by specialOrthogonalWithin_eq_subgroupOf and specialOrthogonalWithinEquiv.

Equations

• Q.specialOrthogonalWithin = Q.orthogonalDet.ker

@[simp]

theorem QuadraticMap.mem_specialOrthogonalWithin_iff {R : Type u} {M : Type v} {N : Type w} [CommRing R] [AddCommGroup M] [Module R M] [AddCommMonoid N] [Module R N] {Q : QuadraticMap R M N} {g : ↥(TauCeti.QuadraticMap.orthogonalGroup Q)} : g ∈ Q.specialOrthogonalWithin ↔ LinearEquiv.det ↑g = 1

theorem QuadraticMap.specialOrthogonalWithin_eq_subgroupOf {R : Type u} {M : Type v} {N : Type w} [CommRing R] [AddCommGroup M] [Module R M] [AddCommMonoid N] [Module R N] {Q : QuadraticMap R M N} : Q.specialOrthogonalWithin = (TauCeti.QuadraticMap.specialOrthogonalGroup Q).subgroupOf (TauCeti.QuadraticMap.orthogonalGroup Q)

specialOrthogonalWithin Q is the special orthogonal group pulled back to O(Q).

noncomputable def QuadraticMap.specialOrthogonalToOrthogonal {R : Type u} {M : Type v} {N : Type w} [CommRing R] [AddCommGroup M] [Module R M] [AddCommMonoid N] [Module R N] (Q : QuadraticMap R M N) : ↥(TauCeti.QuadraticMap.specialOrthogonalGroup Q) →* ↥(TauCeti.QuadraticMap.orthogonalGroup Q)

The inclusion SO(Q) →* O(Q).

Equations

• Q.specialOrthogonalToOrthogonal = Subgroup.inclusion ⋯

@[simp]

theorem QuadraticMap.coe_specialOrthogonalToOrthogonal {R : Type u} {M : Type v} {N : Type w} [CommRing R] [AddCommGroup M] [Module R M] [AddCommMonoid N] [Module R N] {Q : QuadraticMap R M N} (g : ↥(TauCeti.QuadraticMap.specialOrthogonalGroup Q)) : ↑(Q.specialOrthogonalToOrthogonal g) = ↑g

theorem QuadraticMap.orthogonalDet_specialOrthogonalToOrthogonal {R : Type u} {M : Type v} {N : Type w} [CommRing R] [AddCommGroup M] [Module R M] [AddCommMonoid N] [Module R N] {Q : QuadraticMap R M N} (g : ↥(TauCeti.QuadraticMap.specialOrthogonalGroup Q)) : Q.orthogonalDet (Q.specialOrthogonalToOrthogonal g) = 1

The orthogonal determinant of an element of SO(Q) is one.

theorem QuadraticMap.specialOrthogonalToOrthogonal_injective {R : Type u} {M : Type v} {N : Type w} [CommRing R] [AddCommGroup M] [Module R M] [AddCommMonoid N] [Module R N] {Q : QuadraticMap R M N} : Function.Injective ⇑Q.specialOrthogonalToOrthogonal

@[simp]

theorem QuadraticMap.range_specialOrthogonalToOrthogonal {R : Type u} {M : Type v} {N : Type w} [CommRing R] [AddCommGroup M] [Module R M] [AddCommMonoid N] [Module R N] {Q : QuadraticMap R M N} : Q.specialOrthogonalToOrthogonal.range = Q.specialOrthogonalWithin

The image of SO(Q) in O(Q) is exactly the determinant kernel.

noncomputable def QuadraticMap.specialOrthogonalWithinEquiv {R : Type u} {M : Type v} {N : Type w} [CommRing R] [AddCommGroup M] [Module R M] [AddCommMonoid N] [Module R N] (Q : QuadraticMap R M N) : ↥Q.specialOrthogonalWithin ≃* ↥(TauCeti.QuadraticMap.specialOrthogonalGroup Q)

The determinant kernel inside O(Q) is canonically isomorphic to SO(Q).

Equations

• Q.specialOrthogonalWithinEquiv = (MulEquiv.subgroupCongr ⋯).trans (Subgroup.subgroupOfEquivOfLe ⋯)

@[simp]

theorem QuadraticMap.coe_specialOrthogonalWithinEquiv_apply {R : Type u} {M : Type v} {N : Type w} [CommRing R] [AddCommGroup M] [Module R M] [AddCommMonoid N] [Module R N] {Q : QuadraticMap R M N} (g : ↥Q.specialOrthogonalWithin) : ↑(Q.specialOrthogonalWithinEquiv g) = ↑↑g

@[simp]

theorem QuadraticMap.coe_specialOrthogonalWithinEquiv_symm_apply {R : Type u} {M : Type v} {N : Type w} [CommRing R] [AddCommGroup M] [Module R M] [AddCommMonoid N] [Module R N] {Q : QuadraticMap R M N} (g : ↥(TauCeti.QuadraticMap.specialOrthogonalGroup Q)) : ↑(Q.specialOrthogonalWithinEquiv.symm g) = Q.specialOrthogonalToOrthogonal g

theorem QuadraticMap.specialOrthogonalWithin_eq_top {R : Type u} {M : Type v} {N : Type w} [CommRing R] [AddCommGroup M] [Module R M] [AddCommMonoid N] [Module R N] {Q : QuadraticMap R M N} [Subsingleton M] : Q.specialOrthogonalWithin = ⊤

On a zero module the determinant kernel is all of O(Q), both groups being trivial; this is the case excluded from index_specialOrthogonalWithin.

noncomputable def QuadraticMap.IsometryEquiv.specialOrthogonalGroupCongr {R : Type u} {M₁ : Type u_1} {M₂ : Type u_2} {N : Type w} [CommRing R] [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] [AddCommMonoid N] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (e : Q₁.IsometryEquiv Q₂) : ↥(TauCeti.QuadraticMap.specialOrthogonalGroup Q₁) ≃* ↥(TauCeti.QuadraticMap.specialOrthogonalGroup Q₂)

Isometric quadratic maps have isomorphic special orthogonal groups: conjugation by an isometric equivalence e : Q₁.IsometryEquiv Q₂ carries SO(Q₁) onto SO(Q₂).

Equations

• e.specialOrthogonalGroupCongr = TauCeti.Subgroup.congrOfMapEq e.autCongr ⋯

@[simp]

theorem QuadraticMap.IsometryEquiv.coe_specialOrthogonalGroupCongr_apply {R : Type u} {M₁ : Type u_1} {M₂ : Type u_2} {N : Type w} [CommRing R] [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] [AddCommMonoid N] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (e : Q₁.IsometryEquiv Q₂) (f : ↥(TauCeti.QuadraticMap.specialOrthogonalGroup Q₁)) (m : M₂) : ↑(e.specialOrthogonalGroupCongr f) m = e (↑f (e.symm m))

Evaluating special-orthogonal transport is conjugation by the isometry e.

@[simp]

theorem QuadraticMap.IsometryEquiv.coe_specialOrthogonalGroupCongr_symm_apply {R : Type u} {M₁ : Type u_1} {M₂ : Type u_2} {N : Type w} [CommRing R] [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] [AddCommMonoid N] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (e : Q₁.IsometryEquiv Q₂) (g : ↥(TauCeti.QuadraticMap.specialOrthogonalGroup Q₂)) (m : M₁) : ↑(e.specialOrthogonalGroupCongr.symm g) m = e.symm (↑g (e m))

Evaluating inverse special-orthogonal transport is conjugation by the inverse isometry e.symm.

@[simp]

theorem QuadraticMap.IsometryEquiv.orthogonalDet_orthogonalGroupCongr {R : Type u} {M₁ : Type u_1} {M₂ : Type u_2} {N : Type w} [CommRing R] [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] [AddCommMonoid N] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (e : Q₁.IsometryEquiv Q₂) (g : ↥(TauCeti.QuadraticMap.orthogonalGroup Q₁)) : Q₂.orthogonalDet (e.orthogonalGroupCongr g) = Q₁.orthogonalDet g

Transporting an orthogonal automorphism along an isometry preserves its determinant.

This has high simplifier priority so it fires before the general orthogonalDet_apply projection lemma hides the transport.

@[simp]

theorem QuadraticMap.IsometryEquiv.specialOrthogonalToOrthogonal_specialOrthogonalGroupCongr {R : Type u} {M₁ : Type u_1} {M₂ : Type u_2} {N : Type w} [CommRing R] [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] [AddCommMonoid N] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (e : Q₁.IsometryEquiv Q₂) (g : ↥(TauCeti.QuadraticMap.specialOrthogonalGroup Q₁)) : Q₂.specialOrthogonalToOrthogonal (e.specialOrthogonalGroupCongr g) = e.orthogonalGroupCongr (Q₁.specialOrthogonalToOrthogonal g)

Transport of special orthogonal groups commutes with their inclusions into the full orthogonal groups.

@[simp]

theorem QuadraticMap.IsometryEquiv.specialOrthogonalGroupCongr_refl {R : Type u} {M₁ : Type u_1} {N : Type w} [CommRing R] [AddCommGroup M₁] [Module R M₁] [AddCommMonoid N] [Module R N] {Q₁ : QuadraticMap R M₁ N} : (refl Q₁).specialOrthogonalGroupCongr = MulEquiv.refl ↥(TauCeti.QuadraticMap.specialOrthogonalGroup Q₁)

Transporting the special orthogonal group along the identity isometry is the identity equivalence.

@[simp]

theorem QuadraticMap.IsometryEquiv.specialOrthogonalGroupCongr_trans {R : Type u} {M₁ : Type u_1} {M₂ : Type u_2} {M₃ : Type u_3} {N : Type w} [CommRing R] [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup M₃] [Module R M₃] [AddCommMonoid N] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} {Q₃ : QuadraticMap R M₃ N} (e₁₂ : Q₁.IsometryEquiv Q₂) (e₂₃ : Q₂.IsometryEquiv Q₃) : (e₁₂.trans e₂₃).specialOrthogonalGroupCongr = e₁₂.specialOrthogonalGroupCongr.trans e₂₃.specialOrthogonalGroupCongr

Special-orthogonal-group transport respects composition of isometries.

theorem QuadraticMap.IsometryEquiv.specialOrthogonalGroupCongr_symm {R : Type u} {M₁ : Type u_1} {M₂ : Type u_2} {N : Type w} [CommRing R] [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] [AddCommMonoid N] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (e : Q₁.IsometryEquiv Q₂) : e.specialOrthogonalGroupCongr.symm = e.symm.specialOrthogonalGroupCongr

Inverting special-orthogonal-group transport is transport along the inverse isometry.

noncomputable def QuadraticMap.orthogonalToGeneralLinear {R : Type u} [CommSemiring R] {n : Type v} [Fintype n] [DecidableEq n] {N : Type w} [AddCommMonoid N] [Module R N] (Q : QuadraticMap R (n → R) N) : ↥(TauCeti.QuadraticMap.orthogonalGroup Q) →* GL n R

The coordinate inclusion of an orthogonal group into GL(n, R).

Equations

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

@[simp]

theorem QuadraticMap.orthogonalToGeneralLinear_apply {R : Type u} [CommSemiring R] {n : Type v} [Fintype n] [DecidableEq n] {N : Type w} [AddCommMonoid N] [Module R N] (Q : QuadraticMap R (n → R) N) (g : ↥(TauCeti.QuadraticMap.orthogonalGroup Q)) (i j : n) : ↑(Q.orthogonalToGeneralLinear g) i j = ↑g (Pi.single j 1) i

An orthogonal transformation acts through its usual coordinate matrix.

@[simp]

theorem QuadraticMap.coe_orthogonalToGeneralLinear {R : Type u} [CommSemiring R] {n : Type v} [Fintype n] [DecidableEq n] {N : Type w} [AddCommMonoid N] [Module R N] (Q : QuadraticMap R (n → R) N) (g : ↥(TauCeti.QuadraticMap.orthogonalGroup Q)) : ↑(Q.orthogonalToGeneralLinear g) = LinearMap.toMatrix' ↑↑g

The underlying matrix of the coordinate inclusion is the matrix of the linear equivalence.

theorem QuadraticMap.orthogonalToGeneralLinear_injective {R : Type u} [CommSemiring R] {n : Type v} [Fintype n] [DecidableEq n] {N : Type w} [AddCommMonoid N] [Module R N] (Q : QuadraticMap R (n → R) N) : Function.Injective ⇑Q.orthogonalToGeneralLinear

The coordinate inclusion of an orthogonal group is injective.

noncomputable def QuadraticMap.specialOrthogonalToGeneralLinear {R : Type u} [CommRing R] {n : Type v} [Fintype n] [DecidableEq n] {N : Type w} [AddCommMonoid N] [Module R N] (Q : QuadraticMap R (n → R) N) : ↥(TauCeti.QuadraticMap.specialOrthogonalGroup Q) →* GL n R

The coordinate inclusion of a special orthogonal group into GL(n, R).

Equations

• Q.specialOrthogonalToGeneralLinear = Q.orthogonalToGeneralLinear.comp Q.specialOrthogonalToOrthogonal

@[simp]

theorem QuadraticMap.specialOrthogonalToGeneralLinear_apply {R : Type u} [CommRing R] {n : Type v} [Fintype n] [DecidableEq n] {N : Type w} [AddCommMonoid N] [Module R N] (Q : QuadraticMap R (n → R) N) (g : ↥(TauCeti.QuadraticMap.specialOrthogonalGroup Q)) (i j : n) : ↑(Q.specialOrthogonalToGeneralLinear g) i j = ↑g (Pi.single j 1) i

A special orthogonal transformation acts through its usual coordinate matrix.

@[simp]

theorem TauCeti.QuadraticMap.specialOrthogonalToGeneralLinear_mulVec {R : Type u} [CommRing R] {n : Type v} [Fintype n] [DecidableEq n] {N : Type w} [AddCommMonoid N] [Module R N] (Q : QuadraticMap R (n → R) N) (g : ↥(specialOrthogonalGroup Q)) (v : n → R) : (↑(Q.specialOrthogonalToGeneralLinear g)).mulVec v = ↑g v

A special orthogonal transformation acts on coordinate vectors through its general-linear matrix.

theorem QuadraticMap.specialOrthogonalToGeneralLinear_injective {R : Type u} [CommRing R] {n : Type v} [Fintype n] [DecidableEq n] {N : Type w} [AddCommMonoid N] [Module R N] (Q : QuadraticMap R (n → R) N) : Function.Injective ⇑Q.specialOrthogonalToGeneralLinear

The coordinate inclusion of a special orthogonal group is injective.

noncomputable def TauCeti.QuadraticMap.reflection {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (v : M) [Invertible (Q v)] : M ≃ₗ[R] M

The reflection in a vector v of invertible norm: y ↦ y - (polar Q v y / Q v) • v. This is Mathlib's Module.reflection for the functional y ↦ polar Q v y / Q v. When 2 is invertible it is the reflection in the hyperplane v ^ ⊥. In characteristic two v lies in the kernel of polar Q v and the map fixes v; over a field it is then a transvection, or the identity when polar Q v = 0.

Equations

• TauCeti.QuadraticMap.reflection Q v = Module.reflection ⋯

theorem TauCeti.QuadraticMap.reflection_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (v : M) [Invertible (Q v)] (y : M) : (reflection Q v) y = y - (⅟(Q v) * QuadraticMap.polar (⇑Q) v y) • v

@[simp]

theorem TauCeti.QuadraticMap.reflection_smul_eq {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (v : M) [Invertible (Q v)] (a : R) [Invertible a] : have x := ⋯.mpr (have x := invertibleMul a a; invertibleMul (a * a) (Q v)); reflection Q (a • v) = reflection Q v

Rescaling a vector of invertible norm by an invertible scalar does not change its quadratic reflection.

@[simp]

theorem TauCeti.QuadraticMap.reflection_apply_self {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (v : M) [Invertible (Q v)] : (reflection Q v) v = -v

theorem TauCeti.QuadraticMap.reflection_apply_of_polar_eq_zero {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (v : M) [Invertible (Q v)] {y : M} (hy : QuadraticMap.polar (⇑Q) v y = 0) : (reflection Q v) y = y

The reflection in v fixes the kernel of polar Q v.

theorem TauCeti.QuadraticMap.reflection_apply_of_isOrtho {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (v : M) [Invertible (Q v)] {y : M} (hy : QuadraticMap.IsOrtho Q v y) : (reflection Q v) y = y

The reflection in v fixes every vector orthogonal to v. When 2 is invertible, together with reflection_apply_self this says it is the reflection in the hyperplane v ^ ⊥.

theorem TauCeti.QuadraticMap.reflection_mul_self {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (v : M) [Invertible (Q v)] : reflection Q v * reflection Q v = 1

A reflection is an involution, so it has order dividing two in the orthogonal group.

@[simp]

theorem TauCeti.QuadraticMap.reflection_inv {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (v : M) [Invertible (Q v)] : (reflection Q v)⁻¹ = reflection Q v

A reflection is its own inverse.

@[simp]

theorem TauCeti.QuadraticMap.reflection_symm {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (v : M) [Invertible (Q v)] : (reflection Q v).symm = reflection Q v

A reflection is its own inverse, as a linear equivalence.

@[simp]

theorem TauCeti.QuadraticMap.det_reflection {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (v : M) [Invertible (Q v)] [Module.Free R M] [Module.Finite R M] : LinearEquiv.det (reflection Q v) = -1

The determinant of a reflection is -1 on a finite free module.

theorem TauCeti.QuadraticMap.reflection_mem_orthogonalGroup {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (v : M) [Invertible (Q v)] : reflection Q v ∈ orthogonalGroup Q

Reflections are orthogonal. These are the generators a Cartan-Dieudonné theorem writes an orthogonal automorphism as a product of, over a field of characteristic not two, for a nondegenerate form, in finite dimension; none of that is assumed here. In characteristic two polar Q v v is 2 • Q v = 0, so v lies in the kernel of polar Q v and reflection Q v fixes v (over a field it is a transvection or the identity), which is why that theorem excludes characteristic two. They are also the image of the generating vectors of the Pin group under twisted conjugation.

noncomputable def TauCeti.QuadraticMap.reflectionOrthogonal {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (v : M) [Invertible (Q v)] : ↥(orthogonalGroup Q)

The reflection in a vector of invertible norm, as an element of the orthogonal group.

reflection_mem_orthogonalGroup gives the membership; this bundles it, so that statements about reflections inside orthogonalGroup Q — products of reflections, membership in the range of the Pin and Spin actions, generation results — can name the group element instead of repeating the anonymous constructor.

Equations

• TauCeti.QuadraticMap.reflectionOrthogonal Q v = ⟨TauCeti.QuadraticMap.reflection Q v, ⋯⟩

@[simp]

theorem TauCeti.QuadraticMap.coe_reflectionOrthogonal {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (v : M) [Invertible (Q v)] : ↑(reflectionOrthogonal Q v) = reflection Q v

@[simp]

theorem TauCeti.QuadraticMap.reflectionOrthogonal_smul_eq {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (v : M) [Invertible (Q v)] (a : R) [Invertible a] : have x := ⋯.mpr (have x := invertibleMul a a; invertibleMul (a * a) (Q v)); reflectionOrthogonal Q (a • v) = reflectionOrthogonal Q v

Rescaling the defining vector by an invertible scalar does not change the bundled orthogonal reflection.

@[simp]

theorem TauCeti.QuadraticMap.reflectionOrthogonal_mul_self {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (v : M) [Invertible (Q v)] : reflectionOrthogonal Q v * reflectionOrthogonal Q v = 1

The bundled reflection is an involution, so it has order dividing two in the orthogonal group.

@[simp]

theorem TauCeti.QuadraticMap.reflectionOrthogonal_inv {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (v : M) [Invertible (Q v)] : (reflectionOrthogonal Q v)⁻¹ = reflectionOrthogonal Q v

The bundled reflection is its own inverse in the orthogonal group.

theorem QuadraticMap.orthogonalDet_reflectionOrthogonal {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (v : M) [Invertible (Q v)] [Module.Free R M] [Module.Finite R M] : (orthogonalDet Q) (TauCeti.QuadraticMap.reflectionOrthogonal Q v) = -1

The orthogonal determinant of a reflection is minus one.

theorem TauCeti.QuadraticMap.reflection_map_apply {R : Type u} {M₁ : Type u_1} {M₂ : Type u_2} [CommRing R] [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (e : QuadraticMap.IsometryEquiv Q₁ Q₂) (v : M₁) [Invertible (Q₁ v)] [Invertible (Q₂ (e v))] (x : M₂) : (reflection Q₂ (e v)) x = e ((reflection Q₁ v) (e.symm x))

An isometric equivalence e carries the reflection in v to the reflection in e v: τ_{e v} = e ∘ τ_v ∘ e⁻¹. This is the quadratic-form analogue of Mathlib's Submodule.reflection_map_apply in Mathlib.Analysis.InnerProductSpace.Projection.Reflection.

theorem TauCeti.QuadraticMap.reflection_map {R : Type u} {M₁ : Type u_1} {M₂ : Type u_2} [CommRing R] [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (e : QuadraticMap.IsometryEquiv Q₁ Q₂) (v : M₁) [Invertible (Q₁ v)] [Invertible (Q₂ (e v))] : reflection Q₂ (e v) = e.symm ≪≫ₗ (reflection Q₁ v ≪≫ₗ e.toLinearEquiv)

An isometric equivalence e carries the reflection in v to the reflection in e v, as linear equivalences: τ_{e v} = e ∘ τ_v ∘ e⁻¹.

theorem TauCeti.QuadraticMap.orthogonalGroupCongr_reflectionOrthogonal {R : Type u} {M₁ : Type u_1} {M₂ : Type u_2} [CommRing R] [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (e : QuadraticMap.IsometryEquiv Q₁ Q₂) (v : M₁) [Invertible (Q₁ v)] [Invertible (Q₂ (e v))] : e.orthogonalGroupCongr (reflectionOrthogonal Q₁ v) = reflectionOrthogonal Q₂ (e v)

Transporting orthogonal groups along an isometric equivalence e carries the reflection in v to the reflection in e v.

theorem TauCeti.QuadraticMap.mul_reflectionOrthogonal_mul_inv {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (g : ↥(orthogonalGroup Q)) (v : M) [Invertible (Q v)] [Invertible (Q (↑g v))] : g * reflectionOrthogonal Q v * g⁻¹ = reflectionOrthogonal Q (↑g v)

The conjugation law for reflections: g τ_v g⁻¹ = τ_{g v} for g ∈ O(Q). So every conjugate of τ_v in O(Q) is the reflection in a vector of the O(Q)-orbit of v, in particular in a vector with the same value of Q.

theorem TauCeti.QuadraticMap.reflection_apply_eq_sub_div {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (v : V) [Invertible (Q v)] (x : V) : (reflection Q v) x = x - (QuadraticMap.polar (⇑Q) v x / Q v) • v

Over a field, the reflection in v is x ↦ x - (polar Q v x / Q v) • v.

theorem QuadraticForm.polar_div_eq_two_mul_polar_div_polar {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) [NeZero 2] (v x : V) : QuadraticMap.polar (⇑Q) v x / Q v = 2 * QuadraticMap.polar (⇑Q) v x / QuadraticMap.polar (⇑Q) v v

The two spellings of the reflection coefficient agree. Dividing the un-halved polar form by Q v is the same as dividing twice it by polar Q v v = 2 • Q v, the form in which sources whose bilinear form b satisfies b v v = Q v write the reflection. No anisotropy is needed, since both sides vanish when Q v = 0.

theorem TauCeti.QuadraticMap.reflection_apply_eq_sub_two_mul_div {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) [NeZero 2] (v : V) [Invertible (Q v)] (x : V) : (reflection Q v) x = x - (2 * QuadraticMap.polar (⇑Q) v x / QuadraticMap.polar (⇑Q) v v) • v

The reflection in v is x ↦ x - (2 * polar Q v x / polar Q v v) • v.

theorem TauCeti.QuadraticMap.reflection_sub_apply_eq_of_map_eq {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (x y : M) (hxy : Q x = Q y) [Invertible (Q (x - y))] : (reflection Q (x - y)) x = y

If x and y have the same quadratic value, reflecting x in x - y carries it to y whenever x - y has invertible norm.

theorem TauCeti.QuadraticMap.isUnit_sub_or_add_of_map_eq {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) [NeZero 2] (x y : V) (hxy : Q x = Q y) (hy : Q y ≠ 0) : IsUnit (Q (x - y)) ∨ IsUnit (Q (x + y))

If x and y have the same nonzero quadratic value, at least one of x - y and x + y has nonzero, hence invertible, norm.

theorem QuadraticMap.exists_isometryEquiv_apply_eq_of_map_eq {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) [NeZero 2] {x y : V} (hxy : Q x = Q y) (hy : Q y ≠ 0) : ∃ (f : IsometryEquiv Q Q), f x = y

Witt transitivity (Lam I.4.5): over a field of characteristic different from two, any two vectors with the same nonzero value are related by an isometry of the quadratic form.

theorem TauCeti.QuadraticMap.exists_reflectionOrthogonal_list_prod_mul_eqOn_sup_span_singleton {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) [NeZero 2] (g : ↥(orthogonalGroup Q)) (W : Submodule K V) (hfix : ∀ w ∈ W, ↑g w = w) (x : V) [Invertible (Q x)] (hx : ∀ w ∈ W, QuadraticMap.IsOrtho Q x w) : ∃ (l : List ↥(orthogonalGroup Q)), (∀ r ∈ l, ∃ (v : V) (x : Invertible (Q v)), reflectionOrthogonal Q v = r) ∧ l.length ≤ 2 ∧ ∀ y ∈ W ⊔ K ∙ x, ↑(l.prod * g) y = y

If g fixes a subspace W pointwise and x is anisotropic and orthogonal to W, a list of at most two anisotropic reflections can be multiplied into g so that the product fixes W ⊔ K ∙ x pointwise.

theorem TauCeti.QuadraticMap.orthogonalDet_sq {R : Type u} {M : Type v} [CommRing R] [IsDomain R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] {Q : QuadraticForm R M} (hQ : LinearMap.SeparatingLeft (QuadraticMap.polarBilin Q)) (g : ↥(orthogonalGroup Q)) : (QuadraticMap.orthogonalDet Q) g ^ 2 = 1

The determinant of an isometry squares to one. If the polar form of Q is left-separating on a finite free module over an integral domain, every orthogonal automorphism has determinant ±1.

theorem TauCeti.QuadraticMap.finiteIndex_specialOrthogonalWithin {R : Type u} {M : Type v} [CommRing R] [IsDomain R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] {Q : QuadraticForm R M} (hQ : LinearMap.SeparatingLeft (QuadraticMap.polarBilin Q)) : (QuadraticMap.specialOrthogonalWithin Q).FiniteIndex

If the polar form is left-separating on a finite free module over an integral domain, then SO(Q) has finite index in O(Q): every orthogonal determinant is a square root of unity, and there are only finitely many of those.

theorem TauCeti.QuadraticMap.range_orthogonalDet {K : Type u} {V : Type v} [Field K] [NeZero 2] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {Q : QuadraticForm K V} [Nontrivial V] (hQ : QuadraticMap.Nondegenerate) : (QuadraticMap.orthogonalDet Q).range = rootsOfUnity 2 K

The determinant lands exactly in μ₂. For a nondegenerate form over a field of characteristic not two on a nonzero finite-dimensional space, the determinants of the orthogonal automorphisms are exactly the square roots of unity ±1.

theorem TauCeti.QuadraticMap.index_specialOrthogonalWithin {K : Type u} {V : Type v} [Field K] [NeZero 2] [AddCommGroup V] [Module K V] [FiniteDimensional K V] {Q : QuadraticForm K V} [Nontrivial V] (hQ : QuadraticMap.Nondegenerate) : (QuadraticMap.specialOrthogonalWithin Q).index = 2

SO(Q) has index two in O(Q) for a nondegenerate form over a field of characteristic not two, on a nonzero finite-dimensional space. On the zero space the two groups coincide (specialOrthogonalWithin_eq_top).

theorem TauCeti.QuadraticMap.exists_orthogonalGroup_toLinearMap_eq {R : Type u} {M : Type v} [CommRing R] [IsDomain R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] {Q : QuadraticForm R M} (hQ : LinearMap.SeparatingLeft (QuadraticMap.polarBilin Q)) {f : Module.End R M} (hf : ∀ (x : M), Q (f x) = Q x) : ∃ (g : ↥(orthogonalGroup Q)), ↑↑g = f

A form-preserving endomorphism of a finite free module over a domain lifts to an orthogonal automorphism when the polar form is left-separating.

theorem TauCeti.QuadraticMap.range_orthogonalGroup_toLinearMap {R : Type u} {M : Type v} [CommRing R] [IsDomain R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] (Q : QuadraticForm R M) (hQ : LinearMap.SeparatingLeft (QuadraticMap.polarBilin Q)) : (Set.range fun (g : ↥(orthogonalGroup Q)) => ↑↑g) = {f : Module.End R M | ∀ (x : M), Q (f x) = Q x}

An endomorphism of a finite free module over a domain preserves a quadratic form with left-separating polar form exactly when it underlies an orthogonal automorphism.