Documentation

MazurTorsion.AlgebraicGeometry.FiniteFlatCommGroupScheme.CommGroupSchemeFppfHOne

Global fppf H¹ for ambient commutative group schemes #

Global fppf H¹ only uses the represented commutative-group-valued point sheaf. Finiteness and flatness of the representing scheme are not needed to define that coefficient sheaf or its cohomology. This file exposes the construction for an arbitrary commutative group scheme over the base while preserving the existing finite-flat API by definitional adapters.

The broader wrapper is needed for Mazur's pre-admissible groups over Spec ℤ: those groups are quasi-finite over the bad prime and need not be finite over the whole base. No quasi-finite extension, elementary-factor classification, or cohomology calculation is asserted here.

source
@[reducible, inline]
abbrev AlgebraicGeometry.CommGroupScheme.Point {S : Scheme} (G : CommGroupScheme S) (T : CategoryTheory.Over S) :
Type u

The group of points of an ambient commutative group scheme on a test scheme over its base.

Equations
Instances For
    source
    noncomputable def AlgebraicGeometry.CommGroupScheme.commPointPresheaf {S : Scheme} (G : CommGroupScheme S) :
    CategoryTheory.Functor (CategoryTheory.Over S)ᵒᵖ CommGrpCat

    The represented commutative-group-valued point presheaf of an ambient commutative group scheme. Unlike the older finite-flat wrapper, this definition makes no finiteness claim.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      noncomputable def AlgebraicGeometry.CommGroupScheme.pointPresheaf {S : Scheme} (G : CommGroupScheme S) :
      CategoryTheory.Functor (CategoryTheory.Over S)ᵒᵖ GrpCat

      The represented point presheaf, forgotten from commutative groups to groups.

      Equations
      Instances For
        source
        @[simp]
        theorem AlgebraicGeometry.CommGroupScheme.pointPresheaf_obj {S : Scheme} (G : CommGroupScheme S) (T : CategoryTheory.Over S) :
        G.pointPresheaf.obj (Opposite.op T) = GrpCat.of (G.Point T)
        source
        theorem AlgebraicGeometry.CommGroupScheme.pointPresheaf_isFppfSheaf {S : Scheme} (G : CommGroupScheme S) :
        CategoryTheory.Presieve.IsSheaf (Scheme.fppfTopology.over S) (G.pointPresheaf.comp (CategoryTheory.forget GrpCat))

        The point presheaf of every commutative group scheme is an fppf sheaf. This is the subcanonical representability argument and does not require the structure map to be finite.

        source
        @[reducible, inline]
        abbrev AlgebraicGeometry.CommGroupScheme.FppfHOne {S : Scheme} (G : CommGroupScheme S) :
        Type (max (u + 1) (v + 1))

        Global relative fppf H¹ of an ambient commutative group scheme.

        Equations
        Instances For
          source
          @[instance_reducible, instance 90]
          noncomputable instance AlgebraicGeometry.CommGroupScheme.fppfHOneCommGroup {S : Scheme} (G : CommGroupScheme S) :
          CommGroup G.FppfHOne

          The canonical common-refinement group law on global fppf H¹.

          Equations
          source
          theorem AlgebraicGeometry.FiniteFlatCommGroupScheme.commPointPresheaf_toCommGroupScheme {S : Scheme} (G : FiniteFlatCommGroupScheme S) :
          G.obj.commPointPresheaf = G.commPointPresheaf

          The ambient and finite-flat point-presheaf wrappers agree definitionally.

          source
          noncomputable def AlgebraicGeometry.FiniteFlatCommGroupScheme.fppfHOneMulEquivToCommGroupScheme {S : Scheme} (G : FiniteFlatCommGroupScheme S) :
          G.FppfHOne ≃* G.obj.FppfHOne

          The existing finite-flat global fppf H¹ is the ambient construction on the underlying commutative group scheme. This is a compatibility adapter, not a second cohomology theory.

          Equations
          Instances For