Product linear maps

Mathlib builds the product e₁.prodCongr e₂ of two linear equivalences, acting on M₁ × M₂ componentwise. This file identifies which automorphisms of M₁ × M₂ arise this way, records the determinant of such a product, and records that scalar multiplication on a product of complex modules is the product map of the two scalar multiplications.

The characterization needs only containment: an automorphism g of M₁ × M₂ that maps M₁ × 0 into M₁ × 0 and 0 × M₂ into 0 × M₂ already acts componentwise, and each component is then bijective because g is. No finiteness is used, so no separate hypothesis on g⁻¹ is needed. This is what identifies the image of the orthogonal group of an orthogonal sum of quadratic forms with the subgroup preserving both summands.

Main results

• LinearEquiv.prodCongr_inj: products of linear equivalences are equal exactly when their factors are.
• LinearEquiv.exists_prodCongr_eq_iff: an automorphism of M₁ × M₂ is e₁.prodCongr e₂ for automorphisms e₁ of M₁ and e₂ of M₂ exactly when it maps each factor into itself.
• LinearEquiv.det_prodCongr: det (e₁.prodCongr e₂) = det e₁ * det e₂ for finite free modules; this is LinearMap.det_prodMap for linear equivalences.
• TauCeti.LinearMap.lsmul_restrictScalars_prodMap: multiplication by a scalar on a product of complex modules is the product map of the two multiplications.

@[simp]

theorem LinearEquiv.prodCongr_inj {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [Semiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] {M₃ : Type u_4} {M₄ : Type u_5} [AddCommMonoid M₃] [Module R M₃] [AddCommMonoid M₄] [Module R M₄] {e₁ e₁' : M₁ ≃ₗ[R] M₃} {e₂ e₂' : M₂ ≃ₗ[R] M₄} : e₁.prodCongr e₂ = e₁'.prodCongr e₂' ↔ e₁ = e₁' ∧ e₂ = e₂'

Products of linear equivalences are equal exactly when their factors are.

theorem LinearEquiv.exists_prodCongr_eq_iff {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [Semiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] {g : (M₁ × M₂) ≃ₗ[R] M₁ × M₂} : (∃ (e₁ : M₁ ≃ₗ[R] M₁) (e₂ : M₂ ≃ₗ[R] M₂), e₁.prodCongr e₂ = g) ↔ (∀ (m₁ : M₁), (g (m₁, 0)).2 = 0) ∧ ∀ (m₂ : M₂), (g (0, m₂)).1 = 0

A linear automorphism of M₁ × M₂ is a product e₁.prodCongr e₂ of automorphisms of the factors exactly when it maps M₁ × 0 into M₁ × 0 and 0 × M₂ into 0 × M₂.

@[simp]

theorem LinearEquiv.det_prodCongr {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [CommRing R] [AddCommGroup M₁] [Module R M₁] [AddCommGroup M₂] [Module R M₂] [Module.Free R M₁] [Module.Finite R M₁] [Module.Free R M₂] [Module.Finite R M₂] (e₁ : M₁ ≃ₗ[R] M₁) (e₂ : M₂ ≃ₗ[R] M₂) : LinearEquiv.det (e₁.prodCongr e₂) = LinearEquiv.det e₁ * LinearEquiv.det e₂

The determinant of a product of linear automorphisms of finite free modules is the product of their determinants.

theorem TauCeti.LinearMap.lsmul_restrictScalars_prodMap {E : Type u_1} {E' : Type u_2} [AddCommGroup E] [Module ℝ E] [Module ℂ E] [IsScalarTower ℝ ℂ E] [AddCommGroup E'] [Module ℝ E'] [Module ℂ E'] [IsScalarTower ℝ ℂ E'] (c : ℂ) : ↑ℝ ((LinearMap.lsmul ℂ (E × E')) c) = (↑ℝ ((LinearMap.lsmul ℂ E) c)).prodMap (↑ℝ ((LinearMap.lsmul ℂ E') c))

Multiplication by a scalar on a product of complex modules is carried out blockwise. Read as a real-linear map, multiplication by c on E × E' is the LinearMap.prodMap of the multiplications by c on the two factors.