Transporting and decomposing the center of an algebra

Constructions on Subalgebra.center that Mathlib states only for Subring.center, or only as an equality of subalgebras, and that are needed whenever a structure theorem presents an algebra up to an algebra equivalence, together with the criterion for a commutative algebra to be central and the ring of scalars a central subalgebra provides.

• TauCeti.centerCongr transports the center along an algebra equivalence. It is the Subalgebra counterpart of Mathlib's Subring.centerCongr, which sees only the ring structure and therefore cannot record R-linearity.
• TauCeti.centerPiAlgEquiv splits the center of a product of algebras as the product of the centers, upgrading Mathlib's Subalgebra.center_pi from an equality of subalgebras of Π i, S i to an algebra equivalence with Π i, Subalgebra.center R (S i).
• TauCeti.centerAlgEquivOfIsCentral identifies the center of a central algebra with the base field, so that its dimension is one (TauCeti.finrank_center_of_isCentral).
• TauCeti.isCentral_iff_surjective_algebraMap records that a commutative algebra is central exactly when its structure map is surjective, the precise sense in which centrality is a strong condition on a field extension.
• Subalgebra.centralSubalgebraAlgebra makes a subalgebra of the center into a ring of scalars for the ambient algebra, so that finiteness and integrality over it can be stated. Its structure map and action are Subalgebra.centralSubalgebraAlgebra_algebraMap_apply and Subalgebra.centralSubalgebraAlgebra_smul_def, and Subalgebra.isScalarTower_centralSubalgebraAlgebra records that the base ring, the subalgebra and the ambient algebra form a scalar tower.
• Subalgebra.centerAlgebra gives the whole center its canonical scalar action by inclusion. Subalgebra.isScalarTower_centerAlgebra records compatibility with the original base action, and Subalgebra.centerAlgebraIsCentral records that the resulting algebra is central. Subalgebra.finite_centerAlgebra_of_finite transfers module finiteness from the original base ring to the center. Subalgebra.finite_over_center_of_finite transfers module finiteness from a central subalgebra to the center. Subalgebra.finite_center_of_isNoetherian makes the center finite over that subalgebra when the ambient algebra is Noetherian as a module; together with Subalgebra.isNoetherianRing_center_of_finite, this supplies a Noetherian center for applications of the generalized Krull intersection theorem.

@[instance_reducible]

instance Subalgebra.centerAlgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] : Algebra (↥(center R A)) A

The center of an algebra acts on the algebra by its inclusion.

Equations

• Subalgebra.centerAlgebra = (Subalgebra.center R A).val.toAlgebra' ⋯

@[simp]

theorem Subalgebra.centerAlgebra_algebraMap_apply {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (z : ↥(center R A)) : (algebraMap (↥(center R A)) A) z = ↑z

The structure map from the center to an algebra is inclusion.

theorem Subalgebra.centerAlgebra_algebraMap {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] : algebraMap (↥(center R A)) A = (center R A).val.toRingHom

The structure map from the center is the inclusion homomorphism.

theorem Subalgebra.isScalarTower_centerAlgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] : IsScalarTower R (↥(center R A)) A

The original base ring, the center, and the ambient algebra form a scalar tower for the canonical action of the center by inclusion.

instance Subalgebra.centerAlgebraIsCentral {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] : Algebra.IsCentral (↥(center R A)) A

Every algebra is central when regarded as an algebra over its full center.

theorem Subalgebra.finite_centerAlgebra_of_finite {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] [Module.Finite R A] : Module.Finite (↥(center R A)) A

An algebra finite as a module over its original base ring remains finite as a module over its center.

@[reducible, inline]

abbrev Subalgebra.centralSubalgebraAlgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R ↥(center R A)) : Algebra (↥S) A

A subalgebra of the center of an algebra acts on the ambient algebra by multiplication.

Equations

• S.centralSubalgebraAlgebra = ((Subalgebra.center R A).val.comp S.val).toAlgebra' ⋯

@[simp]

theorem Subalgebra.centralSubalgebraAlgebra_algebraMap_apply {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R ↥(center R A)) (s : ↥S) : (algebraMap (↥S) A) s = ↑↑s

