Documentation

TauCeti.Algebra.AlgebraicGroup.Isogeny.Basic

Isogenies of affine group schemes #

A morphism f : H ⟶ K of commutative Hopf algebras represents, contravariantly, a morphism Spec K ⟶ Spec H of affine group schemes. We call this morphism an isogeny when its coordinate map is finite and faithfully flat. These two conditions respectively say that the group-scheme morphism is finite and faithfully flat (hence fpqc-surjective). A central isogeny is an isogeny whose scheme-theoretic kernel is central.

The definitions are stated over an arbitrary commutative base ring. Over a field, for affine algebraic groups of finite type, this is the coordinate-algebra form of the usual finite surjective group morphism. Keeping faithful flatness explicit avoids replacing scheme-theoretic surjectivity by a weaker statement about points over the base field.

Main declarations #

References #

The isogeny and central-kernel interfaces and their proof organization are adapted from the prior formalizations in TauCeti.AlgebraicGeometry.GroupScheme.CentralIsogeny.Basic and TauCeti.AlgebraicGeometry.GroupScheme.CentralIsogeny.Coordinate.

This supplies the central-isogeny interface requested in Layer 6, "Reductive and semisimple groups", of TauCetiRoadmap/ReductiveGroups/README.md. It builds on the existing scheme-theoretic kernel and central Hopf-ideal APIs.

source
def TauCeti.CommHopfAlgCat.IsIsogeny {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) :
Prop

A morphism of affine group schemes is an isogeny when its coordinate morphism is finite and faithfully flat.

For f : H ⟶ K, this predicate concerns the contravariant group-scheme morphism Spec K ⟶ Spec H. Finiteness is therefore finiteness of K as an H-module through f, while faithful flatness is the scheme-theoretic surjectivity condition.

