Conjugating automorphism groups along a semilinear equivalence

Mathlib conjugates general linear groups with LinearMap.GeneralLinearGroup.congrLinearEquiv : GL R₁ M₁ ≃* GL R₂ M₂, and identifies GL R M with the automorphisms M ≃ₗ[R] M through LinearMap.GeneralLinearGroup.generalLinearEquiv. Groups of linear automorphisms cut out by a structure they preserve — an orthogonal group, an isometry group — are subgroups of M ≃ₗ[R] M rather than of GL R M, so what they need is the composite of those two, which this file records as LinearEquiv.autCongr.

Conjugation needs no more than a semilinear equivalence, which is the generality congrLinearEquiv already supplies: e : M₁ ≃ₛₗ[σ₁₂] M₂ carries R₁-automorphisms of M₁ to R₂-automorphisms of M₂, the scalars travelling along σ₁₂. The two inverse-pair assumptions give a round trip on each scalar ring — σ₂₁ ∘ σ₁₂ is the identity on R₁ and σ₁₂ ∘ σ₂₁ the identity on R₂ — and it is the latter that makes the conjugate R₂-linear.

Main definitions

• LinearEquiv.autCongr: conjugation by e : M₁ ≃ₛₗ[σ₁₂] M₂, as an isomorphism (M₁ ≃ₗ[R₁] M₁) ≃* (M₂ ≃ₗ[R₂] M₂).

Main statements

• LinearEquiv.autCongr_apply and LinearEquiv.autCongr_symm_apply: conjugation and its inverse as equalities of linear equivalences, for consumers that read the conjugate as a map rather than at a point. The pointwise autCongr_apply_apply and autCongr_symm_apply_apply are the same facts evaluated at m.

def LinearEquiv.autCongr {R₁ : Type u_1} {R₂ : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [Semiring R₁] [Semiring R₂] [AddCommMonoid M₁] [Module R₁ M₁] [AddCommMonoid M₂] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (e : M₁ ≃ₛₗ[σ₁₂] M₂) : (M₁ ≃ₗ[R₁] M₁) ≃* M₂ ≃ₗ[R₂] M₂

Conjugation by a semilinear equivalence e : M₁ ≃ₛₗ[σ₁₂] M₂, as an isomorphism of automorphism groups: Mathlib's LinearMap.GeneralLinearGroup.congrLinearEquiv read through LinearMap.GeneralLinearGroup.generalLinearEquiv.

The two evaluation lemmas below are its characteristic API.

Equations

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

@[simp]

theorem LinearEquiv.autCongr_apply_apply {R₁ : Type u_1} {R₂ : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [Semiring R₁] [Semiring R₂] [AddCommMonoid M₁] [Module R₁ M₁] [AddCommMonoid M₂] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (e : M₁ ≃ₛₗ[σ₁₂] M₂) (f : M₁ ≃ₗ[R₁] M₁) (m : M₂) : (e.autCongr f) m = e (f (e.symm m))

Conjugating f by e sends m to e (f (e.symm m)).

@[simp]

theorem LinearEquiv.autCongr_symm_apply_apply {R₁ : Type u_1} {R₂ : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [Semiring R₁] [Semiring R₂] [AddCommMonoid M₁] [Module R₁ M₁] [AddCommMonoid M₂] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (e : M₁ ≃ₛₗ[σ₁₂] M₂) (g : M₂ ≃ₗ[R₂] M₂) (m : M₁) : (e.autCongr.symm g) m = e.symm (g (e m))

Inverse conjugation by e sends m to e.symm (g (e m)).

theorem LinearEquiv.autCongr_apply {R₁ : Type u_1} {R₂ : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [Semiring R₁] [Semiring R₂] [AddCommMonoid M₁] [Module R₁ M₁] [AddCommMonoid M₂] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (e : M₁ ≃ₛₗ[σ₁₂] M₂) (f : M₁ ≃ₗ[R₁] M₁) : e.autCongr f = (e.symm.trans f).trans e

Conjugation by e, as an equality of linear equivalences: autCongr e f is f precomposed with e.symm and postcomposed with e. Structural consumers — determinants, traces, anything reading the conjugate as a map rather than at a point — want this form.

theorem LinearEquiv.autCongr_symm_apply {R₁ : Type u_1} {R₂ : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [Semiring R₁] [Semiring R₂] [AddCommMonoid M₁] [Module R₁ M₁] [AddCommMonoid M₂] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (e : M₁ ≃ₛₗ[σ₁₂] M₂) (g : M₂ ≃ₗ[R₂] M₂) : e.autCongr.symm g = (e.trans g).trans e.symm

Inverse conjugation by e, as an equality of linear equivalences: (autCongr e).symm g is g precomposed with e and postcomposed with e.symm.