Structural isometries and special orthogonal groups of quadratic-map products

The orthogonal product (Q₁, Q₂) ↦ Q₁.prod Q₂ is linear in the pair of quadratic maps (QuadraticMap.prodLinear).

Mathlib records the commutativity isometries of QuadraticMap.prod (QuadraticMap.IsometryEquiv.prodComm and QuadraticMap.IsometryEquiv.prodProdProdComm). This file adds the two remaining structural ones: the associator, and the deletion of a factor whose module is trivial. Together with QuadraticMap.IsometryEquiv.prodComm they are what makes orthogonal sum a commutative monoid operation on isometry classes of quadratic forms; the left-commutativity isometry Q₁ ⊕ (Q₂ ⊕ Q₃) ≅ Q₂ ⊕ (Q₁ ⊕ Q₃) is recorded as a composite of them. For an orthogonal sum QuadraticMap.pi indexed by Fin (n + 1), splitting off the first summand is likewise isometric, which lets such a sum be assembled one summand at a time; reindexing an orthogonal sum along an equivalence of its index types is isometric; and so is deleting the summands of an orthogonal sum that are carried by trivial modules.

For a quadratic form over a commutative ring, it also records the isometry associated to a direct-sum decomposition of the underlying module that is orthogonal for the polar form.

Finally, it embeds the product of the orthogonal groups of two quadratic maps with a common codomain into the orthogonal group of their orthogonal sum, acting componentwise, and identifies the image: an orthogonal transformation of Q₁.prod Q₂ is such an orthogonal sum exactly when it maps each summand into itself. No finiteness is needed for this, since a linear automorphism of M₁ × M₂ preserving both summands is automatically a product of automorphisms of the summands. For finite free modules the determinant of an orthogonal sum is the product of the determinants, so the embedding restricts to the special orthogonal groups. Concatenating orthogonal families of the two summands gives an orthogonal family of the orthogonal sum.

Main definitions

• QuadraticMap.prodLinear: the orthogonal product (Q₁, Q₂) ↦ Q₁.prod Q₂, as a linear map.
• QuadraticMap.IsometryEquiv.prodAssoc: LinearEquiv.prodAssoc is isometric.
• QuadraticMap.IsometryEquiv.prodLeftComm: exchanging the first two factors of Q₁ ⊕ (Q₂ ⊕ Q₃) is isometric.
• QuadraticMap.IsometryEquiv.uniqueProd: LinearEquiv.uniqueProd is isometric.
• QuadraticMap.IsometryEquiv.consPi: Fin.consLinearEquiv is isometric.
• QuadraticMap.IsometryEquiv.piCongrLeft: LinearEquiv.piCongrLeft is isometric.
• QuadraticMap.IsometryEquiv.piSubtype: deleting the summands of an orthogonal sum that are carried by trivial modules is isometric.
• QuadraticMap.IsometryEquiv.prodRestrictOrthogonal: an orthogonal direct sum is isometric to the original form.
• QuadraticMap.orthogonalGroupProd: the orthogonal sum O(Q₁) × O(Q₂) →* O(Q₁.prod Q₂).
• QuadraticMap.specialOrthogonalGroupProd: its restriction SO(Q₁) × SO(Q₂) →* SO(Q₁.prod Q₂).

Main results

• QuadraticMap.orthogonalGroupProd_injective and QuadraticMap.specialOrthogonalGroupProd_injective: both maps are injective.
• QuadraticMap.mem_range_orthogonalGroupProd_iff: the image of orthogonalGroupProd is exactly the subgroup of orthogonal transformations of Q₁.prod Q₂ preserving both summands.
• QuadraticMap.mem_range_specialOrthogonalGroupProd_iff: the image of specialOrthogonalGroupProd consists of the special orthogonal transformations preserving both summands whose two diagonal blocks have determinant one.
• QuadraticMap.det_orthogonalGroupProd: the determinant of an orthogonal sum is the product of the determinants.
• QuadraticMap.isOrthoᵢ_associated_prod: orthogonal families of the summands concatenate to an orthogonal family of Q₁.prod Q₂.

References

• O. T. O'Meara, Introduction to Quadratic Forms (1963), §43.

@[simp]

theorem QuadraticMap.smul_prod {R : Type u_1} {S : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_5} [CommSemiring R] [Monoid S] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid P] [Module R M₁] [Module R M₂] [Module R P] [DistribMulAction S P] [SMulCommClass S R P] (c : S) (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) : c • Q₁.prod Q₂ = (c • Q₁).prod (c • Q₂)

