Documentation

TauCeti.Algebra.HopfAlgebra.HopfIdeal.Map

Images of Hopf ideals under morphisms into commutative Hopf algebras #

This file records the pushforward of a Hopf ideal along a bialgebra morphism f : H →ₐc[R] K with commutative codomain: the extension Ideal.map f I of a Hopf ideal I — the ideal of K generated by the image of I — is again a Hopf ideal. Commutativity of the codomain makes the generated ideal two-sided and the antipode an algebra endomorphism; the coideal and counit conditions transport along f because f intertwines the comultiplications and counits.

Commutativity of the codomain is one of two independent sufficient conditions for the generated ideal to be antipode-stable and two-sided (the other is surjectivity of f, where the generated ideal is the set-theoretic image); for a general morphism of noncommutative Hopf algebras the left ideal generated by the image need not be two-sided, and the standard construction uses the two-sided ideal K f(I) K instead. The commutative case is the one the affine group-scheme dictionary consumes.

Together with TauCeti.HopfIdeal.comapOfSurjective, this gives both variance directions for Hopf ideals. The two are adjoint along surjective morphisms (TauCeti.HopfIdeal.map_le_iff_le_comapOfSurjective).

This is a Layer 3 prerequisite for the reductive-groups roadmap target "Hopf ideals ↔ closed subgroup schemes", specifically the "kernels" part of the dictionary: the kernel of the affine group-scheme morphism induced by f is cut out by the image of the augmentation ideal under f.

Main declarations #

References #

The construction is the standard image of a Hopf ideal; see for instance Milne, Algebraic Groups around Definition 3.10, where quotients by such images cut out closed subgroup schemes.

source
@[simp]
theorem TauCeti.HopfIdeal.map_tensor_leftTensorIdeal {R : Type u} [CommSemiring R] {H : Type v} {K : Type w} [Semiring H] [Semiring K] [Algebra R H] [Algebra R K] (f : H →ₐ[R] K) (I : Ideal H) :
Ideal.map (↑(Algebra.TensorProduct.map f f)) (leftTensorIdeal R H I) = leftTensorIdeal R K (Ideal.map f.toRingHom I)

The tensor square of an algebra morphism carries the left tensor ideal generated by I onto the left tensor ideal generated by the image of I.

source
@[simp]
theorem TauCeti.HopfIdeal.map_tensor_rightTensorIdeal {R : Type u} [CommSemiring R] {H : Type v} {K : Type w} [Semiring H] [Semiring K] [Algebra R H] [Algebra R K] (f : H →ₐ[R] K) (I : Ideal H) :
Ideal.map (↑(Algebra.TensorProduct.map f f)) (rightTensorIdeal R H I) = rightTensorIdeal R K (Ideal.map f.toRingHom I)

The tensor square of an algebra morphism carries the right tensor ideal generated by I onto the right tensor ideal generated by the image of I.

This is the ideal-theoretic compatibility used to transport conjugation stability, hence normality, along a morphism of commutative Hopf algebras.

source
def TauCeti.HopfIdeal.map {R : Type u} [CommSemiring R] {H : Type v} {K : Type w} [Semiring H] [CommSemiring K] [HopfAlgebra R H] [HopfAlgebra R K] (I : HopfIdeal R H) (f : H →ₐc[R] K) :
HopfIdeal R K

The image of a Hopf ideal under a bialgebra morphism into a commutative Hopf algebra: the Hopf ideal generated by the set-theoretic image.