The structure map of Subalgebra.centralSubalgebraAlgebra is the inclusion of S into the ambient algebra.

@[simp]

theorem Subalgebra.centralSubalgebraAlgebra_smul_def {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R ↥(center R A)) (s : ↥S) (a : A) : s • a = ↑↑s * a

Subalgebra.centralSubalgebraAlgebra makes S act by multiplication in the ambient algebra.

theorem Subalgebra.isScalarTower_centralSubalgebraAlgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R ↥(center R A)) : IsScalarTower R (↥S) A

R, a subalgebra S of the center, and the ambient algebra form a scalar tower: the two actions of R on the ambient algebra agree because S acts by multiplication.

@[instance_reducible]

def Subalgebra.finiteOverCenterAlgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R ↥(center R A)) : Algebra (↥S) A

The local algebra structure on the ambient algebra for the finiteness transfer.

Equations

• S.finiteOverCenterAlgebra = S.centralSubalgebraAlgebra

@[instance_reducible]

def Subalgebra.finiteOverCenterCenterAlgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R ↥(center R A)) : Algebra ↥S ↥(center R A)

The local algebra structure on the center for the finiteness transfer.

Equations

• S.finiteOverCenterCenterAlgebra = S.val.toAlgebra

theorem Subalgebra.finite_over_center_of_finite {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R ↥(center R A)) [Module.Finite (↥S) A] : Module.Finite (↥(center R A)) A

Finiteness over a central subalgebra implies finiteness over the whole center.

@[instance_reducible]

def Subalgebra.finiteOverCentralSubalgebraAlgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R ↥(center R A)) : Algebra (↥S) A

The local algebra structure on the ambient algebra for the Noetherian transfer.

Equations

• S.finiteOverCentralSubalgebraAlgebra = S.centralSubalgebraAlgebra

@[instance_reducible]

def Subalgebra.finiteOverCentralSubalgebraCenterAlgebra {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R ↥(center R A)) : Algebra ↥S ↥(center R A)

The local algebra structure on the center for the Noetherian transfer.

Equations

• S.finiteOverCentralSubalgebraCenterAlgebra = S.val.toAlgebra

theorem Subalgebra.finite_center_of_isNoetherian {R : Type u_1} {A : Type u_2} [CommSemiring R] [Semiring A] [Algebra R A] (S : Subalgebra R ↥(center R A)) [IsNoetherian (↥S) A] : Module.Finite ↥S ↥(center R A)

If an algebra is Noetherian as a module over a central subalgebra, its center is finite over that subalgebra.

@[instance_reducible]

def Subalgebra.noetherianCenterAlgebra {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R ↥(center R A)) : Algebra (↥S) A

The local algebra structure on the ambient algebra for the Noetherian-center theorem.

Equations

• S.noetherianCenterAlgebra = S.centralSubalgebraAlgebra

@[instance_reducible]

def Subalgebra.noetherianCenterCenterAlgebra {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R ↥(center R A)) : Algebra ↥S ↥(center R A)

The local algebra structure on the center for the Noetherian-center theorem.

Equations

• S.noetherianCenterCenterAlgebra = S.val.toAlgebra

theorem Subalgebra.isNoetherianRing_center_of_finite {R : Type u_1} {A : Type u_2} [CommRing R] [Ring A] [Algebra R A] (S : Subalgebra R ↥(center R A)) [IsNoetherianRing ↥S] [Module.Finite (↥S) A] : IsNoetherianRing ↥(center R A)

A finite algebra over a Noetherian central subalgebra has Noetherian center.

