Products in the general linear group

This file defines the componentwise product of two linear automorphisms and proves its basic compatibility with the group operations.

Main declarations

• LinearMap.GeneralLinearGroup.prodMap: the componentwise product of two linear automorphisms.
• LinearMap.GeneralLinearGroup.prodMap_apply: the product automorphism acts componentwise.

def LinearMap.GeneralLinearGroup.prodMap {K : Type u} {V : Type v} {W : Type w} [Semiring K] [AddCommMonoid V] [Module K V] [AddCommMonoid W] [Module K W] (g : GeneralLinearGroup K V) (h : GeneralLinearGroup K W) : GeneralLinearGroup K (V × W)

The product map of two linear automorphisms, acting componentwise on the product module.

Equations

• g.prodMap h = LinearMap.GeneralLinearGroup.ofLinearEquiv (g.toLinearEquiv.prodCongr h.toLinearEquiv)

theorem LinearMap.GeneralLinearGroup.coe_prodMap {K : Type u} {V : Type v} {W : Type w} [Semiring K] [AddCommMonoid V] [Module K V] [AddCommMonoid W] [Module K W] (g : GeneralLinearGroup K V) (h : GeneralLinearGroup K W) : ↑(g.prodMap h) = (↑g).prodMap ↑h

The endomorphism underlying a product-map automorphism is LinearMap.prodMap.

@[simp]

theorem LinearMap.GeneralLinearGroup.prodMap_apply {K : Type u} {V : Type v} {W : Type w} [Semiring K] [AddCommMonoid V] [Module K V] [AddCommMonoid W] [Module K W] (g : GeneralLinearGroup K V) (h : GeneralLinearGroup K W) (x : V × W) : ↑(g.prodMap h) x = (↑g x.1, ↑h x.2)

A product-map automorphism acts componentwise.

@[simp]

theorem LinearMap.GeneralLinearGroup.prodMap_mul {K : Type u} {V : Type v} {W : Type w} [Semiring K] [AddCommMonoid V] [Module K V] [AddCommMonoid W] [Module K W] (g₁ g₂ : GeneralLinearGroup K V) (h₁ h₂ : GeneralLinearGroup K W) : (g₁ * g₂).prodMap (h₁ * h₂) = g₁.prodMap h₁ * g₂.prodMap h₂

Product maps preserve multiplication.

@[simp]

theorem LinearMap.GeneralLinearGroup.prodMap_one {K : Type u} {V : Type v} {W : Type w} [Semiring K] [AddCommMonoid V] [Module K V] [AddCommMonoid W] [Module K W] : prodMap 1 1 = 1

The product map of two identity automorphisms is the identity.

@[simp]

theorem LinearMap.GeneralLinearGroup.prodMap_inv {K : Type u} {V : Type v} {W : Type w} [Semiring K] [AddCommMonoid V] [Module K V] [AddCommMonoid W] [Module K W] (g : GeneralLinearGroup K V) (h : GeneralLinearGroup K W) : g⁻¹.prodMap h⁻¹ = (g.prodMap h)⁻¹

Product maps preserve inverses.