Inverse images of Hopf ideals

This file records inverse images of Hopf ideals. Over a general commutative base, a surjective bialgebra morphism supplies the tensor exactness needed for the construction. Alternatively, flatness of K/I and H/f⁻¹(I) lets us take the kernel of the composite H → K → K/I. Over a field these flatness conditions hold for every bialgebra morphism.

For a surjective morphism f : H →ₐc[R] K and a Hopf ideal I of K, the preimage f ⁻¹ I is a Hopf ideal of H. The construction is made by applying the existing kernel-of-a-surjective-Hopf-map theorem to the composite H → K → K/I.

The surjectivity hypothesis is intentional: over a general commutative base, the tensor exactness needed for the coideal condition is not automatic without an exactness hypothesis.

Main declarations

• TauCeti.HopfIdeal.comap: the inverse image when the quotient and preimage quotient are flat.
• TauCeti.HopfIdeal.comapOfSurjective: the inverse image under a surjective morphism over a general base.
• TauCeti.HopfIdeal.comap_toIdeal and TauCeti.HopfIdeal.mem_comap: characteristic API for the flat construction.
• TauCeti.HopfIdeal.comapOfSurjective_toIdeal and TauCeti.HopfIdeal.mem_comapOfSurjective: characteristic API over a general base.
• TauCeti.HopfIdeal.comapOfSurjective_eq_comap: comparison of the two constructions when both apply.
• TauCeti.HopfIdeal.comapOfSurjective_le_comapOfSurjective_iff: surjective inverse image reflects containment.
• TauCeti.HopfIdeal.comapOfSurjective_bot: the kernel of a surjective morphism is the inverse image of the zero Hopf ideal.
• TauCeti.HopfIdeal.comapOfSurjective_sup: surjective inverse image preserves binary joins.
• TauCeti.HopfIdeal.comapOfSurjective_iSup and TauCeti.HopfIdeal.comapOfSurjective_sSup: surjective inverse image preserves nonempty suprema.
• TauCeti.HopfIdeal.comapOfSurjective_id and TauCeti.HopfIdeal.comapOfSurjective_comapOfSurjective: identity and composition laws.
• TauCeti.HopfIdeal.comapOfSurjective_bialgEquiv_symm_apply: inverse-image cancellation for a bialgebra equivalence.

References

The constructions are the standard inverse images of Hopf ideals, reduced here to the quotient-kernel constructions already in TauCeti.Algebra.HopfAlgebra.HopfIdeal.Kernel. Over a general base the morphism can be surjective or have the required flat quotient algebras; over a field it is arbitrary.

noncomputable def TauCeti.HopfIdeal.comapOfSurjective {R : Type u} [CommRing R] {H : Type v} {K : Type w} [Ring H] [Ring K] [HopfAlgebra R H] [HopfAlgebra R K] (I : HopfIdeal R K) (f : H →ₐc[R] K) (hf : Function.Surjective ⇑f) : HopfIdeal R H

The inverse image of a Hopf ideal along a surjective bialgebra morphism.

It is defined as the kernel of the composite H → K → K/I; its underlying ideal is the ordinary ideal comap of I.toIdeal.

Equations

• I.comapOfSurjective f hf = TauCeti.HopfIdeal.kerOfSurjective ((Bialgebra.Quotient.mkBialgHom I.toIdeal).comp f) ⋯

@[simp]

theorem TauCeti.HopfIdeal.comapOfSurjective_toIdeal {R : Type u} [CommRing R] {H : Type v} {K : Type w} [Ring H] [Ring K] [HopfAlgebra R H] [HopfAlgebra R K] (I : HopfIdeal R K) (f : H →ₐc[R] K) (hf : Function.Surjective ⇑f) : (I.comapOfSurjective f hf).toIdeal = Ideal.comap (↑f) I.toIdeal

The underlying ideal of I.comapOfSurjective f hf is the ordinary ideal-theoretic inverse image.

@[simp]

theorem TauCeti.HopfIdeal.mem_comapOfSurjective {R : Type u} [CommRing R] {H : Type v} {K : Type w} [Ring H] [Ring K] [HopfAlgebra R H] [HopfAlgebra R K] {I : HopfIdeal R K} {f : H →ₐc[R] K} {hf : Function.Surjective ⇑f} {h : H} : h ∈ I.comapOfSurjective f hf ↔ f h ∈ I

Membership in the inverse-image Hopf ideal is membership after applying the morphism.

theorem TauCeti.HopfIdeal.comapOfSurjective_eq_kerOfSurjective {R : Type u} [CommRing R] {H : Type v} {K : Type w} [Ring H] [Ring K] [HopfAlgebra R H] [HopfAlgebra R K] (I : HopfIdeal R K) (f : H →ₐc[R] K) (hf : Function.Surjective ⇑f) : I.comapOfSurjective f hf = kerOfSurjective ((Bialgebra.Quotient.mkBialgHom I.toIdeal).comp f) ⋯

