Documentation

TauCeti.AlgebraicGeometry.GroupScheme.Kernel

Kernels of group schemes #

This file constructs the scheme-theoretic kernel of an arbitrary homomorphism of group schemes over an arbitrary base. It is the categorical kernel in Grp (Over S), equivalently the fibre of the homomorphism over the identity section. No affineness, finiteness, or flatness hypothesis is imposed.

Formation of this kernel commutes with arbitrary base change. Categorically, this follows because pullback of schemes over a base preserves limits, limits of group objects are created by the forgetful functor, and that functor reflects limits. The comparison isomorphism is Mathlib's canonical PreservesKernel.iso; its compatibility with inclusions and maps between kernels is recorded explicitly for downstream use.

Main declarations #

The categorical kernel and comparison constructions are provided by Mathlib.CategoryTheory.Limits.Shapes.Kernels and Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels.

source
instance TauCeti.GroupScheme.pullbackMapGrp_preservesLimitsOfShape_walkingParallelPair {S T : AlgebraicGeometry.Scheme} (s : T ⟶ S) :
CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.Over.pullback s).mapGrp

Pullback of group schemes along an arbitrary base morphism preserves parallel-pair limits. In particular, it preserves kernels.

source
noncomputable def TauCeti.GroupScheme.kernelBaseChangeIso {S T : AlgebraicGeometry.Scheme} (s : T ⟶ S) {G H : CategoryTheory.Grp (CategoryTheory.Over S)} (f : G ⟶ H) :
(CategoryTheory.Over.pullback s).mapGrp.obj (CategoryTheory.Limits.kernel f) ≅ CategoryTheory.Limits.kernel ((CategoryTheory.Over.pullback s).mapGrp.map f)

