Hopf ideals

This file defines Hopf ideals in a Hopf algebra over a commutative semiring. A Hopf ideal is an ideal I whose comultiplication lands in I ⊗ H + H ⊗ I, whose counit vanishes on I, and which is stable under the antipode.

This is a small Layer 3 prerequisite for the reductive-groups roadmap target "Hopf ideals ↔ closed subgroup schemes": closed subgroup schemes of an affine group scheme are represented on coordinate rings by quotient Hopf algebras, and the ideal being quotiented must satisfy exactly these Hopf-ideal closure conditions.

Main definitions

• TauCeti.HopfIdeal: a Hopf ideal in a Hopf algebra over a commutative semiring.
• TauCeti.HopfIdeal.leftTensorIdeal and TauCeti.HopfIdeal.rightTensorIdeal: the two summands I ⊗ H and H ⊗ I inside H ⊗ H.
• TauCeti.HopfIdeal.ker_tensorProduct_map_eq_leftTensorIdeal_sup_rightTensorIdeal: the tensor product of two surjective algebra maps has the expected kernel in tensor-ideal notation.
• ⊥ : HopfIdeal R H: the zero Hopf ideal.
• I ⊔ J : HopfIdeal R H: the sum of two Hopf ideals.
• sSup S : HopfIdeal R H and ⨆ i, I i : HopfIdeal R H: arbitrary suprema of Hopf ideals, with underlying ideal the supremum of the underlying ideals.
• TauCeti.HopfIdeal.instIsCoideal, TauCeti.HopfIdeal.instIsHopfIdeal: over a commutative ring, the bridge instances exhibiting I.toIdeal as a coideal and a Hopf ideal in Mathlib's sense, so that Mathlib's quotient coalgebra/bialgebra/Hopf instances fire on H ⧸ I.toIdeal.

References

This follows the standard Hopf-algebra definition of a Hopf ideal; see Sweedler, Hopf Algebras, Chapter 1. The formalization uses Mathlib's Hopf-algebra and tensor-product ideal API. The arbitrary-supremum lattice construction follows the local pattern from TauCeti.Algebra.Coalgebra.Subcoalgebra.Lattice and TauCeti.Algebra.Coalgebra.Subcomodule.Lattice.

def TauCeti.HopfIdeal.leftTensorIdeal (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] [Algebra R H] (I : Ideal H) : Ideal (TensorProduct R H H)

The image of an ideal I ≤ H under the left inclusion H → H ⊗[R] H, representing I ⊗ H inside the tensor product algebra.

Equations

• TauCeti.HopfIdeal.leftTensorIdeal R H I = Ideal.map Algebra.TensorProduct.includeLeft.toRingHom I

def TauCeti.HopfIdeal.rightTensorIdeal (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] [Algebra R H] (I : Ideal H) : Ideal (TensorProduct R H H)

The image of an ideal I ≤ H under the right inclusion H → H ⊗[R] H, representing H ⊗ I inside the tensor product algebra.

Equations

• TauCeti.HopfIdeal.rightTensorIdeal R H I = Ideal.map Algebra.TensorProduct.includeRight.toRingHom I

theorem TauCeti.HopfIdeal.leftTensorIdeal_def (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] [Algebra R H] (I : Ideal H) : leftTensorIdeal R H I = Ideal.map Algebra.TensorProduct.includeLeft.toRingHom I

theorem TauCeti.HopfIdeal.rightTensorIdeal_def (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] [Algebra R H] (I : Ideal H) : rightTensorIdeal R H I = Ideal.map Algebra.TensorProduct.includeRight.toRingHom I

theorem TauCeti.HopfIdeal.includeLeft_mem_leftTensorIdeal (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] [Algebra R H] {I : Ideal H} {x : H} (hx : x ∈ I) : Algebra.TensorProduct.includeLeft x ∈ leftTensorIdeal R H I

The left tensor inclusion sends elements of I into I ⊗ H.

