Documentation

TauCeti.Algebra.Module.Equiv.AutCongr

Conjugating automorphism groups along a semilinear equivalence #

Mathlib conjugates general linear groups with LinearMap.GeneralLinearGroup.congrLinearEquiv : GL R₁ M₁ ≃* GL R₂ M₂, and algebra automorphisms with AlgEquiv.autCongr. 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 same conjugation stated directly on M ≃ₗ[R] M, which this file records as LinearEquiv.autCongr, the linear counterpart of AlgEquiv.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 #

Main statements #

source
def LinearEquiv.autCongr {R₁ : Type u_1} {R₂ : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [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: f is sent to e ∘ f ∘ e.symm. It is the counterpart on M ≃ₗ[R] M of Mathlib's LinearMap.GeneralLinearGroup.congrLinearEquiv on general linear groups.

Instances For
    source
    theorem LinearEquiv.autCongr_apply {R₁ : Type u_1} {R₂ : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [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.

    source
    theorem LinearEquiv.autCongr_symm_apply {R₁ : Type u_1} {R₂ : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [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.

    source
    @[simp]
    theorem LinearEquiv.autCongr_apply_apply {R₁ : Type u_1} {R₂ : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [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)).

    source
    theorem LinearEquiv.autCongr_symm_apply_apply {R₁ : Type u_1} {R₂ : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [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)).

    source
    @[simp]
    theorem LinearEquiv.autCongr_refl (R₁ : Type u_1) (M₁ : Type u_4) [Semiring R₁] [AddCommMonoid M₁] [Module R₁ M₁] :
    (refl R₁ M₁).autCongr = MulEquiv.refl (M₁ ≃ₗ[R₁] M₁)

    Conjugation along the identity is the identity.

    source
    @[simp]
    theorem LinearEquiv.autCongr_symm {R₁ : Type u_1} {R₂ : Type u_2} {M₁ : Type u_4} {M₂ : Type u_5} [Semiring R₁] [Semiring R₂] [AddCommMonoid M₁] [Module R₁ M₁] [AddCommMonoid M₂] [Module R₂ M₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] (e : M₁ ≃ₛₗ[σ₁₂] M₂) :
    e.autCongr.symm = e.symm.autCongr

    The inverse of conjugation by e is conjugation by e.symm.

    source
    @[simp]
    theorem LinearEquiv.autCongr_trans {R : Type u_7} {N₁ : Type u_8} {N₂ : Type u_9} {N₃ : Type u_10} [Semiring R] [AddCommMonoid N₁] [Module R N₁] [AddCommMonoid N₂] [Module R N₂] [AddCommMonoid N₃] [Module R N₃] (e₁₂ : N₁ ≃ₗ[R] N₂) (e₂₃ : N₂ ≃ₗ[R] N₃) :
    e₁₂.autCongr.trans e₂₃.autCongr = (e₁₂ ≪≫ₗ e₂₃).autCongr

    Conjugating by e₁₂ and then by e₂₃ is conjugating by their composite. For semilinear equivalences, see LinearEquiv.autCongr_trans'.

    source
    theorem LinearEquiv.autCongr_trans' {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {M₁ : Type u_4} {M₂ : Type u_5} {M₃ : Type u_6} [Semiring R₁] [Semiring R₂] [Semiring R₃] [AddCommMonoid M₁] [Module R₁ M₁] [AddCommMonoid M₂] [Module R₂ M₂] [AddCommMonoid M₃] [Module R₃ M₃] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [RingHomInvPair σ₁₂ σ₂₁] [RingHomInvPair σ₂₁ σ₁₂] {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [RingHomInvPair σ₂₃ σ₃₂] [RingHomInvPair σ₃₂ σ₂₃] [RingHomInvPair σ₁₃ σ₃₁] [RingHomInvPair σ₃₁ σ₁₃] [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] (e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂) (e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃) :
    e₁₂.autCongr.trans e₂₃.autCongr = (e₁₂.trans e₂₃).autCongr

    Conjugating by e₁₂ and then by e₂₃ is conjugating by their composite, for semilinear equivalences. Not a simp lemma, as σ₁₃ and σ₃₁ cannot be inferred from the left-hand side; LinearEquiv.autCongr_trans is the simp form for linear equivalences.