Documentation

TauCeti.Algebra.HopfAlgebra.HopfIdeal.CentralExtension

The central augmentation ideal as an extended ideal #

The ideal of a Hopf algebra generated by its central elements of augmentation zero is extended from an ideal of its commutative center. This identifies its powers with the powers of a commutative ideal acting on the Hopf algebra. In characteristic p, the enveloping algebra of a finite-dimensional Lie algebra is module-finite over a central subalgebra. This identity is the bridge needed to apply the generalized Krull intersection theorem to its central augmentation ideal.

The use of an extended ideal follows G. Hochschild, An Addition to Ado's Theorem, Proc. Amer. Math. Soc. 17 (1966), 531–533.

source
noncomputable def TauCeti.HopfIdeal.centralAugmentationCenterIdeal (K : Type u) (H : Type v) [CommRing K] [Ring H] [HopfAlgebra K H] :
Ideal ↥(Subalgebra.center K H)

The ideal of the center consisting of elements with zero augmentation.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.HopfIdeal.mem_centralAugmentationCenterIdeal (K : Type u) (H : Type v) [CommRing K] [Ring H] [HopfAlgebra K H] (z : ↥(Subalgebra.center K H)) :
    z ∈ centralAugmentationCenterIdeal K H ↔ CoalgebraStruct.counit ↑z = 0

    Membership in the central augmentation ideal of the center is vanishing of the counit.

    source
    @[simp]
    theorem TauCeti.HopfIdeal.map_centralAugmentationCenterIdeal (K : Type u) (H : Type v) [CommRing K] [Ring H] [HopfAlgebra K H] :
    Ideal.map (↑(Subalgebra.center K H).val) (centralAugmentationCenterIdeal K H) = centralAugmentationIdeal K H

    The full central augmentation ideal is extended from the corresponding ideal of the commutative center.

    source
    theorem TauCeti.HopfIdeal.mem_iInf_centralAugmentationIdeal_pow_iff (K : Type u) (H : Type v) [CommRing K] [Ring H] [HopfAlgebra K H] [IsNoetherianRing ↥(Subalgebra.center K H)] [hFinite : Module.Finite (↥(Subalgebra.center K H)) H] (x : H) :
    x ∈ ⨅ (n : ℕ), centralAugmentationIdeal K H ^ n ↔ ∃ z ∈ centralAugmentationCenterIdeal K H, ↑z * x = x

    Krull intersection for the central augmentation ideal of a Hopf algebra finite over its Noetherian center. An element of all powers is fixed by a central scalar of augmentation zero.

    source
    theorem TauCeti.HopfIdeal.iInf_centralAugmentationIdeal_pow_eq_bot (K : Type u) (H : Type v) [CommRing K] [Ring H] [HopfAlgebra K H] [Nontrivial K] [IsNoetherianRing ↥(Subalgebra.center K H)] [hFinite : Module.Finite (↥(Subalgebra.center K H)) H] [NoZeroDivisors H] :
    ⨅ (n : ℕ), centralAugmentationIdeal K H ^ n = ⊥

    If the Hopf algebra is finite over its Noetherian center, the base ring is nontrivial, and the Hopf algebra has no zero divisors, the central augmentation ideal is separated by its powers.