The augmentation Hopf ideal

The augmentation ideal of a Hopf algebra is the kernel of its counit. The counit is split by the unit, hence surjective, so the kernel Hopf ideal machinery of TauCeti.Algebra.HopfAlgebra.HopfIdeal.Kernel applies directly and no Sweedler-decomposition argument is needed.

This is the fundamental example of a Hopf ideal: the quotient by it is the base ring, and its image under a morphism into a commutative Hopf algebra cuts out the kernel of the induced morphism of affine group schemes (TauCeti.CommHopfAlgCat.kernelHopfIdeal).

Main declarations

• TauCeti.HopfIdeal.augmentation: the augmentation ideal as a Hopf ideal.
• TauCeti.HopfIdeal.mem_augmentation, TauCeti.HopfIdeal.augmentation_toIdeal and TauCeti.HopfIdeal.augmentation_toIdeal_ne_top: characteristic API.
• TauCeti.HopfIdeal.le_augmentation: every Hopf ideal is contained in the augmentation ideal.
• TauCeti.HopfIdeal.centralAugmentation: the central part of the augmentation ideal.
• TauCeti.HopfIdeal.centralAugmentationIdeal: the two-sided ideal generated by that central part, with TauCeti.HopfIdeal.nontrivial_quotient_centralAugmentationIdeal_pow recording that the quotient by each of its positive powers is nonzero.
• AlgHom.apply_eq_counit_of_augmentation_le_ker: an algebra morphism that kills the augmentation ideal is evaluation by the counit, followed by the target's scalar map.
• TauCeti.HopfIdeal.comapOfSurjective_augmentation: the augmentation ideal is preserved by pullback along a surjective bialgebra morphism.
• TauCeti.HopfIdeal.counitBialgEquivOfAugmentationEqBot: a Hopf algebra with zero augmentation ideal is bialgebra-equivalent to its base ring via the counit.

References

Waterhouse, Introduction to Affine Group Schemes, §2.1; Milne, Algebraic Groups, around Proposition 4.1, where the augmentation ideal cuts out the identity section.

noncomputable def TauCeti.HopfIdeal.augmentation (R : Type u) (H : Type v) [CommRing R] [Ring H] [HopfAlgebra R H] : HopfIdeal R H

The augmentation Hopf ideal of a Hopf algebra: the kernel of the counit, which is surjective since the unit splits it (Bialgebra.counit_surjective).

The ring hypotheses come from the kernel Hopf ideal construction, whose coideal condition uses tensor-kernel exactness.

Equations

• TauCeti.HopfIdeal.augmentation R H = TauCeti.HopfIdeal.kerOfSurjective (Bialgebra.counitBialgHom R H) ⋯

theorem TauCeti.HopfIdeal.augmentation_def (R : Type u) (H : Type v) [CommRing R] [Ring H] [HopfAlgebra R H] : augmentation R H = kerOfSurjective (Bialgebra.counitBialgHom R H) ⋯

augmentation is the kernel Hopf ideal of the counit.

@[simp]

theorem TauCeti.HopfIdeal.mem_augmentation (R : Type u) (H : Type v) [CommRing R] [Ring H] [HopfAlgebra R H] {x : H} : x ∈ augmentation R H ↔ CoalgebraStruct.counit x = 0

Membership in the augmentation ideal is vanishing of the counit.

theorem AlgHom.apply_eq_counit_of_augmentation_le_ker {k : Type u} {A : Type v} {B : Type w} [CommRing k] [Ring A] [Ring B] [HopfAlgebra k A] [Algebra k B] (f : A →ₐ[k] B) (hf : (TauCeti.HopfIdeal.augmentation k A).toIdeal ≤ RingHom.ker f) (x : A) : f x = (algebraMap k B) (CoalgebraStruct.counit x)

An algebra morphism that kills the augmentation ideal sends each element to its counit, viewed as a scalar in the target.

@[simp]

theorem TauCeti.HopfIdeal.augmentation_toIdeal (R : Type u) (H : Type v) [CommRing R] [Ring H] [HopfAlgebra R H] : (augmentation R H).toIdeal = RingHom.ker (Bialgebra.counitAlgHom R H)

The underlying ideal of the augmentation Hopf ideal is the kernel of the counit algebra homomorphism.

theorem TauCeti.HopfIdeal.augmentation_toIdeal_ne_top (R : Type u) (H : Type v) [CommRing R] [Ring H] [HopfAlgebra R H] [Nontrivial R] : (augmentation R H).toIdeal ≠ ⊤

Over a nontrivial base ring the augmentation ideal is proper, being the kernel of a ring homomorphism onto R.

noncomputable def TauCeti.HopfIdeal.centralAugmentation (R : Type u) (H : Type v) [CommRing R] [Ring H] [HopfAlgebra R H] : Submodule R H

The central part of the augmentation ideal of a Hopf algebra.

Equations

• TauCeti.HopfIdeal.centralAugmentation R H = Subalgebra.toSubmodule (Subalgebra.center R H) ⊓ Submodule.restrictScalars R (TauCeti.HopfIdeal.augmentation R H).toIdeal

@[simp]

theorem TauCeti.HopfIdeal.mem_centralAugmentation (R : Type u) (H : Type v) [CommRing R] [Ring H] [HopfAlgebra R H] {z : H} : z ∈ centralAugmentation R H ↔ z ∈ Subalgebra.center R H ∧ z ∈ (augmentation R H).toIdeal

Membership in the central augmentation submodule means being both central and augmented.

theorem TauCeti.HopfIdeal.centralAugmentation_le_center (R : Type u) (H : Type v) [CommRing R] [Ring H] [HopfAlgebra R H] : centralAugmentation R H ≤ Subalgebra.toSubmodule (Subalgebra.center R H)

