Documentation

TauCeti.Algebra.AlgebraicGroup.HopfIdeal.Quotient.Kernel.Exact

Short exact sequences of affine groups #

A sequence of affine groups 1 → N → G → Q → 1 is exact when G → Q is faithfully flat (a quotient map) and N → G is a closed immersion identifying N with the scheme-theoretic kernel of G → Q (Milne, Algebraic Groups, §5.c). In coordinate Hopf algebras the arrows reverse: such a sequence is a pair of morphisms

O(Q) --p--> O(G) --i--> O(N)

of commutative Hopf algebras with p faithfully flat, i surjective, and ker i equal to the kernel Hopf ideal O(G) · p(O(Q)⁺). This file records that notion, TauCeti.CommHopfAlgCat.IsShortExact, over an arbitrary commutative base ring, with no smoothness, reducedness or finite-type hypotheses, and derives its basic consequences.

Main declarations #

References #

source
structure TauCeti.CommHopfAlgCat.IsShortExact {R : Type u} [CommRing R] {Q G N : CommHopfAlgCat R} (p : Q ⟶ G) (i : G ⟶ N) :
Prop

Coordinate morphisms p : O(Q) ⟶ O(G) and i : O(G) ⟶ O(N) form a short exact sequence of affine groups 1 → N → G → Q → 1 when G → Q is faithfully flat, N → G is a closed immersion, and N is the scheme-theoretic kernel of G → Q: the ideal cutting out N is the kernel Hopf ideal of p.

