Kernels of composite affine group morphisms #

For affine group morphisms G → H → Q, restriction gives ker(G → Q) → ker(H → Q). Its scheme-theoretic kernel is ker(G → H). If G → H is faithfully flat and finitely presented, so is this restriction, giving the short exact sequence of kernels in the fppf topology. We construct the restriction in Hopf coordinates and identify its kernel ideal.

All statements hold over an arbitrary commutative base ring, including for nonreduced groups. The coordinates of the restriction are obtained by base change along the quotient defining ker(H → Q).

References #

J. S. Milne, Algebraic Groups (2017), §5, exact sequences of affine groups.

source

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

quotient K (kernelHopfIdeal f) ⟶ quotient L (kernelHopfIdeal (CategoryTheory.CategoryStruct.comp f g))

The coordinate morphism of the restriction ker(Spec L → Spec H) → ker(Spec K → Spec H) of the group morphism represented by g.

Equations

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

Instances For

source

@[simp]

theorem TauCeti.CommHopfAlgCat.kernelCompositeMap_mk {R : Type u} [CommRing R] {H K L : CommHopfAlgCat R} (f : H ⟶ K) (g : K ⟶ L) (x : ↑K) :

(CommHopfAlgCat.Hom.hom (kernelCompositeMap f g)) ((Ideal.Quotient.mk (kernelHopfIdeal f).toIdeal) x) = (Ideal.Quotient.mk (kernelHopfIdeal (CategoryTheory.CategoryStruct.comp f g)).toIdeal) ((CommHopfAlgCat.Hom.hom g) x)

The restriction on kernels sends a quotient representative to the class of its image.

source

@[simp]

theorem TauCeti.CommHopfAlgCat.mkQuotient_comp_kernelCompositeMap {R : Type u} [CommRing R] {H K L : CommHopfAlgCat R} (f : H ⟶ K) (g : K ⟶ L) :

CategoryTheory.CategoryStruct.comp (mkQuotient K (kernelHopfIdeal f)) (kernelCompositeMap f g) = CategoryTheory.CategoryStruct.comp g (mkQuotient L (kernelHopfIdeal (CategoryTheory.CategoryStruct.comp f g)))

Restriction to kernels commutes with their inclusions into the ambient groups.

source

@[simp]

theorem TauCeti.CommHopfAlgCat.mkQuotient_comp_kernelCompositeMap_assoc {R : Type u} [CommRing R] {H K L : CommHopfAlgCat R} (f : H ⟶ K) (g : K ⟶ L) {Z : CommHopfAlgCat R} (h : quotient L (kernelHopfIdeal (CategoryTheory.CategoryStruct.comp f g)) ⟶ Z) :

CategoryTheory.CategoryStruct.comp (mkQuotient K (kernelHopfIdeal f)) (CategoryTheory.CategoryStruct.comp (kernelCompositeMap f g) h) = CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp (mkQuotient L (kernelHopfIdeal (CategoryTheory.CategoryStruct.comp f g))) h)

Restriction to kernels commutes with their inclusions into the ambient groups.

source

@[simp]

theorem TauCeti.CommHopfAlgCat.kernelCompositeMap_id {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) :

kernelCompositeMap f (CategoryTheory.CategoryStruct.id K) = CategoryTheory.eqToHom ⋯

Restriction along the identity is the identity after identifying its target quotient.

source

@[simp]

theorem TauCeti.CommHopfAlgCat.kernelCompositeMap_comp {R : Type u} [CommRing R] {H K L M : CommHopfAlgCat R} (f : H ⟶ K) (g : K ⟶ L) (h : L ⟶ M) :

CategoryTheory.CategoryStruct.comp (kernelCompositeMap f g) (kernelCompositeMap (CategoryTheory.CategoryStruct.comp f g) h) = CategoryTheory.CategoryStruct.comp (kernelCompositeMap f (CategoryTheory.CategoryStruct.comp g h)) (CategoryTheory.eqToHom ⋯)

Successive restrictions agree with restriction along the composite, after identifying the target quotients by associativity.

source

@[simp]

theorem TauCeti.CommHopfAlgCat.kernelHopfIdeal_kernelCompositeMap {R : Type u} [CommRing R] {H K L : CommHopfAlgCat R} (f : H ⟶ K) (g : K ⟶ L) :

kernelHopfIdeal (kernelCompositeMap f g) = (kernelHopfIdeal g).map (CommHopfAlgCat.Hom.hom (mkQuotient L (kernelHopfIdeal (CategoryTheory.CategoryStruct.comp f g))))

The kernel of the restriction on composite kernels is the original kernel, viewed as a closed subgroup of the composite kernel.

source

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

quotient (quotient L (kernelHopfIdeal (CategoryTheory.CategoryStruct.comp f g))) (kernelHopfIdeal (kernelCompositeMap f g)) ≅ quotient L (kernelHopfIdeal g)

The scheme-theoretic kernel of the restriction on composite kernels is isomorphic to the original kernel, including its possibly nonreduced scheme structure.

Equations