theorem TauCeti.HopfIdeal.includeRight_mem_rightTensorIdeal (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] [Algebra R H] {I : Ideal H} {x : H} (hx : x ∈ I) : Algebra.TensorProduct.includeRight x ∈ rightTensorIdeal R H I

The right tensor inclusion sends elements of I into H ⊗ I.

theorem TauCeti.HopfIdeal.tmul_mem_leftTensorIdeal (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] [Algebra R H] {I : Ideal H} {x : H} (hx : x ∈ I) (y : H) : x ⊗ₜ[R] y ∈ leftTensorIdeal R H I

A pure tensor x ⊗ₜ y with x ∈ I lies in I ⊗ H.

theorem TauCeti.HopfIdeal.tmul_mem_rightTensorIdeal (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] [Algebra R H] {I : Ideal H} (x : H) {y : H} (hy : y ∈ I) : x ⊗ₜ[R] y ∈ rightTensorIdeal R H I

A pure tensor x ⊗ₜ y with y ∈ I lies in H ⊗ I.

theorem TauCeti.HopfIdeal.mem_leftTensorIdeal (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] [Algebra R H] {I : Ideal H} {x : TensorProduct R H H} : x ∈ leftTensorIdeal R H I ↔ x ∈ Ideal.map Algebra.TensorProduct.includeLeft.toRingHom I

theorem TauCeti.HopfIdeal.mem_rightTensorIdeal (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] [Algebra R H] {I : Ideal H} {x : TensorProduct R H H} : x ∈ rightTensorIdeal R H I ↔ x ∈ Ideal.map Algebra.TensorProduct.includeRight.toRingHom I

theorem TauCeti.HopfIdeal.leftTensorIdeal_le_iff (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] [Algebra R H] {I : Ideal H} {J : Ideal (TensorProduct R H H)} : leftTensorIdeal R H I ≤ J ↔ I ≤ Ideal.comap Algebra.TensorProduct.includeLeft.toRingHom J

The order universal property for I ⊗ H.

theorem TauCeti.HopfIdeal.rightTensorIdeal_le_iff (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] [Algebra R H] {I : Ideal H} {J : Ideal (TensorProduct R H H)} : rightTensorIdeal R H I ≤ J ↔ I ≤ Ideal.comap Algebra.TensorProduct.includeRight.toRingHom J

The order universal property for H ⊗ I.

theorem TauCeti.HopfIdeal.leftTensorIdeal_mono (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] [Algebra R H] {I J : Ideal H} (hIJ : I ≤ J) : leftTensorIdeal R H I ≤ leftTensorIdeal R H J

The construction I ↦ I ⊗ H is monotone.

theorem TauCeti.HopfIdeal.rightTensorIdeal_mono (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] [Algebra R H] {I J : Ideal H} (hIJ : I ≤ J) : rightTensorIdeal R H I ≤ rightTensorIdeal R H J

The construction I ↦ H ⊗ I is monotone.

@[simp]

theorem TauCeti.HopfIdeal.leftTensorIdeal_iSup (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] [Algebra R H] {ι : Sort u_1} (I : ι → Ideal H) : leftTensorIdeal R H (⨆ (i : ι), I i) = ⨆ (i : ι), leftTensorIdeal R H (I i)

The construction I ↦ I ⊗ H distributes over arbitrary suprema of ideals.

@[simp]

theorem TauCeti.HopfIdeal.rightTensorIdeal_iSup (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] [Algebra R H] {ι : Sort u_1} (I : ι → Ideal H) : rightTensorIdeal R H (⨆ (i : ι), I i) = ⨆ (i : ι), rightTensorIdeal R H (I i)

The construction I ↦ H ⊗ I distributes over arbitrary suprema of ideals.

@[simp]

theorem TauCeti.HopfIdeal.leftTensorIdeal_sup (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] [Algebra R H] (I J : Ideal H) : leftTensorIdeal R H (I ⊔ J) = leftTensorIdeal R H I ⊔ leftTensorIdeal R H J

The construction I ↦ I ⊗ H distributes over joins of ideals.

@[simp]

