Documentation

TauCeti.Algebra.Subalgebra.Centralizer

A centralizer as an algebra over a commutative subalgebra #

If S is a commutative subalgebra of A, its centralizer C is naturally an S-algebra. Subalgebras of C over S correspond to subalgebras of A over the original base containing S and contained in C. The correspondence preserves the underlying elements and records the degree multiplication in a field tower.

This permits enlargement of subfields inside a division algebra: an extension constructed in the centralizer is transported back to a subalgebra of the original algebra containing the original subfield.

References #

source
@[instance_reducible]
instance Subalgebra.centralizerAlgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) [IsMulCommutative ↥S] :
Algebra ↥S ↥(centralizer R ↑S)

A commutative subalgebra acts on its centralizer by multiplication.

source
@[simp]
theorem Subalgebra.coe_algebraMap_centralizer {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) [IsMulCommutative ↥S] (s : ↥S) :
↑((algebraMap ↥S ↥(centralizer R ↑S)) s) = ↑s

The structure map from a commutative subalgebra to its centralizer is inclusion.

source
@[simp]
theorem Subalgebra.coe_smul_centralizer {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) [IsMulCommutative ↥S] (s : ↥S) (c : ↥(centralizer R ↑S)) :
↑(s • c) = ↑s * ↑c

The scalar action on the centralizer is multiplication in the ambient algebra.

source
instance Subalgebra.isScalarTower_centralizerAlgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) [IsMulCommutative ↥S] :
IsScalarTower R ↥S ↥(centralizer R ↑S)

The centralizer's action by the commutative subalgebra extends its original base action.

source
def Subalgebra.centralizerSubalgebraOrderIso {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) [IsMulCommutative ↥S] :
Subalgebra ↥S ↥(centralizer R ↑S) ≃o { T : Subalgebra R A // S ≤ T ∧ T ≤ centralizer R ↑S }

Subalgebras of a centralizer over its commutative scalar subalgebra correspond to ambient subalgebras lying between the scalar subalgebra and its centralizer.

Instances For
    source
    theorem Subalgebra.centralizerSubalgebraOrderIso_apply {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) [IsMulCommutative ↥S] (T : Subalgebra ↥S ↥(centralizer R ↑S)) :
    ↑(S.centralizerSubalgebraOrderIso T) = map (centralizer R ↑S).val (restrictScalars R T)

    The forward correspondence restricts scalars and includes into the ambient algebra.

    source
    @[simp]
    theorem Subalgebra.mem_centralizerSubalgebraOrderIso {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) [IsMulCommutative ↥S] (T : Subalgebra ↥S ↥(centralizer R ↑S)) (c : ↥(centralizer R ↑S)) :
    ↑c ∈ ↑(S.centralizerSubalgebraOrderIso T) ↔ c ∈ T

    An element of the centralizer belongs to the transported subalgebra exactly when it belongs to the original subalgebra over S.

    source
    @[simp]
    theorem Subalgebra.mem_centralizerSubalgebraOrderIso_symm {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) [IsMulCommutative ↥S] (T : { T : Subalgebra R A // S ≤ T ∧ T ≤ centralizer R ↑S }) (c : ↥(centralizer R ↑S)) :
    c ∈ S.centralizerSubalgebraOrderIso.symm T ↔ ↑c ∈ ↑T

    The inverse correspondence tests ambient membership after including the centralizer.

    source
    @[simp]
    theorem Subalgebra.centralizerSubalgebraOrderIso_bot {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) [IsMulCommutative ↥S] :
    ↑(S.centralizerSubalgebraOrderIso ⊥) = S

    The scalar subalgebra corresponds to the bottom subalgebra of the centralizer over S.

    source
    @[simp]
    theorem Subalgebra.centralizerSubalgebraOrderIso_top {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) [IsMulCommutative ↥S] :
    ↑(S.centralizerSubalgebraOrderIso ⊤) = centralizer R ↑S

    The whole centralizer corresponds to the top subalgebra over S.

    source
    theorem Subalgebra.lt_centralizerSubalgebraOrderIso_iff {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) [IsMulCommutative ↥S] (T : Subalgebra ↥S ↥(centralizer R ↑S)) :
    S < ↑(S.centralizerSubalgebraOrderIso T) ↔ ⊥ < T

    A nontrivial extension inside the centralizer gives a strict enlargement of the original scalar subalgebra inside the ambient algebra.

    source
    theorem Subalgebra.finrank_centralizerSubalgebraOrderIso {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R A) [IsMulCommutative ↥S] [StrongRankCondition R] [StrongRankCondition ↥S] [Module.Free R ↥S] (T : Subalgebra ↥S ↥(centralizer R ↑S)) [Module.Free ↥S ↥T] :
    Module.finrank R ↥↑(S.centralizerSubalgebraOrderIso T) = Module.finrank R ↥S * Module.finrank ↥S ↥T

    The transported subalgebra has the dimension prescribed by the scalar tower. In particular, for subfields this is multiplication of extension degrees.