NYLL
Module

UnrigidifiedGroup.lean

Nyll.AlgebraicCurves.Geometry.Picard.UnrigidifiedGroup
13 declarations indexed from sourceView source ↗

Module documentation

The commutative group of unrigidified Picard-zero classes

Tensor product and actual tensor inverses give the group structure without a section. Pullback is a group homomorphism.

Imports5
Imported by3

Declarations

def

tensorBundle

L41 ↗
AlgebraicGeometry.RelPicard.Unrigidified.tensorBundle
Documentation

Tensor product of actual invertible modules.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory Opposite
open AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.Unrigidified
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  {c : C ⟶ Spec (CommRingCat.of R)}
Lean source · statement
def tensorBundle {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    (M N : LineBundle c t) : LineBundle c t
theorem

baseTwist_tensor_right

L45 ↗
AlgebraicGeometry.RelPicard.Unrigidified.baseTwist_tensor_right
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory Opposite
open AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.Unrigidified
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  {c : C ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem baseTwist_tensor_right {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    (M : LineBundle c t) {N N' : LineBundle c t} (h : BaseTwist c t N N') :
    BaseTwist c t (tensorBundle M N) (tensorBundle M N')
theorem

baseTwist_tensor_left

L52 ↗
AlgebraicGeometry.RelPicard.Unrigidified.baseTwist_tensor_left
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory Opposite
open AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.Unrigidified
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  {c : C ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem baseTwist_tensor_left {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    (N : LineBundle c t) {M M' : LineBundle c t} (h : BaseTwist c t M M') :
    BaseTwist c t (tensorBundle M N) (tensorBundle M' N)
def

classesMul

L59 ↗
AlgebraicGeometry.RelPicard.Unrigidified.classesMul
Documentation

Tensor product descends to relative line-bundle classes.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory Opposite
open AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.Unrigidified
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  {c : C ⟶ Spec (CommRingCat.of R)}
Lean source · statement
def classesMul {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) :
    Classes c t → Classes c t → Classes c t
theorem

fibrewiseZero_tensor

L65 ↗
AlgebraicGeometry.RelPicard.Unrigidified.fibrewiseZero_tensor
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory Opposite
open AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.Unrigidified
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  {c : C ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem fibrewiseZero_tensor {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {M N : LineBundle c t} (hM : FibrewiseZero M) (hN : FibrewiseZero N) :
    FibrewiseZero (tensorBundle M N)
def

zeroMul

L72 ↗
AlgebraicGeometry.RelPicard.Unrigidified.zeroMul
Documentation

Tensor product on fibrewise algebraically trivial classes.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory Opposite
open AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.Unrigidified
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  {c : C ⟶ Spec (CommRingCat.of R)}
Lean source · statement
def zeroMul (X : (Over (Spec (CommRingCat.of R)))ᵒᵖ)
    (x y : (zeroPresheaf c).obj X) : (zeroPresheaf c).obj X
def

zeroOne

L83 ↗
AlgebraicGeometry.RelPicard.Unrigidified.zeroOne
Documentation

The structure sheaf defines the identity class.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory Opposite
open AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.Unrigidified
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  {c : C ⟶ Spec (CommRingCat.of R)}
Lean source · statement
def zeroOne (X : (Over (Spec (CommRingCat.of R)))ᵒᵖ) : (zeroPresheaf c).obj X
def

inverseBundle

L96 ↗
AlgebraicGeometry.RelPicard.Unrigidified.inverseBundle
Documentation

An actual tensor inverse of an invertible module.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory Opposite
open AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.Unrigidified
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  {c : C ⟶ Spec (CommRingCat.of R)}
Lean source · statement
def inverseBundle {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    (M : LineBundle c t) : LineBundle c t
theorem

inverseBundle_iso

L100 ↗
AlgebraicGeometry.RelPicard.Unrigidified.inverseBundle_iso
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory Opposite
open AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.Unrigidified
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  {c : C ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem inverseBundle_iso {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    (M : LineBundle c t) : Nonempty (M.1 ⊗ (inverseBundle M).1 ≅ 𝟙_ _)
theorem

fibrewiseZero_inverse

L104 ↗
AlgebraicGeometry.RelPicard.Unrigidified.fibrewiseZero_inverse
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory Opposite
open AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.Unrigidified
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  {c : C ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem fibrewiseZero_inverse {T : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)}
    {M : LineBundle c t} (hM : FibrewiseZero M) : FibrewiseZero (inverseBundle M)
def

zeroInv

L113 ↗
AlgebraicGeometry.RelPicard.Unrigidified.zeroInv
Documentation

A tensor inverse defines the inverse relative class.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory Opposite
open AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.Unrigidified
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  {c : C ⟶ Spec (CommRingCat.of R)}
Lean source · statement
def zeroInv (X : (Over (Spec (CommRingCat.of R)))ᵒᵖ)
    (x : (zeroPresheaf c).obj X) : (zeroPresheaf c).obj X
def

zeroCommGroup

L122 ↗
AlgebraicGeometry.RelPicard.Unrigidified.zeroCommGroup
Documentation

The commutative group structure supplied by tensor products and tensor inverses.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory Opposite
open AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.Unrigidified
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  {c : C ⟶ Spec (CommRingCat.of R)}
Lean source · full declaration
def zeroCommGroup (X : (Over (Spec (CommRingCat.of R)))ᵒᵖ) :
    CommGroup ((zeroPresheaf c).obj X) where
  mul := zeroMul X
  one := zeroOne X
  inv := zeroInv X
  mul_assoc := by
    rintro ⟨x, hx⟩ ⟨y, hy⟩ ⟨z, hz⟩
    apply Subtype.ext
    induction x using Quot.ind
    induction y using Quot.ind
    induction z using Quot.ind
    exact Quot.sound (baseTwist_of_iso (α_ _ _ _))
  one_mul := by
    rintro ⟨x, hx⟩
    apply Subtype.ext
    induction x using Quot.ind
    exact Quot.sound (baseTwist_of_iso (λ_ _))
  mul_one := by
    rintro ⟨x, hx⟩
    apply Subtype.ext
    induction x using Quot.ind
    exact Quot.sound (baseTwist_of_iso (ρ_ _))
  mul_comm := by
    rintro ⟨x, hx⟩ ⟨y, hy⟩
    apply Subtype.ext
    induction x using Quot.ind
    induction y using Quot.ind
    exact Quot.sound (baseTwist_of_iso (β_ _ _))
  inv_mul_cancel := by
    rintro ⟨x, hx⟩
    apply Subtype.ext
    change classesMul X.unop.hom (Quot.mk _ (inverseBundle (Quot.out x))) x = _
    have h : classesMul X.unop.hom (Quot.mk _ (inverseBundle (Quot.out x)))
        (Quot.mk _ (Quot.out x)) =
        Quot.mk _ ⟨𝟙_ (pullback c X.unop.hom).Modules,
          Scheme.Modules.isInvertible_unit _⟩ :=
      Quot.sound (baseTwist_of_iso
        (β_ (inverseBundle (Quot.out x)).1 (Quot.out x).1 ≪≫
          (inverseBundle_iso (Quot.out x)).some))
    exact (congrArg (classesMul X.unop.hom (Quot.mk _ (inverseBundle (Quot.out x))))
      (Quot.out_eq x)).symm.trans h
def

zeroCommGrpPresheaf

L165 ↗
AlgebraicGeometry.RelPicard.Unrigidified.zeroCommGrpPresheaf
Documentation

The actual commutative-group-valued unrigidified Picard-zero presheaf.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u
open CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory Opposite
open AlgebraicGeometry NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.Unrigidified
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  {c : C ⟶ Spec (CommRingCat.of R)}
Lean source · full declaration
def zeroCommGrpPresheaf (c : C ⟶ Spec (CommRingCat.of R)) :
    (Over (Spec (CommRingCat.of R)))ᵒᵖ ⥤ CommGrpCat.{u + 1} where
  obj X := @CommGrpCat.of ((zeroPresheaf c).obj X) (zeroCommGroup X)
  map {X Y} φ :=
    let _ : CommGroup ((zeroPresheaf c).obj X) := zeroCommGroup X
    let _ : CommGroup ((zeroPresheaf c).obj Y) := zeroCommGroup Y
    CommGrpCat.ofHom
      { toFun := (zeroPresheaf c).map φ
        map_one' := by
          apply Subtype.ext
          exact Quot.sound (baseTwist_of_iso (Scheme.Modules.pullbackUnitIso _))
        map_mul' := by
          rintro ⟨x, hx⟩ ⟨y, hy⟩
          apply Subtype.ext
          induction x using Quot.ind
          induction y using Quot.ind
          exact Quot.sound (baseTwist_of_iso (Scheme.Modules.pullbackTensorObjIso _ _ _)) }
  map_id X := by
    let _ : CommGroup ((zeroPresheaf c).obj X) := zeroCommGroup X
    apply CommGrpCat.hom_ext
    apply MonoidHom.ext
    intro x
    exact ConcreteCategory.congr_hom ((zeroPresheaf c).map_id X) x
  map_comp {X Y Z} φ ψ := by
    let _ : CommGroup ((zeroPresheaf c).obj X) := zeroCommGroup X
    let _ : CommGroup ((zeroPresheaf c).obj Y) := zeroCommGroup Y
    let _ : CommGroup ((zeroPresheaf c).obj Z) := zeroCommGroup Z
    apply CommGrpCat.hom_ext
    apply MonoidHom.ext
    intro x
    exact ConcreteCategory.congr_hom ((zeroPresheaf c).map_comp φ ψ) x

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.