The canonical isomorphism from the base change of a scheme-theoretic kernel to the kernel of the base-changed homomorphism.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.GroupScheme.kernelBaseChangeIso_hom_comp_ι {S T : AlgebraicGeometry.Scheme} (s : T ⟶ S) {G H : CategoryTheory.Grp (CategoryTheory.Over S)} (f : G ⟶ H) :
    CategoryTheory.CategoryStruct.comp (kernelBaseChangeIso s f).hom (CategoryTheory.Limits.kernel.ι ((CategoryTheory.Over.pullback s).mapGrp.map f)) = (CategoryTheory.Over.pullback s).mapGrp.map (CategoryTheory.Limits.kernel.ι f)

    The forward base-change comparison intertwines the two kernel inclusions.

    source
    @[simp]
    theorem TauCeti.GroupScheme.kernelBaseChangeIso_hom_comp_ι_assoc {S T : AlgebraicGeometry.Scheme} (s : T ⟶ S) {G H : CategoryTheory.Grp (CategoryTheory.Over S)} (f : G ⟶ H) {Z : CategoryTheory.Grp (CategoryTheory.Over T)} (h : (CategoryTheory.Over.pullback s).mapGrp.obj G ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (kernelBaseChangeIso s f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι ((CategoryTheory.Over.pullback s).mapGrp.map f)) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Over.pullback s).mapGrp.map (CategoryTheory.Limits.kernel.ι f)) h

    The forward base-change comparison intertwines the two kernel inclusions.

    source
    @[simp]
    theorem TauCeti.GroupScheme.kernelBaseChangeIso_inv_comp_ι {S T : AlgebraicGeometry.Scheme} (s : T ⟶ S) {G H : CategoryTheory.Grp (CategoryTheory.Over S)} (f : G ⟶ H) :
    CategoryTheory.CategoryStruct.comp (kernelBaseChangeIso s f).inv ((CategoryTheory.Over.pullback s).mapGrp.map (CategoryTheory.Limits.kernel.ι f)) = CategoryTheory.Limits.kernel.ι ((CategoryTheory.Over.pullback s).mapGrp.map f)

    The inverse base-change comparison intertwines the two kernel inclusions.

    source
    @[simp]
    theorem TauCeti.GroupScheme.kernelBaseChangeIso_inv_comp_ι_assoc {S T : AlgebraicGeometry.Scheme} (s : T ⟶ S) {G H : CategoryTheory.Grp (CategoryTheory.Over S)} (f : G ⟶ H) {Z : CategoryTheory.Grp (CategoryTheory.Over T)} (h : (CategoryTheory.Over.pullback s).mapGrp.obj G ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (kernelBaseChangeIso s f).inv (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Over.pullback s).mapGrp.map (CategoryTheory.Limits.kernel.ι f)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι ((CategoryTheory.Over.pullback s).mapGrp.map f)) h

    The inverse base-change comparison intertwines the two kernel inclusions.

    source
    theorem TauCeti.GroupScheme.kernelMap_comp_kernelBaseChangeIso_inv {S T : AlgebraicGeometry.Scheme} (s : T ⟶ S) {G₁ H₁ G₂ H₂ : CategoryTheory.Grp (CategoryTheory.Over S)} (f₁ : G₁ ⟶ H₁) (f₂ : G₂ ⟶ H₂) (g : G₁ ⟶ G₂) (h : H₁ ⟶ H₂) (w : CategoryTheory.CategoryStruct.comp f₁ h = CategoryTheory.CategoryStruct.comp g f₂) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.map ((CategoryTheory.Over.pullback s).mapGrp.map f₁) ((CategoryTheory.Over.pullback s).mapGrp.map f₂) ((CategoryTheory.Over.pullback s).mapGrp.map g) ((CategoryTheory.Over.pullback s).mapGrp.map h) ⋯) (kernelBaseChangeIso s f₂).inv = CategoryTheory.CategoryStruct.comp (kernelBaseChangeIso s f₁).inv ((CategoryTheory.Over.pullback s).mapGrp.map (CategoryTheory.Limits.kernel.map f₁ f₂ g h w))

    The base-change comparison for kernels is natural in commutative squares of group-scheme homomorphisms.

    source
    theorem TauCeti.GroupScheme.kernelMap_comp_kernelBaseChangeIso_inv_assoc {S T : AlgebraicGeometry.Scheme} (s : T ⟶ S) {G₁ H₁ G₂ H₂ : CategoryTheory.Grp (CategoryTheory.Over S)} (f₁ : G₁ ⟶ H₁) (f₂ : G₂ ⟶ H₂) (g : G₁ ⟶ G₂) (h : H₁ ⟶ H₂) (w : CategoryTheory.CategoryStruct.comp f₁ h = CategoryTheory.CategoryStruct.comp g f₂) {Z : CategoryTheory.Grp (CategoryTheory.Over T)} (h✝ : (CategoryTheory.Over.pullback s).mapGrp.obj (CategoryTheory.Limits.kernel f₂) ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.map ((CategoryTheory.Over.pullback s).mapGrp.map f₁) ((CategoryTheory.Over.pullback s).mapGrp.map f₂) ((CategoryTheory.Over.pullback s).mapGrp.map g) ((CategoryTheory.Over.pullback s).mapGrp.map h) ⋯) (CategoryTheory.CategoryStruct.comp (kernelBaseChangeIso s f₂).inv h✝) = CategoryTheory.CategoryStruct.comp (kernelBaseChangeIso s f₁).inv (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Over.pullback s).mapGrp.map (CategoryTheory.Limits.kernel.map f₁ f₂ g h w)) h✝)

    The base-change comparison for kernels is natural in commutative squares of group-scheme homomorphisms.

    source
    theorem TauCeti.GroupScheme.isPullback_kernel {S : AlgebraicGeometry.Scheme} {G H : CategoryTheory.Grp (CategoryTheory.Over S)} (f : G ⟶ H) :
    CategoryTheory.IsPullback (CategoryTheory.Limits.kernel.ι f) 0 f 0

    The categorical kernel of a group-scheme homomorphism is its fibre over the identity section. The horizontal maps are the kernel inclusion and the identity section; the other map from the kernel is the unique morphism to the trivial group scheme.

    source
    theorem TauCeti.GroupScheme.isPullback_kernel_scheme {S : AlgebraicGeometry.Scheme} {G H : CategoryTheory.Grp (CategoryTheory.Over S)} (f : G ⟶ H) :
    CategoryTheory.IsPullback (CategoryTheory.Over.Hom.left (CategoryTheory.Limits.kernel.ι f).hom.hom) (CategoryTheory.Over.Hom.left (CategoryTheory.InducedCategory.Hom.hom 0).hom) (CategoryTheory.Over.Hom.left f.hom.hom) (CategoryTheory.Over.Hom.left (CategoryTheory.InducedCategory.Hom.hom 0).hom)

    On underlying schemes, the scheme-theoretic kernel is the fibre of the homomorphism over its identity section.

    source
    noncomputable def TauCeti.GroupScheme.kernelBaseChangeSchemeIso {S T : AlgebraicGeometry.Scheme} (s : T ⟶ S) {G H : CategoryTheory.Grp (CategoryTheory.Over S)} (f : G ⟶ H) :
    ((CategoryTheory.Over.pullback s).mapGrp.obj (CategoryTheory.Limits.kernel f)).X.left ≅ (CategoryTheory.Limits.kernel ((CategoryTheory.Over.pullback s).mapGrp.map f)).X.left

    The underlying-scheme isomorphism from the base change of a scheme-theoretic kernel to the kernel of the base-changed homomorphism.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem TauCeti.GroupScheme.kernelBaseChangeSchemeIso_hom_comp_ι {S T : AlgebraicGeometry.Scheme} (s : T ⟶ S) {G H : CategoryTheory.Grp (CategoryTheory.Over S)} (f : G ⟶ H) :
      CategoryTheory.CategoryStruct.comp (kernelBaseChangeSchemeIso s f).hom (CategoryTheory.Over.Hom.left (CategoryTheory.Limits.kernel.ι ((CategoryTheory.Over.pullback s).mapGrp.map f)).hom.hom) = CategoryTheory.Over.Hom.left ((CategoryTheory.Over.pullback s).mapGrp.map (CategoryTheory.Limits.kernel.ι f)).hom.hom

      The forward underlying-scheme comparison intertwines the two kernel inclusions.

      source
      @[simp]
      theorem TauCeti.GroupScheme.kernelBaseChangeSchemeIso_hom_comp_ι_assoc {S T : AlgebraicGeometry.Scheme} (s : T ⟶ S) {G H : CategoryTheory.Grp (CategoryTheory.Over S)} (f : G ⟶ H) {Z : AlgebraicGeometry.Scheme} (h : ((CategoryTheory.Over.pullback s).mapGrp.obj G).X.left ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (kernelBaseChangeSchemeIso s f).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (CategoryTheory.Limits.kernel.ι ((CategoryTheory.Over.pullback s).mapGrp.map f)).hom.hom) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left ((CategoryTheory.Over.pullback s).mapGrp.map (CategoryTheory.Limits.kernel.ι f)).hom.hom) h

      The forward underlying-scheme comparison intertwines the two kernel inclusions.

      source
      @[simp]
      theorem TauCeti.GroupScheme.kernelBaseChangeSchemeIso_inv_comp_ι {S T : AlgebraicGeometry.Scheme} (s : T ⟶ S) {G H : CategoryTheory.Grp (CategoryTheory.Over S)} (f : G ⟶ H) :
      CategoryTheory.CategoryStruct.comp (kernelBaseChangeSchemeIso s f).inv (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.kernel f).X.hom s) (CategoryTheory.Over.Hom.left (CategoryTheory.Limits.kernel.ι f).hom.hom)) (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.kernel f).X.hom s) ⋯) = CategoryTheory.Over.Hom.left (CategoryTheory.Limits.kernel.ι ((CategoryTheory.Over.pullback s).mapGrp.map f)).hom.hom

      The inverse underlying-scheme comparison intertwines the two kernel inclusions.

      source
      @[simp]
      theorem TauCeti.GroupScheme.kernelBaseChangeSchemeIso_inv_comp_ι_assoc {S T : AlgebraicGeometry.Scheme} (s : T ⟶ S) {G H : CategoryTheory.Grp (CategoryTheory.Over S)} (f : G ⟶ H) {Z : AlgebraicGeometry.Scheme} (h : CategoryTheory.Limits.pullback G.X.hom s ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (kernelBaseChangeSchemeIso s f).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.kernel f).X.hom s) (CategoryTheory.Over.Hom.left (CategoryTheory.Limits.kernel.ι f).hom.hom)) (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.kernel f).X.hom s) ⋯) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left (CategoryTheory.Limits.kernel.ι ((CategoryTheory.Over.pullback s).mapGrp.map f)).hom.hom) h

      The inverse underlying-scheme comparison intertwines the two kernel inclusions.