The equalizer Hopf ideal of two bialgebra morphisms

Let f g : H →ₐc[R] K be two bialgebra morphisms into a ring K. The left ideal of K generated by the differences f a - g a needs no antipode to be formed. When K is commutative and H and K are Hopf algebras, it is a Hopf ideal. The quotient K ⧸ I then corepresents the subfunctor of points of K on which the two morphisms induce the same map.

When H is also commutative, f and g are contravariantly two homomorphisms of affine group schemes Spec K ⟶ Spec H, and this Hopf ideal cuts out their equalizer as a closed subgroup scheme of Spec K. The three closure conditions are the structural compatibilities of a bialgebra morphism: the counit condition because ε(f a - g a) = ε(a) - ε(a), the antipode condition because a bialgebra morphism between Hopf algebras commutes with the antipodes, and the comultiplication condition because

f a₁ ⊗ f a₂ - g a₁ ⊗ g a₂ = (f a₁ - g a₁) ⊗ f a₂ + g a₁ ⊗ (f a₂ - g a₂)

splits a difference of pure tensors across the two summands of I ⊗ K + K ⊗ I.

Main declarations

• TauCeti.HopfIdeal.equalizerIdeal: the underlying ideal, generated by the differences.
• TauCeti.HopfIdeal.equalizer: the equalizer Hopf ideal.
• TauCeti.HopfIdeal.equalizerIdeal_le_ker_iff: a ring homomorphism kills the ideal exactly when it identifies the two morphisms; on points, this is the equalizer condition.
• TauCeti.HopfIdeal.equalizer_eq_bot_iff: the equalizer Hopf ideal vanishes exactly when the two morphisms are equal, which is the separation statement used downstream.

References

The construction is the coordinate-algebra form of the scheme-theoretic equalizer of two group homomorphisms; see Milne, Algebraic Groups, §1.h, and Waterhouse, Introduction to Affine Group Schemes, §15. The resulting equalizer ideal gives a separation criterion for homomorphisms out of a group scheme generated by closed subgroups.

def TauCeti.HopfIdeal.equalizerIdeal {R : Type u} [CommSemiring R] {H : Type v} {K : Type w} [Semiring H] [Ring K] [Bialgebra R H] [Bialgebra R K] (f g : H →ₐc[R] K) : Ideal K

The left ideal of K generated by all differences f a - g a of two bialgebra morphisms into a ring.

Equations

• TauCeti.HopfIdeal.equalizerIdeal f g = Ideal.span (Set.range fun (a : H) => f a - g a)

theorem TauCeti.HopfIdeal.sub_mem_equalizerIdeal {R : Type u} [CommSemiring R] {H : Type v} {K : Type w} [Semiring H] [Ring K] [Bialgebra R H] [Bialgebra R K] (f g : H →ₐc[R] K) (a : H) : f a - g a ∈ equalizerIdeal f g

Every difference of values of the two morphisms lies in the equalizer ideal.

theorem TauCeti.HopfIdeal.equalizerIdeal_le_iff {R : Type u} [CommSemiring R] {H : Type v} {K : Type w} [Semiring H] [Ring K] [Bialgebra R H] [Bialgebra R K] {f g : H →ₐc[R] K} {J : Ideal K} : equalizerIdeal f g ≤ J ↔ ∀ (a : H), f a - g a ∈ J

The equalizer ideal is the smallest ideal containing all differences: its universal property.

theorem TauCeti.HopfIdeal.equalizerIdeal_le_ker_iff {R : Type u} [CommSemiring R] {H : Type v} {K : Type w} [Semiring H] [Ring K] [Bialgebra R H] [Bialgebra R K] {A : Type u_1} [Ring A] {f g : H →ₐc[R] K} (φ : K →+* A) : equalizerIdeal f g ≤ RingHom.ker φ ↔ ∀ (a : H), φ (f a) = φ (g a)

A ring homomorphism out of K kills the equalizer ideal exactly when it identifies the two morphisms. Applied to a point K →ₐ[R] A, this is the defining condition of the equalizer subfunctor.

theorem TauCeti.HopfIdeal.equalizerIdeal_comm {R : Type u} [CommSemiring R] {H : Type v} {K : Type w} [Semiring H] [Ring K] [Bialgebra R H] [Bialgebra R K] (f g : H →ₐc[R] K) : equalizerIdeal f g = equalizerIdeal g f

The equalizer ideal is symmetric in the two morphisms.

@[simp]

