NYLL
Module

ChangeBase.lean

Nyll.AlgebraicCurves.RelativeDivisors.ChangeBase
11 declarations indexed from sourceView source ↗

Module documentation

Relative divisors after changing the base of the curve

The canonical associativity isomorphism identifies the actual divisor ideals, their finite flat projections, and their degrees. This is a change of the base of the curve, in addition to pullback of a divisor along a test scheme.

Imports8
Imported by2

Declarations

def

transport

L33 ↗
AlgebraicGeometry.RelEffCartierDiv.transport
Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.RelEffCartierDiv
Lean source · statement
def transport
    {C S C' S' T : Scheme.{u}} {f : C ⟶ S} {g : T ⟶ S}
    {f' : C' ⟶ S'} {g' : T ⟶ S'} {r : ℕ}
    (D : RelEffCartierDiv f r g) (e : pullback f' g' ≅ pullback f g)
    (he : e.hom ≫ pullback.snd f g = pullback.snd f' g') :
    RelEffCartierDiv f' r g'
def

changeBaseEquiv

L64 ↗
AlgebraicGeometry.RelEffCartierDiv.changeBaseEquiv
Documentation

Divisors on a base changed curve are exactly divisors on the original curve over the composite test map. The ideals are transported by the actual pullback associativity isomorphism.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.RelEffCartierDiv
Lean source · full declaration
def changeBaseEquiv {C S S' T : Scheme.{u}}
    (f : C ⟶ S) (s : S' ⟶ S) (g : T ⟶ S') (r : ℕ) :
    RelEffCartierDiv (pullback.snd f s) r g ≃ RelEffCartierDiv f r (g ≫ s) where
  toFun D := transport D (pullbackLeftPullbackSndIso f s g).symm
    (pullbackLeftPullbackSndIso_inv_snd_snd f s g)
  invFun D := transport D (pullbackLeftPullbackSndIso f s g)
    (pullbackLeftPullbackSndIso_hom_snd f s g)
  left_inv D := by
    apply RelEffCartierDiv.ext
    change (D.I.comap (pullbackLeftPullbackSndIso f s g).inv).comap
      (pullbackLeftPullbackSndIso f s g).hom = D.I
    rw [← Scheme.IdealSheafData.comap_comp, Iso.hom_inv_id,
      Scheme.IdealSheafData.comap_id]
  right_inv D := by
    apply RelEffCartierDiv.ext
    change (D.I.comap (pullbackLeftPullbackSndIso f s g).hom).comap
      (pullbackLeftPullbackSndIso f s g).inv = D.I
    rw [← Scheme.IdealSheafData.comap_comp, Iso.inv_hom_id,
      Scheme.IdealSheafData.comap_id]
theorem

changeBaseEquiv_ideal

L84 ↗
AlgebraicGeometry.RelEffCartierDiv.changeBaseEquiv_ideal
Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.RelEffCartierDiv
Lean source · statement
theorem changeBaseEquiv_ideal {C S S' T : Scheme.{u}}
    (f : C ⟶ S) (s : S' ⟶ S) (g : T ⟶ S') {r : ℕ}
    (D : RelEffCartierDiv (pullback.snd f s) r g) :
    (changeBaseEquiv f s g r D).I =
      D.I.comap (pullbackLeftPullbackSndIso f s g).inv
theorem

changeBaseEquiv_symm_ideal

L90 ↗
AlgebraicGeometry.RelEffCartierDiv.changeBaseEquiv_symm_ideal
Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.RelEffCartierDiv
Lean source · statement
theorem changeBaseEquiv_symm_ideal {C S S' T : Scheme.{u}}
    (f : C ⟶ S) (s : S' ⟶ S) (g : T ⟶ S') {r : ℕ}
    (D : RelEffCartierDiv f r (g ≫ s)) :
    ((changeBaseEquiv f s g r).symm D).I =
      D.I.comap (pullbackLeftPullbackSndIso f s g).hom
theorem

changeBaseIso_map

L96 ↗
AlgebraicGeometry.RelEffCartierDiv.changeBaseIso_map
Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.RelEffCartierDiv
Lean source · statement
theorem changeBaseIso_map {C S S' T T' : Scheme.{u}}
    (f : C ⟶ S) (s : S' ⟶ S) {g : T ⟶ S'} {g' : T' ⟶ S'}
    (φ : T' ⟶ T) (hφ : φ ≫ g = g') :
    (pullbackLeftPullbackSndIso f s g').hom ≫
        mapOnProdOver f φ ((Category.assoc _ _ _).symm.trans (congrArg (· ≫ s) hφ)) =
      mapOnProdOver (pullback.snd f s) φ hφ ≫
        (pullbackLeftPullbackSndIso f s g).hom
theorem

changeBaseEquiv_pullbackAlong

L111 ↗
AlgebraicGeometry.RelEffCartierDiv.changeBaseEquiv_pullbackAlong
Documentation

Changing the base of the curve commutes with actual pullback of divisors along every test-scheme morphism.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.RelEffCartierDiv
Lean source · statement
theorem changeBaseEquiv_pullbackAlong {C S S' T T' : Scheme.{u}}
    (f : C ⟶ S) (s : S' ⟶ S) {g : T ⟶ S'} {g' : T' ⟶ S'} {r : ℕ}
    (D : RelEffCartierDiv (pullback.snd f s) r g)
    (φ : T' ⟶ T) (hφ : φ ≫ g = g') :
    changeBaseEquiv f s g' r (D.pullbackAlong φ hφ) =
      (changeBaseEquiv f s g r D).pullbackAlong φ
        ((Category.assoc _ _ _).symm.trans (congrArg (· ≫ s) hφ))
def

changeBase

L129 ↗
AlgebraicGeometry.RelEffCartierDiv.changeBase
Documentation

The actual scalar extension of a family of relative effective divisors.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.RelEffCartierDiv
Lean source · statement
def changeBase {C S Y : Scheme.{u}} {f : C ⟶ S} {y : Y ⟶ S} {r : ℕ}
    (U : RelEffCartierDiv f r y) {S' : Scheme.{u}} (s : S' ⟶ S) :
    RelEffCartierDiv (pullback.snd f s) r (pullback.snd y s)
theorem

changeBase_pullbackAlong

L135 ↗
AlgebraicGeometry.RelEffCartierDiv.changeBase_pullbackAlong
Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.RelEffCartierDiv
Lean source · full declaration
theorem changeBase_pullbackAlong {C S Y S' T : Scheme.{u}}
    {f : C ⟶ S} {y : Y ⟶ S} {r : ℕ} (U : RelEffCartierDiv f r y)
    (s : S' ⟶ S) {g : T ⟶ S'} (φ : T ⟶ pullback y s)
    (hφ : φ ≫ pullback.snd y s = g) :
    changeBaseEquiv f s g r ((U.changeBase s).pullbackAlong φ hφ) =
      U.pullbackAlong (φ ≫ pullback.fst y s)
        (by rw [Category.assoc, pullback.condition, ← Category.assoc, hφ]) := by
  rw [changeBaseEquiv_pullbackAlong]
  change ((changeBaseEquiv f s (pullback.snd y s) r)
    ((changeBaseEquiv f s (pullback.snd y s) r).symm _)).pullbackAlong _ _ = _
  rw [Equiv.apply_symm_apply, pullbackAlong_comp]
theorem

changeBase

L149 ↗
AlgebraicGeometry.RelEffCartierDiv.IsUniversal.changeBase
Documentation

Universality is preserved by arbitrary scalar extension, with the classifying morphism constructed in the actual scheme pullback.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.RelEffCartierDiv
Lean source · statement
theorem IsUniversal.changeBase {C S Y S' : Scheme.{u}}
    {f : C ⟶ S} {y : Y ⟶ S} {r : ℕ} {U : RelEffCartierDiv f r y}
    (hU : U.IsUniversal) (s : S' ⟶ S) : (U.changeBase s).IsUniversal
theorem

changeBase_lift_fst

L183 ↗
AlgebraicGeometry.RelEffCartierDiv.IsUniversal.changeBase_lift_fst
Documentation

The classifier after scalar extension projects to the original classifier of the same actual divisor.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.RelEffCartierDiv
Lean source · statement
theorem IsUniversal.changeBase_lift_fst {C S Y S' T : Scheme.{u}}
    {f : C ⟶ S} {y : Y ⟶ S} {r : ℕ} {U : RelEffCartierDiv f r y}
    (hU : U.IsUniversal) (s : S' ⟶ S) {g : T ⟶ S'}
    (D : RelEffCartierDiv (pullback.snd f s) r g) :
    (hU.changeBase s).lift D ≫ pullback.fst y s =
      hU.lift (changeBaseEquiv f s g r D)
theorem

changeBaseEquiv_invModule_iso

L199 ↗
AlgebraicGeometry.RelEffCartierDiv.changeBaseEquiv_invModule_iso
Documentation

The inverse ideal module defining the divisor line bundle is transported by the actual pullback associativity isomorphism.

Source context 4 commands

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

noncomputable section
universe u
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.RelEffCartierDiv
Lean source · statement
theorem changeBaseEquiv_invModule_iso {C S S' T : Scheme.{u}}
    (f : C ⟶ S) [IsSeparated f] [SmoothOfRelativeDimension 1 f]
    (s : S' ⟶ S) (g : T ⟶ S') {r : ℕ}
    (D : RelEffCartierDiv f r (g ≫ s)) :
    Nonempty ((Scheme.Modules.pullback (pullbackLeftPullbackSndIso f s g).hom).obj
      D.I.invModule ≅ ((changeBaseEquiv f s g r).symm D).I.invModule)

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