Documentation

TauCeti.AlgebraicGeometry.AffineGroupScheme.Image

Scheme-theoretic images of affine group morphisms #

For a morphism f : H ⟶ K of commutative Hopf algebras over a field, the represented affine group morphism runs from Spec K to Spec H. Its coordinate image is the quotient

H ⟶ H / ker(f) ⟶ K.

This file identifies Spec (H / ker(f)) with Mathlib's scheme-theoretic image of Spec K ⟶ Spec H. The isomorphism carries both maps in the Hopf image factorization to the canonical closed immersion and source factor of the scheme-theoretic image. Thus the existing coordinate construction can be used as an actual closed subgroup scheme, rather than merely as an analogous quotient.

Main declarations #

References #

This is the scheme-side image compatibility required by Layer 3, "Subgroups, quotients, components", of the ReductiveGroups roadmap. It is also the image infrastructure used when constructing generated normal subgroups such as the unipotent radical and derived subgroup.

source
theorem TauCeti.CommHopfAlgCat.hopfSpec_map_left_comp_eqToHom {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left ((AlgebraicGeometry.hopfSpec ↧k).map f.op).hom.hom) (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑↑(CommHopfAlgCat.Hom.hom f)))

After identifying the source and target Hopf spectra with ordinary spectra, the underlying scheme map of hopfSpec.map f.op is Spec.map f.

source
theorem TauCeti.CommHopfAlgCat.specTargetImageIdeal_hopfSpec_map {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) :
AlgebraicGeometry.specTargetImageIdeal (CategoryTheory.Over.Hom.left ((AlgebraicGeometry.hopfSpec ↧k).map f.op).hom.hom) = (HopfIdeal.ker (CommHopfAlgCat.Hom.hom f)).toIdeal

The ideal defining the scheme-theoretic image of a morphism of Hopf spectra is the kernel Hopf ideal's underlying ideal.

source
noncomputable def TauCeti.CommHopfAlgCat.specTargetImageIsoImage {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) :
AlgebraicGeometry.specTargetImage (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑↑(CommHopfAlgCat.Hom.hom f))) ≅ ↧(↑H ⧸ (HopfIdeal.ker (CommHopfAlgCat.Hom.hom f)).toIdeal)

The coordinate ring of the scheme-theoretic image is canonically isomorphic to the Hopf image, the quotient by the kernel Hopf ideal.

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.CommHopfAlgCat.specTargetImageIsoImage_hom_mk {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) (x : ↑H) :
    (CategoryTheory.ConcreteCategory.hom (specTargetImageIsoImage f).hom) ((Ideal.Quotient.mk (AlgebraicGeometry.specTargetImageIdeal (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑↑(CommHopfAlgCat.Hom.hom f))))) x) = (Ideal.Quotient.mk (HopfIdeal.ker (CommHopfAlgCat.Hom.hom f)).toIdeal) x

    The coordinate-ring isomorphism sends the class of an element to the same class in the Hopf image quotient.

    source
    @[simp]
    theorem TauCeti.CommHopfAlgCat.specTargetImageIsoImage_inv_mk {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) (x : ↑H) :
    (CategoryTheory.ConcreteCategory.hom (specTargetImageIsoImage f).inv) ((Ideal.Quotient.mk (HopfIdeal.ker (CommHopfAlgCat.Hom.hom f)).toIdeal) x) = (Ideal.Quotient.mk (AlgebraicGeometry.specTargetImageIdeal (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑↑(CommHopfAlgCat.Hom.hom f))))) x

    The inverse coordinate-ring isomorphism also sends the class of an element to the same class, now regarded in the scheme-theoretic image quotient.

    source
    noncomputable def TauCeti.CommHopfAlgCat.hopfSpecImageSchemeIso {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) :
    ((AlgebraicGeometry.hopfSpec ↧k).obj (Opposite.op (image f))).X.left ≅ AlgebraicGeometry.Spec (AlgebraicGeometry.specTargetImage (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑↑(CommHopfAlgCat.Hom.hom f))))

    The Hopf spectrum of the quotient-by-kernel image is canonically the scheme-theoretic image of the represented affine-group morphism.

    Equations
    Instances For
      source
      theorem TauCeti.CommHopfAlgCat.hopfSpecImageSchemeIso_hom_comp_specTargetImageRingHom {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) :
      CategoryTheory.CategoryStruct.comp (hopfSpecImageSchemeIso f).hom (AlgebraicGeometry.Spec.map (AlgebraicGeometry.specTargetImageRingHom (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑↑(CommHopfAlgCat.Hom.hom f))))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left ((AlgebraicGeometry.hopfSpec ↧k).map (mkImage f).op).hom.hom) (CategoryTheory.eqToHom ⋯)

      Under the image isomorphism, the Hopf-spectrum map induced by the quotient morphism is the closed immersion of the scheme-theoretic image into the target.

      source
      theorem TauCeti.CommHopfAlgCat.hopfSpec_imageι_comp_hopfSpecImageSchemeIso_hom {k : Type u} [Field k] {H K : CommHopfAlgCat k} (f : H ⟶ K) :
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left ((AlgebraicGeometry.hopfSpec ↧k).map (imageι f).op).hom.hom) (hopfSpecImageSchemeIso f).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (AlgebraicGeometry.specTargetImageFactorization (AlgebraicGeometry.Spec.map (CommRingCat.ofHom ↑↑(CommHopfAlgCat.Hom.hom f))))

      Under the image isomorphism, the injective Hopf-algebra factor represents Mathlib's canonical factor from the source to its scheme-theoretic image.