theorem TauCeti.HopfIdeal.rightTensorIdeal_sup (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] [Algebra R H] (I J : Ideal H) : rightTensorIdeal R H (I ⊔ J) = rightTensorIdeal R H I ⊔ rightTensorIdeal R H J

The construction I ↦ H ⊗ I distributes over joins of ideals.

theorem TauCeti.HopfIdeal.ker_tensorProduct_map_id_quotient {R : Type u} {H : Type v} [CommRing R] [CommRing H] [Algebra R H] (I : Ideal H) : RingHom.ker (Algebra.TensorProduct.map (AlgHom.id R H) (Ideal.Quotient.mkₐ R I)) = rightTensorIdeal R H I

The kernel of tensoring the quotient map on the right is the right tensor ideal.

theorem TauCeti.HopfIdeal.ker_tensorProduct_map_quotient_id {R : Type u} {H : Type v} [CommRing R] [CommRing H] [Algebra R H] (I : Ideal H) : RingHom.ker (Algebra.TensorProduct.map (Ideal.Quotient.mkₐ R I) (AlgHom.id R H)) = leftTensorIdeal R H I

The kernel of tensoring the quotient map on the left is the left tensor ideal.

structure TauCeti.HopfIdeal (R : Type u) (H : Type v) [CommSemiring R] [Semiring H] [HopfAlgebra R H] : Type v

A Hopf ideal in a Hopf algebra over a commutative semiring.

The comultiplication condition is stated in the ambient tensor product algebra as Δ(I) ⊆ I ⊗ H + H ⊗ I. Over a commutative ring, the bridge instances HopfIdeal.instIsCoideal and HopfIdeal.instIsHopfIdeal below let Mathlib endow the quotient H ⧸ I.toIdeal with its Hopf-algebra structure.

• carrier : Ideal H

  The underlying ideal.

• isTwoSided' : self.carrier.IsTwoSided

  The underlying ideal is two-sided.

• comul_mem' ⦃x : H⦄ : x ∈ self.carrier → CoalgebraStruct.comul x ∈ leftTensorIdeal R H self.carrier ⊔ rightTensorIdeal R H self.carrier

  The comultiplication of an element of the ideal lies in I ⊗ H + H ⊗ I.

• counit_eq_zero' ⦃x : H⦄ : x ∈ self.carrier → CoalgebraStruct.counit x = 0

  The counit vanishes on the ideal.

• antipode_mem' ⦃x : H⦄ : x ∈ self.carrier → (HopfAlgebraStruct.antipode R) x ∈ self.carrier

  The antipode preserves the ideal.

@[instance_reducible]

instance TauCeti.HopfIdeal.instSetLike {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] : SetLike (HopfIdeal R H) H

Equations

• TauCeti.HopfIdeal.instSetLike = { coe := fun (I : TauCeti.HopfIdeal R H) => ↑I.carrier, coe_injective := ⋯ }

instance TauCeti.HopfIdeal.instAddSubmonoidClass {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] : AddSubmonoidClass (HopfIdeal R H) H

instance TauCeti.HopfIdeal.instSMulMemClass {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] : SMulMemClass (HopfIdeal R H) H H

@[instance_reducible]

instance TauCeti.HopfIdeal.instPartialOrder {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] : PartialOrder (HopfIdeal R H)

Equations

• TauCeti.HopfIdeal.instPartialOrder = PartialOrder.ofSetLike (TauCeti.HopfIdeal R H)

def TauCeti.HopfIdeal.toIdeal {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] (I : HopfIdeal R H) : Ideal H

The underlying ideal of a Hopf ideal.

Equations

• I.toIdeal = I.carrier

instance TauCeti.HopfIdeal.instIsTwoSidedToIdeal {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] (I : HopfIdeal R H) : I.toIdeal.IsTwoSided

@[simp]

theorem TauCeti.HopfIdeal.mem_carrier {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] {I : HopfIdeal R H} {x : H} : x ∈ I.carrier ↔ x ∈ I

@[simp]