theorem TauCeti.HopfIdeal.equalizerIdeal_self {R : Type u} [CommSemiring R] {H : Type v} {K : Type w} [Semiring H] [Ring K] [Bialgebra R H] [Bialgebra R K] (f : H →ₐc[R] K) : equalizerIdeal f f = ⊥

The equalizer ideal of a morphism with itself is zero.

def TauCeti.HopfIdeal.equalizer {R : Type u} [CommRing R] {H : Type v} {K : Type w} [Semiring H] [CommRing K] [HopfAlgebra R H] [HopfAlgebra R K] (f g : H →ₐc[R] K) : HopfIdeal R K

The equalizer Hopf ideal of two bialgebra morphisms into a commutative Hopf algebra.

When H is commutative, the quotient by this Hopf ideal is the coordinate algebra of the closed subgroup scheme of Spec K on which the two induced homomorphisms of affine group schemes agree.

Equations

• TauCeti.HopfIdeal.equalizer f g = TauCeti.HopfIdeal.ofSpan (Set.range fun (a : H) => f a - g a) ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.HopfIdeal.equalizer_toIdeal {R : Type u} [CommRing R] {H : Type v} {K : Type w} [Semiring H] [CommRing K] [HopfAlgebra R H] [HopfAlgebra R K] {f g : H →ₐc[R] K} : (equalizer f g).toIdeal = equalizerIdeal f g

The underlying ideal of the equalizer Hopf ideal is the ideal generated by the differences.

@[simp]

theorem TauCeti.HopfIdeal.mem_equalizer {R : Type u} [CommRing R] {H : Type v} {K : Type w} [Semiring H] [CommRing K] [HopfAlgebra R H] [HopfAlgebra R K] {f g : H →ₐc[R] K} {x : K} : x ∈ equalizer f g ↔ x ∈ equalizerIdeal f g

theorem TauCeti.HopfIdeal.sub_mem_equalizer {R : Type u} [CommRing R] {H : Type v} {K : Type w} [Semiring H] [CommRing K] [HopfAlgebra R H] [HopfAlgebra R K] {f g : H →ₐc[R] K} (a : H) : f a - g a ∈ equalizer f g

Every difference of values of the two morphisms lies in the equalizer Hopf ideal.

theorem TauCeti.HopfIdeal.equalizer_le_iff {R : Type u} [CommRing R] {H : Type v} {K : Type w} [Semiring H] [CommRing K] [HopfAlgebra R H] [HopfAlgebra R K] {f g : H →ₐc[R] K} {J : HopfIdeal R K} : equalizer f g ≤ J ↔ ∀ (a : H), f a - g a ∈ J

The equalizer Hopf ideal is the smallest Hopf ideal containing all differences.

theorem TauCeti.HopfIdeal.equalizer_le_ker_iff {R : Type u} [CommRing R] {H : Type v} {K : Type w} [Semiring H] [CommRing K] [HopfAlgebra R H] [HopfAlgebra R K] {f g : H →ₐc[R] K} {A : Type u_1} [Ring A] (φ : K →+* A) : (equalizer f g).toIdeal ≤ RingHom.ker φ ↔ ∀ (a : H), φ (f a) = φ (g a)

Composing with a ring homomorphism that kills the equalizer Hopf ideal identifies the two morphisms, and conversely.

@[simp]

theorem TauCeti.HopfIdeal.equalizer_self {R : Type u} [CommRing R] {H : Type v} {K : Type w} [Semiring H] [CommRing K] [HopfAlgebra R H] [HopfAlgebra R K] (f : H →ₐc[R] K) : equalizer f f = ⊥

The equalizer of a morphism with itself is the zero Hopf ideal.

theorem TauCeti.HopfIdeal.equalizer_comm {R : Type u} [CommRing R] {H : Type v} {K : Type w} [Semiring H] [CommRing K] [HopfAlgebra R H] [HopfAlgebra R K] {f g : H →ₐc[R] K} : equalizer f g = equalizer g f

The equalizer Hopf ideal is symmetric in the two morphisms.

@[simp]

theorem TauCeti.HopfIdeal.equalizer_eq_bot_iff {R : Type u} [CommRing R] {H : Type v} {K : Type w} [Semiring H] [CommRing K] [HopfAlgebra R H] [HopfAlgebra R K] {f g : H →ₐc[R] K} : equalizer f g = ⊥ ↔ f = g

Separation. The equalizer Hopf ideal vanishes exactly when the two morphisms agree. This is the form used to prove that a homomorphism out of a group generated by a family of subgroups is determined by its restrictions.