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. The quotient of K by TauCeti.CommHopfAlgCat.equalizerHopfIdeal represents the closed subgroup scheme of Spec K on which the two agree, and this file records the resulting cone.

equalizerSpecι is a closed immersion equalizing the two homomorphisms, and it is universal among homomorphisms of affine group schemes into Spec K that do so: such a homomorphism factors through equalizerSpec in exactly one way. The factorization is the image under hopfSpec of the coequalizer factorization on coordinate Hopf algebras, and its uniqueness comes from full faithfulness of hopfSpec together with uniqueness of that factorization.

Main declarations

• TauCeti.CommHopfAlgCat.equalizerSpec and TauCeti.CommHopfAlgCat.equalizerSpecι: the equalizer as a closed subgroup scheme of Spec K, together with its closed immersion.
• TauCeti.CommHopfAlgCat.equalizerSpecι_comp_hopfSpec_map: the equalizing equation.
• TauCeti.CommHopfAlgCat.liftEqualizerSpec, with TauCeti.CommHopfAlgCat.liftEqualizerSpec_comp_equalizerSpecι and TauCeti.CommHopfAlgCat.liftEqualizerSpec_unique: the universal property of that cone among affine group schemes.

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. It serves TauCetiRoadmap/ReductiveGroups/README.md, "Hopf ideals ↔ closed subgroup schemes".

@[reducible, inline]

noncomputable abbrev TauCeti.CommHopfAlgCat.equalizerSpec {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f g : H ⟶ K) : CategoryTheory.Grp (CategoryTheory.Over (AlgebraicGeometry.Spec ↧R))

The equalizer group scheme of two homomorphisms of affine group schemes: the closed subgroup scheme of Spec K cut out by the equalizer Hopf ideal.

Equations

• TauCeti.CommHopfAlgCat.equalizerSpec f g = TauCeti.CommHopfAlgCat.quotientSpec K (TauCeti.CommHopfAlgCat.equalizerHopfIdeal f g)

noncomputable def TauCeti.CommHopfAlgCat.equalizerSpecι {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f g : H ⟶ K) : equalizerSpec f g ⟶ (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op K)

The inclusion of the equalizer group scheme into Spec K.

Equations

• TauCeti.CommHopfAlgCat.equalizerSpecι f g = TauCeti.CommHopfAlgCat.quotientSpecι K (TauCeti.CommHopfAlgCat.equalizerHopfIdeal f g)

theorem TauCeti.CommHopfAlgCat.equalizerSpecι_def {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f g : H ⟶ K) : equalizerSpecι f g = quotientSpecι K (equalizerHopfIdeal f g)

equalizerSpecι is the inclusion of the quotient by the equalizer Hopf ideal.

instance TauCeti.CommHopfAlgCat.isClosedImmersion_equalizerSpecι {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f g : H ⟶ K) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Over.Hom.left (equalizerSpecι f g).hom.hom)

The equalizer is a closed subgroup scheme of Spec K.

theorem TauCeti.CommHopfAlgCat.equalizerSpecι_comp_hopfSpec_map {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f g : H ⟶ K) : CategoryTheory.CategoryStruct.comp (equalizerSpecι f g) ((AlgebraicGeometry.hopfSpec ↧R).map f.op) = CategoryTheory.CategoryStruct.comp (equalizerSpecι f g) ((AlgebraicGeometry.hopfSpec ↧R).map g.op)

The equalizer group scheme equalizes the two homomorphisms of affine group schemes.

noncomputable def TauCeti.CommHopfAlgCat.liftEqualizerSpec {R : Type u} [CommRing R] {H K Y : CommHopfAlgCat R} (f g : H ⟶ K) (q : (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op Y) ⟶ (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op K)) (hq : CategoryTheory.CategoryStruct.comp q ((AlgebraicGeometry.hopfSpec ↧R).map f.op) = CategoryTheory.CategoryStruct.comp q ((AlgebraicGeometry.hopfSpec ↧R).map g.op)) : (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op Y) ⟶ equalizerSpec f g

The universal property of the equalizer: a homomorphism of affine group schemes into Spec K equalizing f and g factors through the equalizer group scheme.

Equations

• TauCeti.CommHopfAlgCat.liftEqualizerSpec f g q hq = (AlgebraicGeometry.hopfSpec ↧R).map (TauCeti.CommHopfAlgCat.liftEqualizer (AlgebraicGeometry.hopfSpec.fullyFaithful.preimage q).unop ⋯).op

@[simp]

theorem TauCeti.CommHopfAlgCat.liftEqualizerSpec_comp_equalizerSpecι {R : Type u} [CommRing R] {H K Y : CommHopfAlgCat R} (f g : H ⟶ K) (q : (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op Y) ⟶ (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op K)) (hq : CategoryTheory.CategoryStruct.comp q ((AlgebraicGeometry.hopfSpec ↧R).map f.op) = CategoryTheory.CategoryStruct.comp q ((AlgebraicGeometry.hopfSpec ↧R).map g.op)) : CategoryTheory.CategoryStruct.comp (liftEqualizerSpec f g q hq) (equalizerSpecι f g) = q

The factorization law of the equalizer: liftEqualizerSpec followed by the inclusion of the equalizer is the original homomorphism.

theorem TauCeti.CommHopfAlgCat.liftEqualizerSpec_unique {R : Type u} [CommRing R] {H K Y : CommHopfAlgCat R} (f g : H ⟶ K) (q : (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op Y) ⟶ (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op K)) (hq : CategoryTheory.CategoryStruct.comp q ((AlgebraicGeometry.hopfSpec ↧R).map f.op) = CategoryTheory.CategoryStruct.comp q ((AlgebraicGeometry.hopfSpec ↧R).map g.op)) (m : (AlgebraicGeometry.hopfSpec ↧R).obj (Opposite.op Y) ⟶ equalizerSpec f g) (hm : CategoryTheory.CategoryStruct.comp m (equalizerSpecι f g) = q) : m = liftEqualizerSpec f g q hq

The uniqueness law of the equalizer: liftEqualizerSpec is the only factorization of q through the inclusion of the equalizer group scheme.