Instances For
    source
    theorem TauCeti.CommHopfAlgCat.IsShortExact.kerOfSurjective_eq_kernelHopfIdeal {R : Type u} [CommRing R] {Q G N : CommHopfAlgCat R} {p : Q ⟶ G} {i : G ⟶ N} (h : IsShortExact p i) :
    HopfIdeal.kerOfSurjective (CommHopfAlgCat.Hom.hom i) ⋯ = kernelHopfIdeal p

    In a short exact sequence, the Hopf ideal cutting out the subgroup is the kernel Hopf ideal of the quotient map.

    source
    @[simp]
    theorem TauCeti.CommHopfAlgCat.IsShortExact.comp_eq_unit_comp_counit {R : Type u} [CommRing R] {Q G N : CommHopfAlgCat R} {p : Q ⟶ G} {i : G ⟶ N} (h : IsShortExact p i) :
    CategoryTheory.CategoryStruct.comp p i = CommHopfAlgCat.ofHom ((Bialgebra.unitBialgHom R ↑N).comp (Bialgebra.counitBialgHom R ↑Q))

    The composite N → G → Q of a short exact sequence is the trivial homomorphism.

    source
    @[simp]
    theorem TauCeti.CommHopfAlgCat.IsShortExact.comp_eq_unit_comp_counit_assoc {R : Type u} [CommRing R] {Q G N : CommHopfAlgCat R} {p : Q ⟶ G} {i : G ⟶ N} (h : IsShortExact p i) {Z : CommHopfAlgCat R} (h✝ : N ⟶ Z) :
    CategoryTheory.CategoryStruct.comp p (CategoryTheory.CategoryStruct.comp i h✝) = CategoryTheory.CategoryStruct.comp (CommHopfAlgCat.ofHom ((Bialgebra.unitBialgHom R ↑N).comp (Bialgebra.counitBialgHom R ↑Q))) h✝

    The composite N → G → Q of a short exact sequence is the trivial homomorphism.

    source
    noncomputable def TauCeti.CommHopfAlgCat.IsShortExact.kernelIso {R : Type u} [CommRing R] {Q G N : CommHopfAlgCat R} {p : Q ⟶ G} {i : G ⟶ N} (h : IsShortExact p i) :
    quotient G (kernelHopfIdeal p) ≅ N

    The subgroup in a short exact sequence is isomorphic to the scheme-theoretic kernel of the quotient map, compatibly with the inclusions into G (mkQuotient_comp_kernelIso_hom).

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.CommHopfAlgCat.IsShortExact.mkQuotient_comp_kernelIso_hom {R : Type u} [CommRing R] {Q G N : CommHopfAlgCat R} {p : Q ⟶ G} {i : G ⟶ N} (h : IsShortExact p i) :
      CategoryTheory.CategoryStruct.comp (mkQuotient G (kernelHopfIdeal p)) h.kernelIso.hom = i

      The identification of the subgroup with the kernel respects the inclusions into G.

      source
      @[simp]
      theorem TauCeti.CommHopfAlgCat.IsShortExact.mkQuotient_comp_kernelIso_hom_assoc {R : Type u} [CommRing R] {Q G N : CommHopfAlgCat R} {p : Q ⟶ G} {i : G ⟶ N} (h : IsShortExact p i) {Z : CommHopfAlgCat R} (h✝ : N ⟶ Z) :
      CategoryTheory.CategoryStruct.comp (mkQuotient G (kernelHopfIdeal p)) (CategoryTheory.CategoryStruct.comp h.kernelIso.hom h✝) = CategoryTheory.CategoryStruct.comp i h✝

      The identification of the subgroup with the kernel respects the inclusions into G.

      source
      @[simp]
      theorem TauCeti.CommHopfAlgCat.IsShortExact.comp_kernelIso_inv {R : Type u} [CommRing R] {Q G N : CommHopfAlgCat R} {p : Q ⟶ G} {i : G ⟶ N} (h : IsShortExact p i) :
      CategoryTheory.CategoryStruct.comp i h.kernelIso.inv = mkQuotient G (kernelHopfIdeal p)

      The inverse identification of the subgroup with the kernel respects the inclusions into G.

      source
      @[simp]
      theorem TauCeti.CommHopfAlgCat.IsShortExact.comp_kernelIso_inv_assoc {R : Type u} [CommRing R] {Q G N : CommHopfAlgCat R} {p : Q ⟶ G} {i : G ⟶ N} (h : IsShortExact p i) {Z : CommHopfAlgCat R} (h✝ : quotient G (kernelHopfIdeal p) ⟶ Z) :
      CategoryTheory.CategoryStruct.comp i (CategoryTheory.CategoryStruct.comp h.kernelIso.inv h✝) = CategoryTheory.CategoryStruct.comp (mkQuotient G (kernelHopfIdeal p)) h✝

      The inverse identification of the subgroup with the kernel respects the inclusions into G.

      source
      theorem TauCeti.CommHopfAlgCat.IsShortExact.coinvariants_eq_range {R : Type u} [CommRing R] {Q G N : CommHopfAlgCat R} {p : Q ⟶ G} {i : G ⟶ N} (h : IsShortExact p i) :
      (HopfIdeal.kerOfSurjective (CommHopfAlgCat.Hom.hom i) ⋯).coinvariants = (↑(CommHopfAlgCat.Hom.hom p)).range

      The functions on G invariant under the subgroup N of a short exact sequence are exactly the functions pulled back from the quotient Q.

      source
      theorem TauCeti.CommHopfAlgCat.IsShortExact.ker_mapPointsFunctor_app_eq_range {R : Type u} [CommRing R] {Q G N : CommHopfAlgCat R} {p : Q ⟶ G} {i : G ⟶ N} (h : IsShortExact p i) (A : CommAlgCat R) :
      (GrpCat.Hom.hom ((mapPointsFunctor p).app A)).ker = (GrpCat.Hom.hom ((mapPointsFunctor i).app A)).range

      Exactness on points: for every commutative R-algebra A, an A-point of G maps to the identity of Q(A) exactly when it comes from an A-point of N.

      source
      theorem TauCeti.CommHopfAlgCat.IsShortExact.isIsogeny_iff_moduleFinite {R : Type u} [CommRing R] {Q G N : CommHopfAlgCat R} {p : Q ⟶ G} {i : G ⟶ N} (h : IsShortExact p i) :
      IsIsogeny p ↔ Module.Finite R ↑N

      The quotient map of a short exact sequence is an isogeny exactly when the subgroup is finite over the base.

      source
      theorem TauCeti.CommHopfAlgCat.isShortExact_mkQuotient_kernelHopfIdeal {R : Type u} [CommRing R] {Q G : CommHopfAlgCat R} (p : Q ⟶ G) (hp : (↑(CommHopfAlgCat.Hom.hom p)).FaithfullyFlat) :
      IsShortExact p (mkQuotient G (kernelHopfIdeal p))

      A faithfully flat morphism and the quotient map onto its scheme-theoretic kernel form a short exact sequence.

      source
      theorem TauCeti.CommHopfAlgCat.isShortExact_iff_exists_iso {R : Type u} [CommRing R] {Q G N : CommHopfAlgCat R} (p : Q ⟶ G) (i : G ⟶ N) :
      IsShortExact p i ↔ (↑(CommHopfAlgCat.Hom.hom p)).FaithfullyFlat ∧ ∃ (e : quotient G (kernelHopfIdeal p) ≅ N), CategoryTheory.CategoryStruct.comp (mkQuotient G (kernelHopfIdeal p)) e.hom = i

      A pair of coordinate morphisms is short exact exactly when the first is faithfully flat and the second is, up to isomorphism of its target, the quotient map onto the kernel Hopf ideal of the first.