The equalizer of two homomorphisms of affine group schemes

Two morphisms f g : H ⟶ K of commutative Hopf algebras are, contravariantly, two homomorphisms Spec K ⟶ Spec H of affine group schemes. This file cuts out the locus where they agree.

The Hopf ideal equalizerHopfIdeal f g of K is generated by the differences f a - g a. On coordinate algebras the quotient by it is the coequalizer of f and g in the category of commutative Hopf algebras: f ≫ mkQuotient = g ≫ mkQuotient, and every morphism out of K coequalizing the two factors uniquely through the quotient. Contravariantly that is the equalizer of the two homomorphisms of affine group schemes, and because the ideal is a Hopf ideal it is cut out by a closed subgroup scheme rather than a bare subfunctor. The points-level and scheme-level faces of this construction live in TauCeti.Algebra.AlgebraicGroup.HopfIdeal.Points.Equalizer and TauCeti.Algebra.AlgebraicGroup.HopfIdeal.Scheme.Equalizer.

The application is a rigidity principle. If a family p i : H ⟶ K i has vanishing common-kernel Hopf ideal — contravariantly, Spec H is generated as a closed subgroup scheme by the images of the Spec (K i) — then two morphisms into H agreeing after composition with each p i are equal, because their equalizer Hopf ideal is squeezed below the common kernel. Since a common-kernel quotient always has vanishing common kernel for the lifted family, this applies in particular to the group schemes generated by a family of subgroups.

Main declarations

• TauCeti.CommHopfAlgCat.equalizerHopfIdeal: the equalizer Hopf ideal of two morphisms, with TauCeti.CommHopfAlgCat.equalizerHopfIdeal_def, TauCeti.CommHopfAlgCat.equalizerHopfIdeal_toIdeal, TauCeti.CommHopfAlgCat.mem_equalizerHopfIdeal, TauCeti.CommHopfAlgCat.sub_mem_equalizerHopfIdeal and TauCeti.CommHopfAlgCat.equalizerHopfIdeal_le_iff describing it.
• TauCeti.CommHopfAlgCat.equalizerHopfIdeal_le_ker_iff and TauCeti.CommHopfAlgCat.equalizerHopfIdeal_toIdeal_le_ker_iff: a ring homomorphism, respectively a morphism of commutative Hopf algebras, kills the equalizer Hopf ideal exactly when it identifies the two morphisms.
• TauCeti.CommHopfAlgCat.liftEqualizer, with TauCeti.CommHopfAlgCat.mkQuotient_comp_liftEqualizer and TauCeti.CommHopfAlgCat.liftEqualizer_unique: the coequalizer universal property of the quotient by the equalizer Hopf ideal.
• TauCeti.CommHopfAlgCat.hom_ext_of_commonKernelHopfIdeal_eq_bot, TauCeti.CommHopfAlgCat.hom_ext_of_le_iff_forall_toIdeal_le_ker and TauCeti.CommHopfAlgCat.commonKernelLift_hom_ext: the rigidity principle.

References

The equalizer of two homomorphisms of group schemes is a closed subgroup scheme; see Milne, Algebraic Groups, §1.h, and Waterhouse, Introduction to Affine Group Schemes, §15.3. The rigidity principle is the standard argument that a homomorphism out of a group generated by a family of subgroups is determined by its restrictions to them. Its Kostant specialization serves Layer 9's explicit "Chevalley--Demazure construction" and "Root subgroup maps" targets. It does not by itself prove the separate pinned-isomorphism uniqueness statement, which requires generation by the simple root subgroups.

noncomputable def TauCeti.CommHopfAlgCat.equalizerHopfIdeal {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f g : H ⟶ K) : HopfIdeal R ↑K

The equalizer Hopf ideal of two morphisms of commutative Hopf algebras: the Hopf ideal of K generated by the differences f a - g a.

Contravariantly, its quotient is the coordinate algebra of the closed subgroup scheme of Spec K on which the two homomorphisms Spec K ⟶ Spec H agree.

Equations

• TauCeti.CommHopfAlgCat.equalizerHopfIdeal f g = TauCeti.HopfIdeal.equalizer (CommHopfAlgCat.Hom.hom f) (CommHopfAlgCat.Hom.hom g)

theorem TauCeti.CommHopfAlgCat.equalizerHopfIdeal_def {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f g : H ⟶ K) : equalizerHopfIdeal f g = HopfIdeal.equalizer (CommHopfAlgCat.Hom.hom f) (CommHopfAlgCat.Hom.hom g)