The inverse image is the kernel of the composite with the quotient morphism.

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

Inverse image of Hopf ideals is monotone.

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

For a surjective morphism, inverse image of Hopf ideals reflects containment.

@[simp]

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

For a surjective morphism, containment after inverse image is equivalent to containment before inverse image.

@[simp]

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

For a surjective morphism, inverse image of Hopf ideals reflects equality.

@[simp]

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

The inverse image of the zero Hopf ideal is the kernel Hopf ideal.

@[simp]

theorem TauCeti.HopfIdeal.comapOfSurjective_iSup {R : Type u} [CommRing R] {H : Type v} {K : Type w} [Ring H] [Ring K] [HopfAlgebra R H] [HopfAlgebra R K] {ι : Sort u_1} [Nonempty ι] (I : ι → HopfIdeal R K) (f : H →ₐc[R] K) (hf : Function.Surjective ⇑f) : (⨆ (i : ι), I i).comapOfSurjective f hf = ⨆ (i : ι), (I i).comapOfSurjective f hf

Surjective inverse image of Hopf ideals preserves nonempty suprema of families.

@[simp]

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

Surjective inverse image of Hopf ideals preserves joins.

@[simp]

theorem TauCeti.HopfIdeal.comapOfSurjective_sSup {R : Type u} [CommRing R] {H : Type v} {K : Type w} [Ring H] [Ring K] [HopfAlgebra R H] [HopfAlgebra R K] (S : Set (HopfIdeal R K)) (hS : S.Nonempty) (f : H →ₐc[R] K) (hf : Function.Surjective ⇑f) : (sSup S).comapOfSurjective f hf = sSup ((fun (I : HopfIdeal R K) => I.comapOfSurjective f hf) '' S)

Surjective inverse image of Hopf ideals preserves nonempty suprema of sets.

@[simp]

theorem TauCeti.HopfIdeal.comapOfSurjective_id {R : Type u} [CommRing R] {H : Type v} [Ring H] [HopfAlgebra R H] (I : HopfIdeal R H) : I.comapOfSurjective (BialgHom.id R H) ⋯ = I

Pulling a Hopf ideal back along the identity morphism leaves it unchanged.

@[simp]

theorem TauCeti.HopfIdeal.comapOfSurjective_comapOfSurjective {R : Type u} [CommRing R] {H : Type v} {K : Type w} {L : Type x} [Ring H] [Ring K] [Ring L] [HopfAlgebra R H] [HopfAlgebra R K] [HopfAlgebra R L] (I : HopfIdeal R L) (g : K →ₐc[R] L) (hg : Function.Surjective ⇑g) (f : H →ₐc[R] K) (hf : Function.Surjective ⇑f) : (I.comapOfSurjective g hg).comapOfSurjective f hf = I.comapOfSurjective (g.comp f) ⋯

Inverse image of Hopf ideals is compatible with composition of surjective morphisms.

theorem TauCeti.HopfIdeal.comapOfSurjective_bialgEquiv_symm_apply {R : Type u} [CommRing R] {H : Type v} {K : Type w} [Ring H] [Ring K] [HopfAlgebra R H] [HopfAlgebra R K] (I : HopfIdeal R H) (e : H ≃ₐc[R] K) : (I.comapOfSurjective e.symm.toBialgHom ⋯).comapOfSurjective e.toBialgHom ⋯ = I

Pulling a Hopf ideal back along a bialgebra equivalence and then along its inverse recovers the original ideal.

noncomputable def TauCeti.HopfIdeal.comap {H : Type v} {K : Type w} [Ring H] [Ring K] {k : Type u} [CommRing k] [HopfAlgebra k H] [HopfAlgebra k K] (I : HopfIdeal k K) (f : H →ₐc[k] K) [Module.Flat k (K ⧸ I.toIdeal)] [Module.Flat k (H ⧸ Ideal.comap (↑f) I.toIdeal)] : HopfIdeal k H

The inverse image of a Hopf ideal along a bialgebra morphism with flat quotient algebras K/I and H/f⁻¹(I).

In particular, this construction needs no surjectivity hypothesis over a field.

Equations

• I.comap f = TauCeti.HopfIdeal.ker ((Bialgebra.Quotient.mkBialgHom I.toIdeal).comp f)

@[simp]