Scaling an orthogonal product scales both of its factors.

def QuadraticMap.prodLinear (R : Type u_1) (M₁ : Type u_2) (M₂ : Type u_3) (P : Type u_4) [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid P] [Module R M₁] [Module R M₂] [Module R P] : QuadraticMap R M₁ P × QuadraticMap R M₂ P →ₗ[R] QuadraticMap R (M₁ × M₂) P

The orthogonal product (Q₁, Q₂) ↦ Q₁.prod Q₂ of quadratic maps, as a linear map.

@[simp]

theorem QuadraticMap.prodLinear_apply {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {P : Type u_4} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid P] [Module R M₁] [Module R M₂] [Module R P] (Q : QuadraticMap R M₁ P × QuadraticMap R M₂ P) : (prodLinear R M₁ M₂ P) Q = Q.1.prod Q.2

Unfolding QuadraticMap.prodLinear.

def QuadraticMap.IsometryEquiv.prodAssoc {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} {P : Type u_5} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid P] [Module R M₁] [Module R M₂] [Module R M₃] [Module R P] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) (Q₃ : QuadraticMap R M₃ P) : ((Q₁.prod Q₂).prod Q₃).IsometryEquiv (Q₁.prod (Q₂.prod Q₃))

LinearEquiv.prodAssoc is isometric.

@[simp]

theorem QuadraticMap.IsometryEquiv.prodAssoc_apply {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} {P : Type u_5} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid P] [Module R M₁] [Module R M₂] [Module R M₃] [Module R P] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) (Q₃ : QuadraticMap R M₃ P) (m : (M₁ × M₂) × M₃) : (prodAssoc Q₁ Q₂ Q₃) m = (m.1.1, m.1.2, m.2)

The forward map of QuadraticMap.IsometryEquiv.prodAssoc.

@[simp]

theorem QuadraticMap.IsometryEquiv.prodAssoc_symm_apply {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} {P : Type u_5} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid P] [Module R M₁] [Module R M₂] [Module R M₃] [Module R P] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) (Q₃ : QuadraticMap R M₃ P) (m : M₁ × M₂ × M₃) : (prodAssoc Q₁ Q₂ Q₃).invFun m = ((m.1, m.2.1), m.2.2)

The inverse map of QuadraticMap.IsometryEquiv.prodAssoc.

def QuadraticMap.IsometryEquiv.prodLeftComm {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} {P : Type u_5} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid P] [Module R M₁] [Module R M₂] [Module R M₃] [Module R P] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) (Q₃ : QuadraticMap R M₃ P) : (Q₁.prod (Q₂.prod Q₃)).IsometryEquiv (Q₂.prod (Q₁.prod Q₃))

Exchanging the first two factors of an iterated orthogonal product is isometric: Q₁ ⊕ (Q₂ ⊕ Q₃) ≅ Q₂ ⊕ (Q₁ ⊕ Q₃). It lets a summand be moved past others to its place in an orthogonal sum.

@[simp]

theorem QuadraticMap.IsometryEquiv.prodLeftComm_apply {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {M₃ : Type u_4} {P : Type u_5} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃] [AddCommMonoid P] [Module R M₁] [Module R M₂] [Module R M₃] [Module R P] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) (Q₃ : QuadraticMap R M₃ P) (m : M₁ × M₂ × M₃) : (prodLeftComm Q₁ Q₂ Q₃) m = (m.2.1, m.1, m.2.2)

The forward map of QuadraticMap.IsometryEquiv.prodLeftComm.

def QuadraticMap.IsometryEquiv.uniqueProd {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {P : Type u_5} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid P] [Module R M₁] [Module R M₂] [Module R P] [Unique M₁] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) : (Q₁.prod Q₂).IsometryEquiv Q₂

LinearEquiv.uniqueProd is isometric: a factor carried by a trivial module may be deleted from an orthogonal product.

@[simp]

theorem QuadraticMap.IsometryEquiv.uniqueProd_apply {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {P : Type u_5} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid P] [Module R M₁] [Module R M₂] [Module R P] [Unique M₁] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) (m : M₁ × M₂) : (uniqueProd Q₁ Q₂) m = m.2

The forward map of QuadraticMap.IsometryEquiv.uniqueProd.

@[simp]

