Documentation

MazurTorsion.Upstream.AINTLIB.Picard.Pic

The Picard group of a scheme #

Stage P2 of the AINTLIB ModularCurves T-PIC0 stream (GME 2.2.2, p. 108): the Picard group. Source of record, verbatim: "We write E_T for E ×_S T and Pic(E_T) for the group of isomorphism classes of all invertible sheaves on E_T."

With the [GAP1-W-MONO] leaf sorry-free (sheafificationW_isMonoidal + sheafificationW_isLocalization), mathlib's LocalizedMonoidal hands the category of sheaves of modules over a sheaf of commutative rings its symmetric monoidal structure — the previously Nonempty-wrapped payoff, now as data (the v10.8 no-sorried-monoidal-DATA discipline is satisfied, not bypassed). Following mathlib's own packaging (CategoryTheory.Sheaf.monoidalCategory in Sites/Monoidal.lean) these are defs, not global instances, to stay merge-safe against a future upstream instance.

The Picard group is then the group of ⊗-invertible iso-classes, following mathlib's CommRing.Pic pattern (RingTheory/PicardGroup.lean): the units of the ⊗-monoid on the skeleton, Pic X := (Skeleton X.Modules)ˣ. An element is an iso-class [M] together with an inverse class; commutativity comes from the braiding.

Main definitions #

The comparison with the cover-local IsInvertible predicate of Picard/InvertibleSheaf.lean — GME's "the formation of an invertible sheaf is local", (2.17) — is the registered follow-up [PIC-P2-CMP]; its invertible-to-unit direction constructs the dual sheaf, which is coordinated with the Cartier-duality lane (v10.36 two-route edge: never build duality twice).

source
@[implicit_reducible]
noncomputable def PresheafOfModules.sheafOfModulesMonoidalCategory {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] (S : CategoryTheory.Functor Cᵒᵖ CommRingCat) (hS : CategoryTheory.Presheaf.IsSheaf J (S.comp (CategoryTheory.forget₂ CommRingCat RingCat))) :
CategoryTheory.MonoidalCategory (SheafOfModules { obj := S.comp (CategoryTheory.forget₂ CommRingCat RingCat), property := hS })

The monoidal category of sheaves of modules over a sheaf of commutative rings: mathlib's LocalizedMonoidal applied to the sheafification localization (sheafificationW_isLocalization) with the ⊗-stable localizing class (sheafificationW_isMonoidal, the [GAP1-W-MONO] leaf). A def, not an instance, per the CategoryTheory.Sheaf.monoidalCategory precedent — activate with attribute [local instance] or letI.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[implicit_reducible]
    noncomputable def PresheafOfModules.sheafOfModulesSymmetricCategory {C : Type u} [CategoryTheory.Category.{u, u} C] {J : CategoryTheory.GrothendieckTopology C} [J.WEqualsLocallyBijective AddCommGrpCat] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] (S : CategoryTheory.Functor Cᵒᵖ CommRingCat) (hS : CategoryTheory.Presheaf.IsSheaf J (S.comp (CategoryTheory.forget₂ CommRingCat RingCat))) :
    CategoryTheory.SymmetricCategory (SheafOfModules { obj := S.comp (CategoryTheory.forget₂ CommRingCat RingCat), property := hS })

    The symmetric monoidal structure on sheaves of modules (the braiding descends from the symmetric structure on presheaves of modules through the localization).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[implicit_reducible]
      noncomputable def AlgebraicGeometry.Scheme.Modules.monoidalCategory (X : Scheme) :
      CategoryTheory.MonoidalCategory X.Modules

      The monoidal category structure on 𝒪ₓ-modules (transport of PresheafOfModules.sheafOfModulesMonoidalCategory across the structure-eta identification X.ringCatSheaf = ⟨X.sheaf.obj ⋙ forget₂, _⟩). A def, not an instance — activate with letI / attribute [local instance].

      Equations
      Instances For
        source
        @[implicit_reducible]
        noncomputable def AlgebraicGeometry.Scheme.Modules.symmetricCategory (X : Scheme) :
        CategoryTheory.SymmetricCategory X.Modules

        The symmetric monoidal structure on 𝒪ₓ-modules.

        Equations
        Instances For
          source
          noncomputable def AlgebraicGeometry.Scheme.Pic (X : Scheme) :
          Type (u + 1)

          The Picard group of a scheme (GME 2.2.2 (2.16), p. 108: Pic(E_T) is "the group of isomorphism classes of all invertible sheaves") — following mathlib's CommRing.Pic pattern, the units of the ⊗-monoid of iso-classes of 𝒪ₓ-modules: an element is an iso-class [𝓛] together with an inverse class [𝓛⁻¹]. The comparison with the cover-local IsInvertible predicate is the registered follow-up [PIC-P2-CMP] (its invertible-to-unit direction constructs the dual — Cartier-duality-lane coordinated).

          Equations
          Instances For
            source
            @[instance_reducible]
            noncomputable instance AlgebraicGeometry.Scheme.instCommGroupPic (X : Scheme) :
            CommGroup X.Pic
            Equations
            • One or more equations did not get rendered due to their size.