theorem TauCeti.HopfIdeal.mem_toIdeal {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] {I : HopfIdeal R H} {x : H} : x ∈ I.toIdeal ↔ x ∈ I

theorem TauCeti.HopfIdeal.toIdeal_carrier {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] (I : HopfIdeal R H) : I.toIdeal = I.carrier

theorem TauCeti.HopfIdeal.le_def {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] {I J : HopfIdeal R H} : I ≤ J ↔ ∀ ⦃x : H⦄, x ∈ I → x ∈ J

theorem TauCeti.HopfIdeal.toIdeal_le_toIdeal {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] {I J : HopfIdeal R H} : I.toIdeal ≤ J.toIdeal ↔ I ≤ J

theorem TauCeti.HopfIdeal.ext {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] {I J : HopfIdeal R H} (h : ∀ (x : H), x ∈ I ↔ x ∈ J) : I = J

Two Hopf ideals are equal when they contain the same elements.

theorem TauCeti.HopfIdeal.ext_iff {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] {I J : HopfIdeal R H} : I = J ↔ ∀ (x : H), x ∈ I ↔ x ∈ J

def TauCeti.HopfIdeal.ofIdeal {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] (I : Ideal H) [I.IsTwoSided] (hcomul : ∀ ⦃x : H⦄, x ∈ I → CoalgebraStruct.comul x ∈ leftTensorIdeal R H I ⊔ rightTensorIdeal R H I) (hcounit : ∀ ⦃x : H⦄, x ∈ I → CoalgebraStruct.counit x = 0) (hantipode : ∀ ⦃x : H⦄, x ∈ I → (HopfAlgebraStruct.antipode R) x ∈ I) : HopfIdeal R H

Constructor from an ideal and the three Hopf-ideal closure conditions.

Equations

• TauCeti.HopfIdeal.ofIdeal I hcomul hcounit hantipode = { carrier := I, isTwoSided' := ⋯, comul_mem' := hcomul, counit_eq_zero' := hcounit, antipode_mem' := hantipode }

@[simp]

theorem TauCeti.HopfIdeal.ofIdeal_carrier {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] (I : Ideal H) [I.IsTwoSided] (hcomul : ∀ ⦃x : H⦄, x ∈ I → CoalgebraStruct.comul x ∈ leftTensorIdeal R H I ⊔ rightTensorIdeal R H I) (hcounit : ∀ ⦃x : H⦄, x ∈ I → CoalgebraStruct.counit x = 0) (hantipode : ∀ ⦃x : H⦄, x ∈ I → (HopfAlgebraStruct.antipode R) x ∈ I) : (ofIdeal I hcomul hcounit hantipode).carrier = I

@[simp]

theorem TauCeti.HopfIdeal.mem_ofIdeal {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] {I : Ideal H} [I.IsTwoSided] {hcomul : ∀ ⦃x : H⦄, x ∈ I → CoalgebraStruct.comul x ∈ leftTensorIdeal R H I ⊔ rightTensorIdeal R H I} {hcounit : ∀ ⦃x : H⦄, x ∈ I → CoalgebraStruct.counit x = 0} {hantipode : ∀ ⦃x : H⦄, x ∈ I → (HopfAlgebraStruct.antipode R) x ∈ I} {x : H} : x ∈ ofIdeal I hcomul hcounit hantipode ↔ x ∈ I

def TauCeti.HopfIdeal.ofSpan {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] (S : Set H) [hS : (Ideal.span S).IsTwoSided] (hcomul : ∀ x ∈ S, CoalgebraStruct.comul x ∈ leftTensorIdeal R H (Ideal.span S) ⊔ rightTensorIdeal R H (Ideal.span S)) (hcounit : ∀ x ∈ S, CoalgebraStruct.counit x = 0) (hantipode : ∀ x ∈ S, (HopfAlgebraStruct.antipode R) x ∈ Ideal.span S) : HopfIdeal R H

Construct the Hopf ideal spanned by a set of generators by checking the three Hopf-ideal closure conditions only on those generators.

Equations