theorem QuadraticMap.IsometryEquiv.uniqueProd_symm_apply {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {P : Type u_5} [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid P] [Module R M₁] [Module R M₂] [Module R P] [Unique M₁] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) (m : M₂) : (uniqueProd Q₁ Q₂).invFun m = (default, m)

The inverse map of QuadraticMap.IsometryEquiv.uniqueProd.

def QuadraticMap.IsometryEquiv.consPi {R : Type u_1} {P : Type u_5} [CommSemiring R] [AddCommMonoid P] [Module R P] {n : ℕ} {M : Fin (n + 1) → Type u_6} [(i : Fin (n + 1)) → AddCommMonoid (M i)] [(i : Fin (n + 1)) → Module R (M i)] (Q : (i : Fin (n + 1)) → QuadraticMap R (M i) P) : ((Q 0).prod (QuadraticMap.pi fun (i : Fin n) => Q i.succ)).IsometryEquiv (QuadraticMap.pi Q)

Fin.consLinearEquiv is isometric: an orthogonal sum indexed by Fin (n + 1) is the orthogonal product of its first summand with the orthogonal sum of the remaining ones.

@[simp]

theorem QuadraticMap.IsometryEquiv.consPi_apply {R : Type u_1} {P : Type u_5} [CommSemiring R] [AddCommMonoid P] [Module R P] {n : ℕ} {M : Fin (n + 1) → Type u_6} [(i : Fin (n + 1)) → AddCommMonoid (M i)] [(i : Fin (n + 1)) → Module R (M i)] (Q : (i : Fin (n + 1)) → QuadraticMap R (M i) P) (x : M 0) (y : (i : Fin n) → M i.succ) : (consPi Q) (x, y) = Fin.cons x y

The forward map of QuadraticMap.IsometryEquiv.consPi.

def QuadraticMap.IsometryEquiv.piCongrLeft {R : Type u_1} {P : Type u_5} [CommSemiring R] [AddCommMonoid P] [Module R P] {ι : Type u_6} {ι' : Type u_7} [Fintype ι] [Fintype ι'] {M : ι → Type u_8} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (Q : (i : ι) → QuadraticMap R (M i) P) (e : ι' ≃ ι) : (QuadraticMap.pi fun (i' : ι') => Q (e i')).IsometryEquiv (QuadraticMap.pi Q)

LinearEquiv.piCongrLeft is isometric: reindexing an orthogonal sum along an equivalence of its finite index types does not change it.

@[simp]