Equations
Instances For
    source
    def TauCeti.CommHopfAlgCat.IsCentralIsogeny {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) :
    Prop

    A central isogeny is an isogeny whose scheme-theoretic kernel is central. The kernel is represented by the quotient of K by kernelHopfIdeal f, so centrality is imposed on that Hopf ideal.

    Equations
    Instances For
      source
      theorem TauCeti.CommHopfAlgCat.isCentralIsogeny_iff {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) :
      IsCentralIsogeny f ↔ (↑(CommHopfAlgCat.Hom.hom f)).Finite ∧ (↑(CommHopfAlgCat.Hom.hom f)).FaithfullyFlat ∧ (kernelHopfIdeal f).IsCentral

      Restatement of the coordinate-algebra conditions defining a central isogeny.

      source
      theorem TauCeti.CommHopfAlgCat.isIsogeny_iff_isIsogeny_hopfSpec_map {k : Type u} [CommRing k] {H₀ K₀ : CommHopfAlgCat k} (f : H₀ ⟶ K₀) :
      IsIsogeny f ↔ GroupScheme.IsIsogeny ((AlgebraicGeometry.hopfSpec (CommRingCat.of k)).map f.op)

      The coordinate-algebra definition of an isogeny agrees with the group-scheme definition after applying the contravariant Hopf spectrum functor.

      source
      theorem TauCeti.CommHopfAlgCat.isCentralIsogeny_iff_isCentralIsogeny_hopfSpec_map {k : Type u} [CommRing k] {H₀ K₀ : CommHopfAlgCat k} (f : H₀ ⟶ K₀) :
      IsCentralIsogeny f ↔ GroupScheme.IsCentralIsogeny ((AlgebraicGeometry.hopfSpec (CommRingCat.of k)).map f.op)

      The coordinate-algebra definition of a central isogeny agrees with the group-scheme definition after applying the contravariant Hopf spectrum functor.

      source
      theorem TauCeti.CommHopfAlgCat.IsIsogeny.finite {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {f : H ⟶ K} (hf : IsIsogeny f) :
      (↑(CommHopfAlgCat.Hom.hom f)).Finite

      The coordinate algebra of the source of an isogeny is finite over that of the target.

      source
      theorem TauCeti.CommHopfAlgCat.IsIsogeny.faithfullyFlat {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {f : H ⟶ K} (hf : IsIsogeny f) :
      (↑(CommHopfAlgCat.Hom.hom f)).FaithfullyFlat

      The coordinate map of an isogeny is faithfully flat.

      source
      theorem TauCeti.CommHopfAlgCat.IsIsogeny.injective {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {f : H ⟶ K} (hf : IsIsogeny f) :
      Function.Injective ⇑(CommHopfAlgCat.Hom.hom f)

      The coordinate map of an isogeny is injective.

      source
      theorem TauCeti.CommHopfAlgCat.IsIsogeny.isIso_iff_surjective {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {f : H ⟶ K} (hf : IsIsogeny f) :
      CategoryTheory.IsIso f ↔ Function.Surjective ⇑(CommHopfAlgCat.Hom.hom f)

      An isogeny is an isomorphism exactly when its coordinate map is surjective.

      source
      theorem TauCeti.CommHopfAlgCat.IsIsogeny.finiteType {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {f : H ⟶ K} (hf : IsIsogeny f) :
      (↑(CommHopfAlgCat.Hom.hom f)).FiniteType

      A finite coordinate morphism is in particular of finite type.

      source
      theorem TauCeti.CommHopfAlgCat.IsIsogeny.comp {R : Type u} [CommRing R] {H K L : CommHopfAlgCat R} {f : H ⟶ K} {g : K ⟶ L} (hf : IsIsogeny f) (hg : IsIsogeny g) :
      IsIsogeny (CategoryTheory.CategoryStruct.comp f g)

      A composite of isogenies is an isogeny.

      source
      theorem TauCeti.CommHopfAlgCat.IsCentralIsogeny.isIsogeny {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {f : H ⟶ K} (hf : IsCentralIsogeny f) :
      IsIsogeny f

      Forgetting centrality from a central isogeny gives an isogeny.

      source
      theorem TauCeti.CommHopfAlgCat.IsCentralIsogeny.isCentral_kernelHopfIdeal {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {f : H ⟶ K} (hf : IsCentralIsogeny f) :
      (kernelHopfIdeal f).IsCentral

      The kernel Hopf ideal of a central isogeny is central.

      source
      theorem TauCeti.CommHopfAlgCat.IsCentralIsogeny.isNormal_kernelHopfIdeal {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {f : H ⟶ K} (hf : IsCentralIsogeny f) :
      (kernelHopfIdeal f).IsNormal

      The kernel Hopf ideal of a central isogeny is normal.

      source
      theorem TauCeti.CommHopfAlgCat.IsCentralIsogeny.isCocomm_quotient_kernelHopfIdeal {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {f : H ⟶ K} (hf : IsCentralIsogeny f) :
      Coalgebra.IsCocomm R ↑(quotient K (kernelHopfIdeal f))

      The coordinate ring of the kernel of a central isogeny is cocommutative. Equivalently, the kernel group scheme is commutative.

      source
      theorem TauCeti.CommHopfAlgCat.IsCentralIsogeny.finite {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {f : H ⟶ K} (hf : IsCentralIsogeny f) :
      (↑(CommHopfAlgCat.Hom.hom f)).Finite

      A central isogeny is finite on coordinate algebras.

      source
      theorem TauCeti.CommHopfAlgCat.IsCentralIsogeny.faithfullyFlat {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {f : H ⟶ K} (hf : IsCentralIsogeny f) :
      (↑(CommHopfAlgCat.Hom.hom f)).FaithfullyFlat

      A central isogeny is faithfully flat on coordinate algebras.

      source
      theorem TauCeti.CommHopfAlgCat.IsCentralIsogeny.injective {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} {f : H ⟶ K} (hf : IsCentralIsogeny f) :
      Function.Injective ⇑(CommHopfAlgCat.Hom.hom f)

      The coordinate map of a central isogeny is injective.

      source
      @[simp]
      theorem TauCeti.CommHopfAlgCat.isIsogeny_id {R : Type u} [CommRing R] (H : CommHopfAlgCat R) :
      IsIsogeny (CategoryTheory.CategoryStruct.id H)

      The identity morphism is an isogeny.

      source
      theorem TauCeti.CommHopfAlgCat.isIsogeny_of_bijective {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (hf : Function.Bijective ⇑(CommHopfAlgCat.Hom.hom f)) :
      IsIsogeny f

      A bijective coordinate morphism is an isogeny.

      source
      theorem TauCeti.CommHopfAlgCat.isCentralIsogeny_of_bijective {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) (hf : Function.Bijective ⇑(CommHopfAlgCat.Hom.hom f)) :
      IsCentralIsogeny f

      A bijective coordinate morphism is a central isogeny. Its kernel Hopf ideal is the augmentation ideal, hence cuts out the trivial central subgroup.

      source
      theorem TauCeti.CommHopfAlgCat.isCentralIsogeny_unit_of_isCocomm {R : Type u} [CommRing R] (K : CommHopfAlgCat R) [Module.Finite R ↑K] [Module.FaithfullyFlat R ↑K] [Coalgebra.IsCocomm R ↑K] :
      IsCentralIsogeny (CommHopfAlgCat.ofHom (Bialgebra.unitBialgHom R ↑K))

      The structure morphism from a finite faithfully flat commutative affine group scheme to the trivial group is a central isogeny. Its kernel is the whole source group, so nontrivial choices of K give central isogenies with nontrivial kernel.

      source
      theorem TauCeti.CommHopfAlgCat.isIsogeny_of_isIso {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) [CategoryTheory.IsIso f] :
      IsIsogeny f

      Every categorical isomorphism of commutative Hopf algebras is an isogeny.

      source
      theorem TauCeti.CommHopfAlgCat.isCentralIsogeny_of_isIso {R : Type u} [CommRing R] {H K : CommHopfAlgCat R} (f : H ⟶ K) [CategoryTheory.IsIso f] :
      IsCentralIsogeny f

      Every categorical isomorphism of commutative Hopf algebras is a central isogeny.

      source
      @[simp]
      theorem TauCeti.CommHopfAlgCat.isCentralIsogeny_id {R : Type u} [CommRing R] (H : CommHopfAlgCat R) :
      IsCentralIsogeny (CategoryTheory.CategoryStruct.id H)

      The identity morphism is a central isogeny.

      source
      theorem TauCeti.CommHopfAlgCat.IsIsogeny.mapPointsFunctor_app_surjective {R : Type u} [CommRing R] {a✝ a✝¹ : CommHopfAlgCat R} {f : a✝ ⟶ a✝¹} (hf : IsIsogeny f) (F : Type w) [Field F] [Algebra R F] [IsAlgClosed F] :
      Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom ((mapPointsFunctor f).app (CommAlgCat.of R F)))

      An isogeny is surjective on points valued in an algebraically closed field.