• TauCeti.HopfIdeal.ofSpan S hcomul hcounit hantipode = TauCeti.HopfIdeal.ofIdeal (Ideal.span S) ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.HopfIdeal.ofSpan_toIdeal {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] (S : Set H) [hS : (Ideal.span S).IsTwoSided] (hcomul : ∀ x ∈ S, CoalgebraStruct.comul x ∈ leftTensorIdeal R H (Ideal.span S) ⊔ rightTensorIdeal R H (Ideal.span S)) (hcounit : ∀ x ∈ S, CoalgebraStruct.counit x = 0) (hantipode : ∀ x ∈ S, (HopfAlgebraStruct.antipode R) x ∈ Ideal.span S) : (ofSpan S hcomul hcounit hantipode).toIdeal = Ideal.span S

The ideal underlying ofSpan S is the ideal span of S.

theorem TauCeti.HopfIdeal.comul_mem {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] (I : HopfIdeal R H) {x : H} (hx : x ∈ I) : CoalgebraStruct.comul x ∈ leftTensorIdeal R H I.toIdeal ⊔ rightTensorIdeal R H I.toIdeal

The comultiplication of an element of a Hopf ideal lies in I ⊗ H + H ⊗ I.

theorem TauCeti.HopfIdeal.counit_eq_zero {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] (I : HopfIdeal R H) {x : H} (hx : x ∈ I) : CoalgebraStruct.counit x = 0

The counit vanishes on a Hopf ideal.

theorem TauCeti.HopfIdeal.antipode_mem {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] (I : HopfIdeal R H) {x : H} (hx : x ∈ I) : (HopfAlgebraStruct.antipode R) x ∈ I

The antipode preserves a Hopf ideal.

theorem TauCeti.HopfIdeal.mul_mem_right {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] (I : HopfIdeal R H) {x : H} (hx : x ∈ I) (y : H) : x * y ∈ I

A Hopf ideal absorbs multiplication on the right as well as on the left.

@[instance_reducible]

instance TauCeti.HopfIdeal.instBot {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] : Bot (HopfIdeal R H)

The zero ideal as a Hopf ideal.

Equations

• TauCeti.HopfIdeal.instBot = { bot := { carrier := ⊥, isTwoSided' := ⋯, comul_mem' := ⋯, counit_eq_zero' := ⋯, antipode_mem' := ⋯ } }

@[simp]

theorem TauCeti.HopfIdeal.bot_toIdeal {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] : ⊥.toIdeal = ⊥

@[simp]

theorem TauCeti.HopfIdeal.mem_bot {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] {x : H} : x ∈ ⊥ ↔ x = 0

@[instance_reducible]

instance TauCeti.HopfIdeal.instOrderBot {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] : OrderBot (HopfIdeal R H)

The zero Hopf ideal is contained in every Hopf ideal.

Equations

• TauCeti.HopfIdeal.instOrderBot = { toBot := TauCeti.HopfIdeal.instBot, bot_le := ⋯ }

@[instance_reducible]

instance TauCeti.HopfIdeal.instMax {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] : Max (HopfIdeal R H)

The sum of two Hopf ideals is a Hopf ideal.

Equations

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

@[simp]

theorem TauCeti.HopfIdeal.sup_toIdeal {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] (I J : HopfIdeal R H) : (I ⊔ J).toIdeal = I.toIdeal ⊔ J.toIdeal

The underlying ideal of the join of two Hopf ideals is the join of their underlying ideals.

theorem TauCeti.HopfIdeal.mem_sup {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] {I J : HopfIdeal R H} {x : H} : x ∈ I ⊔ J ↔ ∃ y ∈ I, ∃ z ∈ J, y + z = x

Membership in the join of two Hopf ideals.

@[instance_reducible]

instance TauCeti.HopfIdeal.instSemilatticeSup {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] : SemilatticeSup (HopfIdeal R H)

Hopf ideals form a semilattice under ideal sum, with ⊔ given by the sum construction.

Equations

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

@[instance_reducible]