theorem TauCeti.HopfIdeal.comap_toIdeal {H : Type v} {K : Type w} [Ring H] [Ring K] {k : Type u} [CommRing k] [HopfAlgebra k H] [HopfAlgebra k K] (I : HopfIdeal k K) (f : H →ₐc[k] K) [Module.Flat k (K ⧸ I.toIdeal)] [Module.Flat k (H ⧸ Ideal.comap (↑f) I.toIdeal)] : (I.comap f).toIdeal = Ideal.comap (↑f) I.toIdeal

The underlying ideal of comap is the ordinary ideal-theoretic inverse image.

@[simp]

theorem TauCeti.HopfIdeal.mem_comap {H : Type v} {K : Type w} [Ring H] [Ring K] {k : Type u} [CommRing k] [HopfAlgebra k H] [HopfAlgebra k K] {I : HopfIdeal k K} {f : H →ₐc[k] K} [Module.Flat k (K ⧸ I.toIdeal)] [Module.Flat k (H ⧸ Ideal.comap (↑f) I.toIdeal)] {h : H} : h ∈ I.comap f ↔ f h ∈ I

Membership in the inverse image is membership after applying the morphism.

theorem TauCeti.HopfIdeal.comapOfSurjective_eq_comap {H : Type v} {K : Type w} [Ring H] [Ring K] {k : Type u} [CommRing k] [HopfAlgebra k H] [HopfAlgebra k K] (I : HopfIdeal k K) (f : H →ₐc[k] K) [Module.Flat k (K ⧸ I.toIdeal)] [Module.Flat k (H ⧸ Ideal.comap (↑f) I.toIdeal)] (hf : Function.Surjective ⇑f) : I.comapOfSurjective f hf = I.comap f

The surjective and flat inverse-image constructions agree whenever both apply.

theorem TauCeti.HopfIdeal.comap_mono {H : Type v} {K : Type w} [Ring H] [Ring K] {k : Type u} [CommRing k] [HopfAlgebra k H] [HopfAlgebra k K] (f : H →ₐc[k] K) {I J : HopfIdeal k K} (hIJ : I ≤ J) [Module.Flat k (K ⧸ I.toIdeal)] [Module.Flat k (K ⧸ J.toIdeal)] [Module.Flat k (H ⧸ Ideal.comap (↑f) I.toIdeal)] [Module.Flat k (H ⧸ Ideal.comap (↑f) J.toIdeal)] : I.comap f ≤ J.comap f

Inverse image of Hopf ideals is monotone whenever the required quotients are flat.

theorem TauCeti.HopfIdeal.ker_comp {H : Type v} {K : Type w} {L : Type x} [Ring H] [Ring K] [Ring L] {k : Type u} [CommRing k] [HopfAlgebra k H] [HopfAlgebra k K] [HopfAlgebra k L] (f : H →ₐc[k] K) (g : K →ₐc[k] L) [Module.Flat k L] [Module.Flat k (K ⧸ RingHom.ker ↑g)] [Module.Flat k (H ⧸ RingHom.ker ↑(g.comp f))] : ker (g.comp f) = (ker g).comap f

The kernel of a composite is the inverse image of the second morphism's kernel.

@[simp]

theorem TauCeti.HopfIdeal.comap_bot {H : Type v} {K : Type w} [Ring H] [Ring K] {k : Type u} [CommRing k] [HopfAlgebra k H] [HopfAlgebra k K] (f : H →ₐc[k] K) [Module.Flat k K] [Module.Flat k (H ⧸ RingHom.ker ↑f)] : ⊥.comap f = ker f

The inverse image of the zero Hopf ideal is the Hopf-ideal kernel when the required quotients are flat.

@[simp]

theorem TauCeti.HopfIdeal.comap_id {H : Type v} [Ring H] {k : Type u} [CommRing k] [HopfAlgebra k H] (I : HopfIdeal k H) [Module.Flat k (H ⧸ I.toIdeal)] : I.comap (BialgHom.id k H) = I

Pulling a Hopf ideal back along the identity leaves it unchanged when its quotient is flat.

@[simp]

theorem TauCeti.HopfIdeal.comap_comap {H : Type v} {K : Type w} {L : Type x} [Ring H] [Ring K] [Ring L] {k : Type u} [CommRing k] [HopfAlgebra k H] [HopfAlgebra k K] [HopfAlgebra k L] (I : HopfIdeal k L) (g : K →ₐc[k] L) (f : H →ₐc[k] K) [Module.Flat k (L ⧸ I.toIdeal)] [Module.Flat k (K ⧸ Ideal.comap (↑g) I.toIdeal)] [Module.Flat k (H ⧸ Ideal.comap (↑(g.comp f)) I.toIdeal)] : (I.comap g).comap f = I.comap (g.comp f)

Inverse image of Hopf ideals is compatible with composition when all quotient presentations are flat.