The equalizer Hopf ideal is the equalizer Hopf ideal of the underlying bialgebra morphisms.

@[simp]

theorem TauCeti.CommHopfAlgCat.equalizerHopfIdeal_toIdeal {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f g : H ⟶ K) : (equalizerHopfIdeal f g).toIdeal = HopfIdeal.equalizerIdeal (CommHopfAlgCat.Hom.hom f) (CommHopfAlgCat.Hom.hom g)

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

@[simp]

theorem TauCeti.CommHopfAlgCat.mem_equalizerHopfIdeal {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {f g : H ⟶ K} {x : ↑K} : x ∈ equalizerHopfIdeal f g ↔ x ∈ HopfIdeal.equalizerIdeal (CommHopfAlgCat.Hom.hom f) (CommHopfAlgCat.Hom.hom g)

Membership in the equalizer Hopf ideal is membership in the ideal generated by the differences.

theorem TauCeti.CommHopfAlgCat.sub_mem_equalizerHopfIdeal {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f g : H ⟶ K) (a : ↑H) : (CommHopfAlgCat.Hom.hom f) a - (CommHopfAlgCat.Hom.hom g) a ∈ equalizerHopfIdeal f g

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

theorem TauCeti.CommHopfAlgCat.equalizerHopfIdeal_le_iff {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {f g : H ⟶ K} {J : HopfIdeal R ↑K} : equalizerHopfIdeal f g ≤ J ↔ ∀ (a : ↑H), (CommHopfAlgCat.Hom.hom f) a - (CommHopfAlgCat.Hom.hom g) a ∈ J

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

theorem TauCeti.CommHopfAlgCat.equalizerHopfIdeal_le_ker_iff {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {A : Type u_1} [Ring A] (f g : H ⟶ K) (φ : ↑K →+* A) : (equalizerHopfIdeal f g).toIdeal ≤ RingHom.ker φ ↔ ∀ (a : ↑H), φ ((CommHopfAlgCat.Hom.hom f) a) = φ ((CommHopfAlgCat.Hom.hom g) a)

A ring homomorphism out of K kills the equalizer Hopf ideal exactly when it identifies the values of the two morphisms. Applied to an A-point of K this is the equalizer condition on points.

theorem TauCeti.CommHopfAlgCat.equalizerHopfIdeal_toIdeal_le_ker_iff {R : Type u} [CommRing R] {H K T : CommHopfAlgCat R} (f g : H ⟶ K) (p : K ⟶ T) : (equalizerHopfIdeal f g).toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom p)).toRingHom ↔ CategoryTheory.CategoryStruct.comp f p = CategoryTheory.CategoryStruct.comp g p

A morphism out of K kills the equalizer Hopf ideal exactly when it coequalizes the two morphisms. This is the defining property of the ideal, and the source of the coequalizer universal property below.

@[simp]

theorem TauCeti.CommHopfAlgCat.equalizerHopfIdeal_eq_bot_iff {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f g : H ⟶ K) : equalizerHopfIdeal f g = ⊥ ↔ f = g

Separation. The equalizer Hopf ideal vanishes exactly when the two morphisms are equal.

theorem TauCeti.CommHopfAlgCat.comp_mkQuotient_equalizerHopfIdeal {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f g : H ⟶ K) : CategoryTheory.CategoryStruct.comp f (mkQuotient K (equalizerHopfIdeal f g)) = CategoryTheory.CategoryStruct.comp g (mkQuotient K (equalizerHopfIdeal f g))

The quotient by the equalizer Hopf ideal coequalizes the two morphisms.

noncomputable def TauCeti.CommHopfAlgCat.liftEqualizer {R : Type u} [CommRing R] {H K T : CommHopfAlgCat R} {f g : H ⟶ K} (p : K ⟶ T) (hp : CategoryTheory.CategoryStruct.comp f p = CategoryTheory.CategoryStruct.comp g p) : quotient K (equalizerHopfIdeal f g) ⟶ T

The coequalizer universal property on coordinate Hopf algebras: a morphism out of K coequalizing f and g factors through the quotient by the equalizer Hopf ideal.

Contravariantly, this is the factorization of a homomorphism of affine group schemes into Spec K that equalizes the two induced homomorphisms through their equalizer.

Equations

• TauCeti.CommHopfAlgCat.liftEqualizer p hp = TauCeti.CommHopfAlgCat.liftQuotient (TauCeti.CommHopfAlgCat.equalizerHopfIdeal f g) p ⋯

@[simp]

theorem TauCeti.CommHopfAlgCat.mkQuotient_comp_liftEqualizer {R : Type u} [CommRing R] {H K T : CommHopfAlgCat R} {f g : H ⟶ K} (p : K ⟶ T) (hp : CategoryTheory.CategoryStruct.comp f p = CategoryTheory.CategoryStruct.comp g p) : CategoryTheory.CategoryStruct.comp (mkQuotient K (equalizerHopfIdeal f g)) (liftEqualizer p hp) = p

The factorization law of the coequalizer: liftEqualizer p hp restricts along the quotient morphism to p.

theorem TauCeti.CommHopfAlgCat.liftEqualizer_unique {R : Type u} [CommRing R] {H K T : CommHopfAlgCat R} {f g : H ⟶ K} (p : K ⟶ T) (hp : CategoryTheory.CategoryStruct.comp f p = CategoryTheory.CategoryStruct.comp g p) (q : quotient K (equalizerHopfIdeal f g) ⟶ T) (hq : CategoryTheory.CategoryStruct.comp (mkQuotient K (equalizerHopfIdeal f g)) q = p) : q = liftEqualizer p hp

The uniqueness law of the coequalizer: liftEqualizer p hp is the only morphism out of the quotient restricting to p along the quotient morphism.

theorem TauCeti.CommHopfAlgCat.hom_ext_of_commonKernelHopfIdeal_eq_bot {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {ι : Type w} {K : ι → CommHopfAlgCat R} {Y : CommHopfAlgCat R} (p : (i : ι) → H ⟶ K i) (hp : commonKernelHopfIdeal p = ⊥) (u v : Y ⟶ H) (h : ∀ (i : ι), CategoryTheory.CategoryStruct.comp u (p i) = CategoryTheory.CategoryStruct.comp v (p i)) : u = v

Rigidity. A family of morphisms out of H with vanishing common-kernel Hopf ideal is jointly monic: two morphisms into H that agree after composition with every member of the family are equal.

Contravariantly, Spec H is the closed subgroup scheme generated by the images of the Spec (K i), and a homomorphism out of a group generated by a family of subgroups is determined by its restrictions to them.

theorem TauCeti.CommHopfAlgCat.hom_ext_of_le_iff_forall_toIdeal_le_ker {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {ι : Type w} {K : ι → CommHopfAlgCat R} {I : HopfIdeal R ↑H} {p : (i : ι) → H ⟶ K i} (hI : ∀ (J : HopfIdeal R ↑H), J ≤ I ↔ ∀ (i : ι), J.toIdeal ≤ RingHom.ker (↑(CommHopfAlgCat.Hom.hom (p i))).toRingHom) {c : (i : ι) → quotient H I ⟶ K i} (hc : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (mkQuotient H I) (c i) = p i) {Y : CommHopfAlgCat R} (u v : Y ⟶ quotient H I) (h : ∀ (i : ι), CategoryTheory.CategoryStruct.comp u (c i) = CategoryTheory.CategoryStruct.comp v (c i)) : u = v

Rigidity for a presented quotient. Suppose I is the largest Hopf ideal of H killed by every member of a family p, and each p i factors through H ⧸ I as c i. Then two morphisms into H ⧸ I that agree after composition with every c i are equal.

Contravariantly, Spec (H ⧸ I) is the closed subgroup scheme of Spec H generated by the images of the Spec (K i), and a homomorphism out of it is determined by its restrictions to those subgroups. The two hypotheses are exactly the universal property of the generated subgroup and the factorization of each generator through it, so a consumer that has named those two facts need not also expose how its defining ideal was built.

theorem TauCeti.CommHopfAlgCat.commonKernelLift_hom_ext {R : Type u} [CommRing R] {H : CommHopfAlgCat R} {ι : Type w} {K : ι → CommHopfAlgCat R} {Y : CommHopfAlgCat R} (p : (i : ι) → H ⟶ K i) (u v : Y ⟶ quotient H (commonKernelHopfIdeal p)) (h : ∀ (i : ι), CategoryTheory.CategoryStruct.comp u (commonKernelLift p i) = CategoryTheory.CategoryStruct.comp v (commonKernelLift p i)) : u = v

A morphism out of a common-kernel quotient is determined by its composites with the lifted family. This is the rigidity statement in the form a generated closed subgroup scheme uses.