The central augmentation submodule is contained in the centre.

theorem TauCeti.HopfIdeal.centralAugmentation_le_augmentation (R : Type u) (H : Type v) [CommRing R] [Ring H] [HopfAlgebra R H] : centralAugmentation R H ≤ Submodule.restrictScalars R (augmentation R H).toIdeal

The central augmentation submodule is contained in the augmentation ideal.

noncomputable def TauCeti.HopfIdeal.centralAugmentationIdeal (R : Type u) (H : Type v) [CommRing R] [Ring H] [HopfAlgebra R H] : Ideal H

The ideal generated by the central part of the augmentation ideal.

Equations

• TauCeti.HopfIdeal.centralAugmentationIdeal R H = Ideal.span ↑(TauCeti.HopfIdeal.centralAugmentation R H)

@[simp]

theorem TauCeti.HopfIdeal.centralAugmentationIdeal_le_iff (R : Type u) (H : Type v) [CommRing R] [Ring H] [HopfAlgebra R H] {I : Ideal H} : centralAugmentationIdeal R H ≤ I ↔ ↑(centralAugmentation R H) ⊆ ↑I

The universal property of the central augmentation ideal.

theorem TauCeti.HopfIdeal.mem_centralAugmentationIdeal_of_mem_centralAugmentation (R : Type u) (H : Type v) [CommRing R] [Ring H] [HopfAlgebra R H] {z : H} (hz : z ∈ centralAugmentation R H) : z ∈ centralAugmentationIdeal R H

A central element of augmentation zero belongs to the ideal generated by all such elements.

instance TauCeti.HopfIdeal.instIsTwoSidedCentralAugmentationIdeal (R : Type u) (H : Type v) [CommRing R] [Ring H] [HopfAlgebra R H] : (centralAugmentationIdeal R H).IsTwoSided

The ideal generated by the central elements of augmentation zero is two-sided.

theorem TauCeti.HopfIdeal.centralAugmentationIdeal_le_augmentation (R : Type u) (H : Type v) [CommRing R] [Ring H] [HopfAlgebra R H] : centralAugmentationIdeal R H ≤ (augmentation R H).toIdeal

The central augmentation ideal is contained in the augmentation ideal.

theorem TauCeti.HopfIdeal.centralAugmentationIdeal_ne_top (R : Type u) (H : Type v) [CommRing R] [Ring H] [HopfAlgebra R H] [Nontrivial R] : centralAugmentationIdeal R H ≠ ⊤

Over a nontrivial base ring, the central augmentation ideal is proper.

theorem TauCeti.HopfIdeal.nontrivial_quotient_centralAugmentationIdeal_pow (R : Type u) (H : Type v) [CommRing R] [Ring H] [HopfAlgebra R H] [Nontrivial R] {n : ℕ} (hn : n ≠ 0) : Nontrivial (H ⧸ centralAugmentationIdeal R H ^ n)

The quotient by a positive power of the central augmentation ideal is nonzero. Every positive power is contained in the ideal itself, which is proper over a nontrivial base ring.

theorem TauCeti.HopfIdeal.exists_finset_span_eq_centralAugmentationIdeal (R : Type u) (H : Type v) [CommRing R] [Ring H] [HopfAlgebra R H] [IsNoetherianRing H] : ∃ (s : Finset H), ↑s ⊆ ↑(centralAugmentation R H) ∧ Ideal.span ↑s = centralAugmentationIdeal R H

In a left-Noetherian Hopf algebra, the central augmentation ideal has a finite generating subset whose members are themselves central and of augmentation zero.

@[simp]

theorem TauCeti.HopfIdeal.le_augmentation (R : Type u) (H : Type v) [CommRing R] [Ring H] [HopfAlgebra R H] (I : HopfIdeal R H) : I ≤ augmentation R H

Every Hopf ideal is contained in the augmentation ideal.

theorem TauCeti.HopfIdeal.comapOfSurjective_augmentation {S : Type u} {K : Type v} {L : Type w} [CommRing S] [Ring K] [Ring L] [HopfAlgebra S K] [HopfAlgebra S L] (f : K →ₐc[S] L) (hf : Function.Surjective ⇑f) : (augmentation S L).comapOfSurjective f hf = augmentation S K

Pulling the augmentation ideal back along a surjective bialgebra morphism gives the augmentation ideal.

noncomputable def TauCeti.HopfIdeal.counitBialgEquivOfAugmentationEqBot {S : Type u} {K : Type v} [CommRing S] [Ring K] [HopfAlgebra S K] (h : augmentation S K = ⊥) : K ≃ₐc[S] S

A Hopf algebra whose augmentation ideal is zero is bialgebra-equivalent to its base ring via the counit.

Equations

• TauCeti.HopfIdeal.counitBialgEquivOfAugmentationEqBot h = BialgEquiv.ofBijective (Bialgebra.counitBialgHom S K) ⋯

@[simp]

theorem TauCeti.HopfIdeal.counitBialgEquivOfAugmentationEqBot_apply {S : Type u} {K : Type v} [CommRing S] [Ring K] [HopfAlgebra S K] (h : augmentation S K = ⊥) (x : K) : (counitBialgEquivOfAugmentationEqBot h) x = (Bialgebra.counitBialgHom S K) x

The equivalence from a Hopf algebra with zero augmentation ideal to its base ring is the counit.

@[simp]

theorem TauCeti.HopfIdeal.counitBialgEquivOfAugmentationEqBot_symm_apply {S : Type u} {K : Type v} [CommRing S] [Ring K] [HopfAlgebra S K] (h : augmentation S K = ⊥) (r : S) : (counitBialgEquivOfAugmentationEqBot h).symm r = (algebraMap S K) r

The inverse equivalence from the base ring is the structure map.