theorem QuadraticMap.IsometryEquiv.toLinearEquiv_piCongrLeft {R : Type u_1} {P : Type u_5} [CommSemiring R] [AddCommMonoid P] [Module R P] {ι : Type u_6} {ι' : Type u_7} [Fintype ι] [Fintype ι'] {M : ι → Type u_8} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (Q : (i : ι) → QuadraticMap R (M i) P) (e : ι' ≃ ι) : (piCongrLeft Q e).toLinearEquiv = LinearEquiv.piCongrLeft R M e

Reindexing an orthogonal sum has LinearEquiv.piCongrLeft as its underlying linear map.

@[simp]

theorem QuadraticMap.IsometryEquiv.piCongrLeft_apply_apply {R : Type u_1} {P : Type u_5} [CommSemiring R] [AddCommMonoid P] [Module R P] {ι : Type u_6} {ι' : Type u_7} [Fintype ι] [Fintype ι'] {M : ι → Type u_8} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (Q : (i : ι) → QuadraticMap R (M i) P) (e : ι' ≃ ι) (x : (i' : ι') → M (e i')) (i' : ι') : (piCongrLeft Q e) x (e i') = x i'

The forward map of QuadraticMap.IsometryEquiv.piCongrLeft at a reindexed coordinate.

def QuadraticMap.IsometryEquiv.piSubtype {R : Type u_1} {P : Type u_5} [CommSemiring R] [AddCommMonoid P] [Module R P] {ι : Type u_6} [Fintype ι] {M : ι → Type u_7} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (Q : (i : ι) → QuadraticMap R (M i) P) (S : ι → Prop) [DecidablePred S] (hS : ∀ (i : ι), ¬S i → Subsingleton (M i)) : (QuadraticMap.pi Q).IsometryEquiv (QuadraticMap.pi fun (i : Subtype S) => Q ↑i)

Restriction to the summands indexed by {i // S i} is isometric when every other summand is carried by a trivial module: such summands may be deleted from an orthogonal sum.

@[simp]

theorem QuadraticMap.IsometryEquiv.piSubtype_apply {R : Type u_1} {P : Type u_5} [CommSemiring R] [AddCommMonoid P] [Module R P] {ι : Type u_6} [Fintype ι] {M : ι → Type u_7} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (Q : (i : ι) → QuadraticMap R (M i) P) (S : ι → Prop) [DecidablePred S] (hS : ∀ (i : ι), ¬S i → Subsingleton (M i)) (x : (i : ι) → M i) (i : Subtype S) : (piSubtype Q S hS) x i = x ↑i

The forward map of QuadraticMap.IsometryEquiv.piSubtype restricts to the retained summands.

@[simp]

theorem QuadraticMap.IsometryEquiv.piSubtype_symm_apply {R : Type u_1} {P : Type u_5} [CommSemiring R] [AddCommMonoid P] [Module R P] {ι : Type u_6} [Fintype ι] {M : ι → Type u_7} [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (Q : (i : ι) → QuadraticMap R (M i) P) (S : ι → Prop) [DecidablePred S] (hS : ∀ (i : ι), ¬S i → Subsingleton (M i)) (y : (i : Subtype S) → M ↑i) (i : ι) : (piSubtype Q S hS).symm y i = if hi : S i then y ⟨i, hi⟩ else 0

The inverse map of QuadraticMap.IsometryEquiv.piSubtype extends by zero.

noncomputable def QuadraticMap.IsometryEquiv.prodRestrictOrthogonal {R : Type u_6} {V : Type u_7} [CommRing R] [AddCommGroup V] [Module R V] (Q : QuadraticForm R V) (W : Submodule R V) (hW : IsCompl W (LinearMap.BilinForm.orthogonal (polarBilin Q) W)) : ((restrict Q W).prod (restrict Q (LinearMap.BilinForm.orthogonal (polarBilin Q) W))).IsometryEquiv Q

An orthogonal direct-sum decomposition of a quadratic space, orthogonal for the polar form, gives an isometry from the product of the two restricted forms to the original form.

@[simp]

theorem QuadraticMap.IsometryEquiv.prodRestrictOrthogonal_apply {R : Type u_6} {V : Type u_7} [CommRing R] [AddCommGroup V] [Module R V] (Q : QuadraticForm R V) (W : Submodule R V) (hW : IsCompl W (LinearMap.BilinForm.orthogonal (polarBilin Q) W)) (x : ↥W × ↥(LinearMap.BilinForm.orthogonal (polarBilin Q) W)) : (prodRestrictOrthogonal Q W hW) x = ↑x.1 + ↑x.2

The orthogonal-decomposition isometry sends a pair to the sum of its components.

@[simp]

theorem QuadraticMap.IsometryEquiv.prodRestrictOrthogonal_symm_apply {R : Type u_6} {V : Type u_7} [CommRing R] [AddCommGroup V] [Module R V] (Q : QuadraticForm R V) (W : Submodule R V) (hW : IsCompl W (LinearMap.BilinForm.orthogonal (polarBilin Q) W)) (v : V) : (prodRestrictOrthogonal Q W hW).symm v = ((W.projectionOnto (LinearMap.BilinForm.orthogonal (polarBilin Q) W) hW) v, ((LinearMap.BilinForm.orthogonal (polarBilin Q) W).projectionOnto W ⋯) v)

The inverse of the orthogonal-decomposition isometry sends a vector to its two projections along the decomposition.

theorem QuadraticMap.prodCongr_mem_orthogonalGroup {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {N : Type u_4} [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} {f₁ : M₁ ≃ₗ[R] M₁} {f₂ : M₂ ≃ₗ[R] M₂} (hf₁ : f₁ ∈ TauCeti.QuadraticMap.orthogonalGroup Q₁) (hf₂ : f₂ ∈ TauCeti.QuadraticMap.orthogonalGroup Q₂) : f₁.prodCongr f₂ ∈ TauCeti.QuadraticMap.orthogonalGroup (Q₁.prod Q₂)

The componentwise product of orthogonal transformations of Q₁ and Q₂ is an orthogonal transformation of their orthogonal sum Q₁.prod Q₂.

def QuadraticMap.orthogonalGroupProd {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {N : Type u_4} [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) : ↥(TauCeti.QuadraticMap.orthogonalGroup Q₁) × ↥(TauCeti.QuadraticMap.orthogonalGroup Q₂) →* ↥(TauCeti.QuadraticMap.orthogonalGroup (Q₁.prod Q₂))

The orthogonal sum of orthogonal transformations: a pair (f₁, f₂) of orthogonal transformations of Q₁ and Q₂ acts on M₁ × M₂ componentwise, preserving Q₁.prod Q₂.

It is injective (orthogonalGroupProd_injective), and its image is exactly the subgroup of orthogonal transformations of Q₁.prod Q₂ that preserve both summands (mem_range_orthogonalGroupProd_iff).

@[simp]

theorem QuadraticMap.orthogonalGroupProd_apply {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {N : Type u_4} [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) (f : ↥(TauCeti.QuadraticMap.orthogonalGroup Q₁) × ↥(TauCeti.QuadraticMap.orthogonalGroup Q₂)) (x : M₁ × M₂) : ↑((Q₁.orthogonalGroupProd Q₂) f) x = (↑f.1 x.1, ↑f.2 x.2)

The orthogonal sum of two orthogonal transformations acts componentwise.

theorem QuadraticMap.coe_orthogonalGroupProd {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {N : Type u_4} [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) (f : ↥(TauCeti.QuadraticMap.orthogonalGroup Q₁) × ↥(TauCeti.QuadraticMap.orthogonalGroup Q₂)) : ↑((Q₁.orthogonalGroupProd Q₂) f) = (↑f.1).prodCongr ↑f.2

The orthogonal transformation orthogonalGroupProd Q₁ Q₂ f is the product of the two underlying linear automorphisms.

theorem QuadraticMap.orthogonalGroupProd_injective {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {N : Type u_4} [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) : Function.Injective ⇑(Q₁.orthogonalGroupProd Q₂)

The orthogonal sum of orthogonal groups embeds into the orthogonal group of the orthogonal sum.

theorem QuadraticMap.mem_range_orthogonalGroupProd_iff {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {N : Type u_4} [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) {g : ↥(TauCeti.QuadraticMap.orthogonalGroup (Q₁.prod Q₂))} : g ∈ (Q₁.orthogonalGroupProd Q₂).range ↔ (∀ (m₁ : M₁), (↑g (m₁, 0)).2 = 0) ∧ ∀ (m₂ : M₂), (↑g (0, m₂)).1 = 0

The image of the orthogonal sum of orthogonal groups. An orthogonal transformation g of Q₁.prod Q₂ is an orthogonal sum f₁ ⊕ f₂ of orthogonal transformations of Q₁ and Q₂ exactly when it preserves both summands, that is, maps M₁ × 0 into M₁ × 0 and 0 × M₂ into 0 × M₂.

@[simp]

theorem QuadraticMap.det_orthogonalGroupProd {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {N : Type u_4} [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) [Module.Free R M₁] [Module.Finite R M₁] [Module.Free R M₂] [Module.Finite R M₂] (f : ↥(TauCeti.QuadraticMap.orthogonalGroup Q₁) × ↥(TauCeti.QuadraticMap.orthogonalGroup Q₂)) : LinearEquiv.det ↑((Q₁.orthogonalGroupProd Q₂) f) = LinearEquiv.det ↑f.1 * LinearEquiv.det ↑f.2

The determinant of an orthogonal sum of orthogonal transformations is the product of their determinants.

def QuadraticMap.specialOrthogonalGroupProd {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {N : Type u_4} [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) [Module.Free R M₁] [Module.Finite R M₁] [Module.Free R M₂] [Module.Finite R M₂] : ↥(TauCeti.QuadraticMap.specialOrthogonalGroup Q₁) × ↥(TauCeti.QuadraticMap.specialOrthogonalGroup Q₂) →* ↥(TauCeti.QuadraticMap.specialOrthogonalGroup (Q₁.prod Q₂))

Combine special orthogonal transformations of two finite free quadratic maps with a common codomain into a special orthogonal transformation of their product.

theorem QuadraticMap.coe_specialOrthogonalGroupProd {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {N : Type u_4} [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) [Module.Free R M₁] [Module.Finite R M₁] [Module.Free R M₂] [Module.Finite R M₂] (f : ↥(TauCeti.QuadraticMap.specialOrthogonalGroup Q₁) × ↥(TauCeti.QuadraticMap.specialOrthogonalGroup Q₂)) : ↑((Q₁.specialOrthogonalGroupProd Q₂) f) = (↑f.1).prodCongr ↑f.2

The special orthogonal transformation specialOrthogonalGroupProd Q₁ Q₂ f is the product of the two underlying linear automorphisms.

@[simp]

theorem QuadraticMap.specialOrthogonalGroupProd_apply {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {N : Type u_4} [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) [Module.Free R M₁] [Module.Finite R M₁] [Module.Free R M₂] [Module.Finite R M₂] (fg : ↥(TauCeti.QuadraticMap.specialOrthogonalGroup Q₁) × ↥(TauCeti.QuadraticMap.specialOrthogonalGroup Q₂)) (x : M₁ × M₂) : ↑((Q₁.specialOrthogonalGroupProd Q₂) fg) x = (↑fg.1 x.1, ↑fg.2 x.2)

The product of two special orthogonal transformations acts componentwise.

theorem QuadraticMap.specialOrthogonalGroupProd_injective {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {N : Type u_4} [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) [Module.Free R M₁] [Module.Finite R M₁] [Module.Free R M₂] [Module.Finite R M₂] : Function.Injective ⇑(Q₁.specialOrthogonalGroupProd Q₂)

The orthogonal sum of special orthogonal groups embeds into the special orthogonal group of the orthogonal sum.

theorem QuadraticMap.mem_range_specialOrthogonalGroupProd_iff {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {N : Type u_4} [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) [Module.Free R M₁] [Module.Finite R M₁] [Module.Free R M₂] [Module.Finite R M₂] {g : ↥(TauCeti.QuadraticMap.specialOrthogonalGroup (Q₁.prod Q₂))} : g ∈ (Q₁.specialOrthogonalGroupProd Q₂).range ↔ (∀ (m₁ : M₁), (↑g (m₁, 0)).2 = 0) ∧ (∀ (m₂ : M₂), (↑g (0, m₂)).1 = 0) ∧ LinearMap.det (LinearMap.fst R M₁ M₂ ∘ₗ ↑↑g ∘ₗ LinearMap.inl R M₁ M₂) = 1 ∧ LinearMap.det (LinearMap.snd R M₁ M₂ ∘ₗ ↑↑g ∘ₗ LinearMap.inr R M₁ M₂) = 1

The image of the orthogonal sum of special orthogonal groups. A special orthogonal transformation g of Q₁.prod Q₂ is an orthogonal sum f₁ ⊕ f₂ of special orthogonal transformations of Q₁ and Q₂ exactly when it preserves both summands and both of its diagonal blocks M₁ → M₁ and M₂ → M₂ have determinant one. Preserving the summands alone does not suffice, since f₁ ⊕ f₂ with det f₁ = det f₂ = -1 is special orthogonal.

theorem QuadraticMap.orthogonalGroupProd_reflectionOrthogonal_one {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [CommRing R] [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) (v : M₁) [Invertible (Q₁ v)] : (orthogonalGroupProd Q₁ Q₂) (TauCeti.QuadraticMap.reflectionOrthogonal Q₁ v, 1) = TauCeti.QuadraticMap.reflectionOrthogonal (prod Q₁ Q₂) (v, 0)

The reflection of Q₁.prod Q₂ in a vector (v, 0) of the first summand is the orthogonal sum of the reflection of Q₁ in v with the identity of the second summand.

theorem QuadraticMap.orthogonalGroupProd_one_reflectionOrthogonal {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [CommRing R] [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) (w : M₂) [Invertible (Q₂ w)] : (orthogonalGroupProd Q₁ Q₂) (1, TauCeti.QuadraticMap.reflectionOrthogonal Q₂ w) = TauCeti.QuadraticMap.reflectionOrthogonal (prod Q₁ Q₂) (0, w)

The reflection of Q₁.prod Q₂ in a vector (0, w) of the second summand is the orthogonal sum of the identity of the first summand with the reflection of Q₂ in w.

theorem QuadraticMap.isOrthoᵢ_associated_prod {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {N : Type u_4} [CommRing R] [Invertible 2] [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} {ι₁ : Type u_5} {ι₂ : Type u_6} {v₁ : ι₁ → M₁} {v₂ : ι₂ → M₂} (h₁ : LinearMap.IsOrthoᵢ (associated Q₁) v₁) (h₂ : LinearMap.IsOrthoᵢ (associated Q₂) v₂) : LinearMap.IsOrthoᵢ (associated (Q₁.prod Q₂)) (Sum.elim (fun (i : ι₁) => (v₁ i, 0)) fun (j : ι₂) => (0, v₂ j))

Concatenating a Q₁-orthogonal family of M₁ and a Q₂-orthogonal family of M₂, placed in the two summands, gives a family orthogonal for the orthogonal sum Q₁.prod Q₂.