Conjugating automorphism groups along a linear 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 TauCeti.LinearEquiv.congrAut.

Main definitions

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

def TauCeti.LinearEquiv.congrAut {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [Semiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] (e : M₁ ≃ₗ[R] M₂) : (M₁ ≃ₗ[R] M₁) ≃* M₂ ≃ₗ[R] M₂

Conjugation by a linear equivalence e : M₁ ≃ₗ[R] 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 TauCeti.LinearEquiv.congrAut_apply {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [Semiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] (e : M₁ ≃ₗ[R] M₂) (f : M₁ ≃ₗ[R] M₁) (m : M₂) : ((congrAut e) f) m = e (f (e.symm m))

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

@[simp]

theorem TauCeti.LinearEquiv.congrAut_symm_apply {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [Semiring R] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] (e : M₁ ≃ₗ[R] M₂) (g : M₂ ≃ₗ[R] M₂) (m : M₁) : ((congrAut e).symm g) m = e.symm (g (e m))

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