Module

UnrigidifiedGroupComparison.lean

Nyll.AlgebraicCurves.Geometry.Picard.UnrigidifiedGroupComparison

2 declarations indexed from sourceView source ↗

Module documentation

The group comparison between pointed and unrigidified Picard classes

Forgetting rigidification preserves tensor products on actual representatives. The normalization equivalence is therefore an equivalence of commutative groups.

Imports3

Imported by3

def

forgetZeroMulEquiv

L32 ↗

AlgebraicGeometry.RelPicard.Unrigidified.forgetZeroMulEquiv

Documentation

Forgetting the rigidification is a multiplicative equivalence on Picard-zero classes.

Source context 6 commands

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

universe u
open CategoryTheory AlgebraicGeometry AlgebraicGeometry.RelPicard Opposite
open NeronModelInfra
noncomputable section
namespace AlgebraicGeometry.RelPicard.Unrigidified
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
  {c : C ⟶ Spec (CommRingCat.of R)}
  (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)

Lean source · full declaration

def forgetZeroMulEquiv (X : (Over (Spec (CommRingCat.of R)))ᵒᵖ) :
    (relSubPicCommGrpPresheaf c ε (algEquivZeroGroupCut c ε)).obj X ≃*
      (zeroCommGrpPresheaf c).obj X where
  toEquiv := (zeroClassesEquiv ε X.unop.hom).symm
  map_mul' := by
    rintro ⟨x, hx⟩ ⟨y, hy⟩
    apply Subtype.ext
    induction x using Quotient.ind
    induction y using Quotient.ind
    rfl

def

normalizeZeroMulEquiv

L44 ↗

AlgebraicGeometry.RelPicard.Unrigidified.normalizeZeroMulEquiv