theorem TauCeti.map_center_eq_center {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (e : A ≃ₐ[R] B) : Subalgebra.map (↑e) (Subalgebra.center R A) = Subalgebra.center R B

An algebra equivalence carries the center onto the center.

def TauCeti.centerCongr {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (e : A ≃ₐ[R] B) : ↥(Subalgebra.center R A) ≃ₐ[R] ↥(Subalgebra.center R B)

The center of an algebra, transported along an algebra equivalence.

Equations

• TauCeti.centerCongr e = (e.subalgebraMap (Subalgebra.center R A)).trans ((Subalgebra.map (↑e) (Subalgebra.center R A)).equivOfEq (Subalgebra.center R B) ⋯)

@[simp]

theorem TauCeti.centerCongr_apply_coe {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (e : A ≃ₐ[R] B) (x : ↥(Subalgebra.center R A)) : ↑((centerCongr e) x) = e ↑x

@[simp]

theorem TauCeti.centerCongr_symm_apply_coe {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] (e : A ≃ₐ[R] B) (y : ↥(Subalgebra.center R B)) : ↑((centerCongr e).symm y) = e.symm ↑y

The inverse of centerCongr e transports the center back along e.symm.

def TauCeti.centerPiAlgEquiv {R : Type u_1} [CommSemiring R] {ι : Type u_4} {S : ι → Type u_5} [(i : ι) → Semiring (S i)] [(i : ι) → Algebra R (S i)] : ↥(Subalgebra.center R ((i : ι) → S i)) ≃ₐ[R] (i : ι) → ↥(Subalgebra.center R (S i))

The center of a product of algebras is the product of their centers.

Equations

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

@[simp]

theorem TauCeti.centerPiAlgEquiv_apply_coe {R : Type u_1} [CommSemiring R] {ι : Type u_4} {S : ι → Type u_5} [(i : ι) → Semiring (S i)] [(i : ι) → Algebra R (S i)] (x : ↥(Subalgebra.center R ((i : ι) → S i))) (i : ι) : ↑(centerPiAlgEquiv x i) = ↑x i

@[simp]

theorem TauCeti.centerPiAlgEquiv_symm_apply_coe {R : Type u_1} [CommSemiring R] {ι : Type u_4} {S : ι → Type u_5} [(i : ι) → Semiring (S i)] [(i : ι) → Algebra R (S i)] (y : (i : ι) → ↥(Subalgebra.center R (S i))) (i : ι) : ↑(centerPiAlgEquiv.symm y) i = ↑(y i)

The inverse of centerPiAlgEquiv assembles a tuple of central elements componentwise.

noncomputable def TauCeti.centerAlgEquivOfIsCentral (K : Type u_4) (D : Type u_5) [Field K] [Semiring D] [Nontrivial D] [Algebra K D] [Algebra.IsCentral K D] : ↥(Subalgebra.center K D) ≃ₐ[K] K

The center of a central algebra is the base field.

Equations

• TauCeti.centerAlgEquivOfIsCentral K D = ((Subalgebra.center K D).equivOfEq ⊥ ⋯).trans (Algebra.botEquiv K D)

@[simp]

theorem TauCeti.coe_centerAlgEquivOfIsCentral_symm (K : Type u_4) (D : Type u_5) [Field K] [Semiring D] [Nontrivial D] [Algebra K D] [Algebra.IsCentral K D] (r : K) : ↑((centerAlgEquivOfIsCentral K D).symm r) = (algebraMap K D) r

The inverse of centerAlgEquivOfIsCentral is the structure map of the algebra.

@[simp]

theorem TauCeti.algebraMap_centerAlgEquivOfIsCentral (K : Type u_4) (D : Type u_5) [Field K] [Semiring D] [Nontrivial D] [Algebra K D] [Algebra.IsCentral K D] (x : ↥(Subalgebra.center K D)) : (algebraMap K D) ((centerAlgEquivOfIsCentral K D) x) = ↑x

centerAlgEquivOfIsCentral sends a central element to the scalar it is the image of.

@[simp]

theorem TauCeti.finrank_center_of_isCentral (K : Type u_4) (D : Type u_5) [Field K] [Semiring D] [Nontrivial D] [Algebra K D] [Algebra.IsCentral K D] : Module.finrank K ↥(Subalgebra.center K D) = 1

A central algebra has a one-dimensional center.

theorem TauCeti.isCentral_iff_surjective_algebraMap (K : Type u_4) (D : Type u_5) [CommSemiring K] [CommSemiring D] [Algebra K D] : Algebra.IsCentral K D ↔ Function.Surjective ⇑(algebraMap K D)

A commutative K-algebra is central over K exactly when its structure map is surjective: the center of a commutative algebra is all of it, so demanding that the center be the image of K demands that everything be in the image of K.

This is the precise sense in which centrality is a strong condition on a field extension: L / K is central only when L = K.