Its underlying ideal is the ideal-theoretic extension Ideal.map.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.HopfIdeal.map_toIdeal {R : Type u} [CommSemiring R] {H : Type v} {K : Type w} [Semiring H] [CommSemiring K] [HopfAlgebra R H] [HopfAlgebra R K] (I : HopfIdeal R H) (f : H →ₐc[R] K) :
    (I.map f).toIdeal = Ideal.map (↑f) I.toIdeal

    The underlying ideal of I.map f is the ordinary ideal-theoretic image.

    source
    theorem TauCeti.HopfIdeal.mem_map_of_mem {R : Type u} [CommSemiring R] {H : Type v} {K : Type w} [Semiring H] [CommSemiring K] [HopfAlgebra R H] [HopfAlgebra R K] (f : H →ₐc[R] K) {I : HopfIdeal R H} {x : H} (hx : x ∈ I) :
    f x ∈ I.map f

    The image of a Hopf ideal contains the image of each of its elements.

    source
    theorem TauCeti.HopfIdeal.map_mono {R : Type u} [CommSemiring R] {H : Type v} {K : Type w} [Semiring H] [CommSemiring K] [HopfAlgebra R H] [HopfAlgebra R K] (f : H →ₐc[R] K) {I J : HopfIdeal R H} (hIJ : I ≤ J) :
    I.map f ≤ J.map f

    Image of Hopf ideals is monotone.

    source
    theorem TauCeti.HopfIdeal.map_le_iff {R : Type u} [CommSemiring R] {H : Type v} {K : Type w} [Semiring H] [CommSemiring K] [HopfAlgebra R H] [HopfAlgebra R K] {f : H →ₐc[R] K} {I : HopfIdeal R H} {J : HopfIdeal R K} :
    I.map f ≤ J ↔ ∀ ⦃x : H⦄, x ∈ I → f x ∈ J

    The universal property of the image: I.map f is below J exactly when f sends I into J. Membership in I.map f itself is characterized only along surjective morphisms (TauCeti.HopfIdeal.mem_map_iff_of_surjective), since the image Hopf ideal is generated by, and in general larger than, the set-theoretic image of I.

    source
    @[simp]
    theorem TauCeti.HopfIdeal.map_bot {R : Type u} [CommSemiring R] {H : Type v} {K : Type w} [Semiring H] [CommSemiring K] [HopfAlgebra R H] [HopfAlgebra R K] (f : H →ₐc[R] K) :
    ⊥.map f = ⊥

    The image of the zero Hopf ideal is zero.

    source
    @[simp]
    theorem TauCeti.HopfIdeal.mem_map_iff_of_surjective {R : Type u} [CommSemiring R] {H : Type v} {K : Type w} [Semiring H] [CommSemiring K] [HopfAlgebra R H] [HopfAlgebra R K] {f : H →ₐc[R] K} (hf : Function.Surjective ⇑f) {I : HopfIdeal R H} {y : K} :
    y ∈ I.map f ↔ ∃ x ∈ I, f x = y

    For a surjective morphism, membership in the image Hopf ideal means being the value of a member.

    source
    theorem TauCeti.HopfIdeal.map_eq_bot_iff {R : Type u} [CommSemiring R] {H : Type v} {K : Type w} [Semiring H] [CommSemiring K] [HopfAlgebra R H] [HopfAlgebra R K] (I : HopfIdeal R H) (f : H →ₐc[R] K) :
    I.map f = ⊥ ↔ I.toIdeal ≤ RingHom.ker ↑f

    The image vanishes exactly when the Hopf ideal is contained in the kernel of the underlying ring homomorphism. For surjective morphisms the right side is the kernel Hopf ideal (TauCeti.HopfIdeal.map_eq_bot_iff_le_ker).

    source
    @[simp]
    theorem TauCeti.HopfIdeal.map_sup {R : Type u} [CommSemiring R] {H : Type v} {K : Type w} [Semiring H] [CommSemiring K] [HopfAlgebra R H] [HopfAlgebra R K] (I J : HopfIdeal R H) (f : H →ₐc[R] K) :
    (I ⊔ J).map f = I.map f ⊔ J.map f

    Image of Hopf ideals preserves binary joins.

    source
    @[simp]
    theorem TauCeti.HopfIdeal.map_iSup {R : Type u} [CommSemiring R] {H : Type v} {K : Type w} [Semiring H] [CommSemiring K] [HopfAlgebra R H] [HopfAlgebra R K] {ι : Sort u_1} (I : ι → HopfIdeal R H) (f : H →ₐc[R] K) :
    (⨆ (i : ι), I i).map f = ⨆ (i : ι), (I i).map f

    Image of Hopf ideals preserves indexed suprema.

    source
    @[simp]
    theorem TauCeti.HopfIdeal.map_sSup {R : Type u} [CommSemiring R] {H : Type v} {K : Type w} [Semiring H] [CommSemiring K] [HopfAlgebra R H] [HopfAlgebra R K] (S : Set (HopfIdeal R H)) (f : H →ₐc[R] K) :
    (sSup S).map f = sSup ((fun (I : HopfIdeal R H) => I.map f) '' S)

    Image of Hopf ideals preserves suprema of sets.

    source
    @[simp]
    theorem TauCeti.HopfIdeal.map_id {R : Type u} [CommSemiring R] {H : Type v} [CommSemiring H] [HopfAlgebra R H] (I : HopfIdeal R H) :
    I.map (BialgHom.id R H) = I

    The image of a Hopf ideal under the identity morphism.

    source
    @[simp]
    theorem TauCeti.HopfIdeal.map_map {R : Type u} [CommSemiring R] {H : Type v} {K : Type w} {L : Type x} [Semiring H] [CommSemiring K] [CommSemiring L] [HopfAlgebra R H] [HopfAlgebra R K] [HopfAlgebra R L] (I : HopfIdeal R H) (f : H →ₐc[R] K) (g : K →ₐc[R] L) :
    (I.map f).map g = I.map (g.comp f)

    Image of Hopf ideals is functorial.

    source
    theorem TauCeti.HopfIdeal.map_le_iff_le_comapOfSurjective {R : Type u} [CommRing R] {H : Type v} {K : Type w} [Ring H] [CommRing K] [HopfAlgebra R H] [HopfAlgebra R K] {f : H →ₐc[R] K} (hf : Function.Surjective ⇑f) {I : HopfIdeal R H} {J : HopfIdeal R K} :
    I.map f ≤ J ↔ I ≤ J.comapOfSurjective f hf

    Along a surjective morphism, the image of Hopf ideals is left adjoint to the inverse image.

    source
    @[simp]
    theorem TauCeti.HopfIdeal.map_comapOfSurjective {R : Type u} [CommRing R] {H : Type v} {K : Type w} [Ring H] [CommRing K] [HopfAlgebra R H] [HopfAlgebra R K] (J : HopfIdeal R K) (f : H →ₐc[R] K) (hf : Function.Surjective ⇑f) :
    (J.comapOfSurjective f hf).map f = J

    Along a surjective morphism, image after inverse image recovers the Hopf ideal.

    source
    theorem TauCeti.HopfIdeal.comapOfSurjective_map {R : Type u} [CommRing R] {H : Type v} {K : Type w} [Ring H] [CommRing K] [HopfAlgebra R H] [HopfAlgebra R K] (I : HopfIdeal R H) (f : H →ₐc[R] K) (hf : Function.Surjective ⇑f) :
    (I.map f).comapOfSurjective f hf = I ⊔ kerOfSurjective f hf

    Along a surjective morphism, inverse image after image is the join with the kernel.

    source
    theorem TauCeti.HopfIdeal.comapOfSurjective_map_of_bijective {R : Type u} [CommRing R] {H : Type v} {K : Type w} [Ring H] [CommRing K] [HopfAlgebra R H] [HopfAlgebra R K] (I : HopfIdeal R H) (f : H →ₐc[R] K) (hf : Function.Bijective ⇑f) :
    (I.map f).comapOfSurjective f ⋯ = I

    Along a bijective morphism, inverse image after image recovers the Hopf ideal.

    source
    theorem TauCeti.HopfIdeal.map_eq_bot_iff_le_ker {R : Type u} [CommRing R] {H : Type v} {K : Type w} [Ring H] [CommRing K] [HopfAlgebra R H] [HopfAlgebra R K] (I : HopfIdeal R H) (f : H →ₐc[R] K) (hf : Function.Surjective ⇑f) :
    I.map f = ⊥ ↔ I ≤ kerOfSurjective f hf

    The image vanishes exactly on Hopf ideals contained in the kernel Hopf ideal: the surjective bundled form of TauCeti.HopfIdeal.map_eq_bot_iff.

    source
    @[simp]
    theorem TauCeti.HopfIdeal.comapOfSurjective_map_mkBialgHom {R : Type u} [CommRing R] {H : Type v} [CommRing H] [HopfAlgebra R H] {I J : HopfIdeal R H} (hIJ : I ≤ J) :
    (J.map (Bialgebra.Quotient.mkBialgHom I.toIdeal)).comapOfSurjective (Bialgebra.Quotient.mkBialgHom I.toIdeal) ⋯ = J

    Pulling the image of J in H ⧸ I back along the quotient morphism recovers J when I ≤ J.