instance TauCeti.HopfIdeal.instSupSet {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] : SupSet (HopfIdeal R H)

The supremum of a set of Hopf ideals has underlying ideal the supremum of the underlying ideals. The four proof obligations are the implementation of this construction, so they are discharged inline rather than as standalone lemmas.

Equations

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

@[simp]

theorem TauCeti.HopfIdeal.sSup_toIdeal {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] (S : Set (HopfIdeal R H)) : (sSup S).toIdeal = ⨆ (I : ↑S), (↑I).toIdeal

The underlying ideal of a supremum of a set of Hopf ideals is the supremum of the underlying ideals indexed by that set.

theorem TauCeti.HopfIdeal.mem_sSup {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] {S : Set (HopfIdeal R H)} {x : H} : x ∈ sSup S ↔ ∃ (f : ↑S →₀ H), (∀ (I : ↑S), f I ∈ ↑I) ∧ (f.sum fun (x : ↑S) (y : H) => y) = x

Membership in the supremum of a set of Hopf ideals.

@[simp]

theorem TauCeti.HopfIdeal.iSup_toIdeal {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] {ι : Sort u_1} (I : ι → HopfIdeal R H) : (⨆ (i : ι), I i).toIdeal = ⨆ (i : ι), (I i).toIdeal

The underlying ideal of a supremum of a family of Hopf ideals is the supremum of the underlying ideals.

theorem TauCeti.HopfIdeal.mem_iSup {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] {ι : Type u_1} {I : ι → HopfIdeal R H} {x : H} : x ∈ ⨆ (i : ι), I i ↔ ∃ (f : ι →₀ H), (∀ (i : ι), f i ∈ I i) ∧ (f.sum fun (x : ι) (y : H) => y) = x

Membership in the supremum of a family of Hopf ideals.

@[instance_reducible]

instance TauCeti.HopfIdeal.instCompleteSemilatticeSup {R : Type u} {H : Type v} [CommSemiring R] [Semiring H] [HopfAlgebra R H] : CompleteSemilatticeSup (HopfIdeal R H)

Hopf ideals have arbitrary suprema, computed on underlying ideals.

Equations

• TauCeti.HopfIdeal.instCompleteSemilatticeSup = { toPartialOrder := TauCeti.HopfIdeal.instPartialOrder, toSupSet := TauCeti.HopfIdeal.instSupSet, isLUB_sSup := ⋯ }

instance TauCeti.HopfIdeal.instIsCoideal {R : Type u} {H : Type v} [CommRing R] [Ring H] [HopfAlgebra R H] (I : HopfIdeal R H) : (Submodule.restrictScalars R I.toIdeal).IsCoideal

A HopfIdeal gives Mathlib's coideal structure on the underlying R-submodule, so that Mathlib's quotient Coalgebra/Bialgebra instances fire on H ⧸ I.toIdeal.

instance TauCeti.HopfIdeal.instIsHopfIdeal {R : Type u} {H : Type v} [CommRing R] [Ring H] [HopfAlgebra R H] (I : HopfIdeal R H) : Ideal.IsHopfIdeal R I.toIdeal

A HopfIdeal gives Mathlib's Ideal.IsHopfIdeal, so that Mathlib's quotient HopfAlgebra instance fires on H ⧸ I.toIdeal.

theorem TauCeti.HopfIdeal.ker_tensorProduct_map_eq_leftTensorIdeal_sup_rightTensorIdeal {R : Type u} {H : Type v} [CommRing R] [Ring H] [Algebra R H] {A : Type u_1} {B : Type u_2} [Ring A] [Ring B] [Algebra R A] [Algebra R B] (f : H →ₐ[R] A) (g : H →ₐ[R] B) (hf : Function.Surjective ⇑f) (hg : Function.Surjective ⇑g) : RingHom.ker (Algebra.TensorProduct.map f g) = leftTensorIdeal R H (RingHom.ker f) ⊔ rightTensorIdeal R H (RingHom.ker g)

The tensor-kernel exactness theorem in the tensor-ideal notation used by HopfIdeal.