NYLL
Module

RigidifiedLineBundleOfInvertible.lean

Nyll.AlgebraicCurves.Geometry.Schemes.RigidifiedLineBundleOfInvertible
15 declarations indexed from sourceView source ↗

Module documentation

Rigidified line bundles, their tensor products and tensor inverses, and compatibility with pullback.

Imports9
Imported by45

Declarations

def

isoOfTensorIsoUnit

L43 ↗
AlgebraicGeometry.Scheme.Modules.isoOfTensorIsoUnit
Documentation

The isomorphism identifying two tensor inverses of the same module.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
    AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry
namespace Scheme.Modules
variable {V : Scheme.{u}}
Lean source · statement
def isoOfTensorIsoUnit (X Y Y' : V.Modules) (i : X ⊗ Y ≅ 𝟙_ _) (i' : X ⊗ Y' ≅ 𝟙_ _) : Y ≅ Y'
def

tensorTensorTensorComm

L48 ↗
AlgebraicGeometry.Scheme.Modules.tensorTensorTensorComm
Documentation

The isomorphism permuting the middle factors in a tensor product of four modules.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
    AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry
namespace Scheme.Modules
variable {V : Scheme.{u}}
Lean source · statement
def tensorTensorTensorComm (W X Y Z : V.Modules) : (W ⊗ X) ⊗ (Y ⊗ Z) ≅ (W ⊗ Y) ⊗ (X ⊗ Z)
theorem

nonempty_dual_tensorUnit_iso

L52 ↗
AlgebraicGeometry.Scheme.Modules.nonempty_dual_tensorUnit_iso
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
    AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry
namespace Scheme.Modules
variable {V : Scheme.{u}}
Lean source · statement
theorem nonempty_dual_tensorUnit_iso (V : Scheme.{u}) : Nonempty (dual (𝟙_ V.Modules) ≅ 𝟙_
    V.Modules)
theorem

rigSection_snd

L65 ↗
AlgebraicGeometry.RelPicard.rigSection_snd
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
    AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {T T' : Scheme.{u}}
  {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem rigSection_snd (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (t : T ⟶ Spec
    (CommRingCat.of R)) :
    rigSection c t ε ≫ pullback.snd c t = 𝟙 T
theorem

baseChangeSnd_snd

L70 ↗
AlgebraicGeometry.RelPicard.baseChangeSnd_snd
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
    AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {T T' : Scheme.{u}}
  {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem baseChangeSnd_snd (ψ : SchemeHomOver t' t) :
    baseChangeSnd c ψ ≫ pullback.snd c t = pullback.snd c t' ≫ ψ.1
abbrev

rigCorrection

L75 ↗
AlgebraicGeometry.RelPicard.rigCorrection
Documentation

The dual of the restriction to the rigidifying section, used to normalize the module.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
    AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {T T' : Scheme.{u}}
  {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)}
Lean source · statement
abbrev rigCorrection (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (t : T ⟶ Spec
    (CommRingCat.of R))
    (L : (Limits.pullback c t).Modules) : T.Modules
def

rigSectionPullbackSndPullbackIso

L81 ↗
AlgebraicGeometry.RelPicard.rigSectionPullbackSndPullbackIso
Documentation

Pullback along the rigidifying section cancels pullback from the base.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
    AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {T T' : Scheme.{u}}
  {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)}
Lean source · statement
def rigSectionPullbackSndPullbackIso (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (t : T
    ⟶ Spec (CommRingCat.of R))
    (D : T.Modules) :
    (Scheme.Modules.pullback (rigSection c t ε)).obj ((Scheme.Modules.pullback (pullback.snd c
      t)).obj D) ≅ D
def

ofInvertible

L92 ↗
AlgebraicGeometry.RelPicard.RigidifiedLineBundle.ofInvertible
Documentation

The rigidified line bundle obtained by normalizing an invertible module along the distinguished section.

Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
    AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {T T' : Scheme.{u}}
  {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)}
Lean source · full declaration
def RigidifiedLineBundle.ofInvertible (L : (Limits.pullback c t).Modules) (hL :
    Scheme.Modules.IsInvertible L) :
    RigidifiedLineBundle c ε t where
  L := Scheme.Modules.rigidify (rigSection c t ε) (pullback.snd c t) L
  isInvertible := hL.tensor (((hL.pullback _).dual).1.pullback _)
  rigidified := ⟨Scheme.Modules.pullbackTensorObjIso _ _ _ ≪≫
    (Iso.refl _ ⊗ᵢ rigSectionPullbackSndPullbackIso ε t _) ≪≫ (hL.pullback _).dual.2.some⟩
theorem

ofInvertible_L

L100 ↗
AlgebraicGeometry.RelPicard.RigidifiedLineBundle.ofInvertible_L
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
    AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {T T' : Scheme.{u}}
  {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem RigidifiedLineBundle.ofInvertible_L (L : (Limits.pullback c t).Modules) (hL :
    Scheme.Modules.IsInvertible L) :
    (RigidifiedLineBundle.ofInvertible (ε := ε) L hL).L = Scheme.Modules.rigidify (rigSection c
      t ε) (pullback.snd c t) L
theorem

ofInvertible_L_eq_tensor

L105 ↗
AlgebraicGeometry.RelPicard.RigidifiedLineBundle.ofInvertible_L_eq_tensor
Source context 6 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
    AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {T T' : Scheme.{u}}
  {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)}
Lean source · statement
theorem RigidifiedLineBundle.ofInvertible_L_eq_tensor (L : (Limits.pullback c t).Modules) (hL :
    Scheme.Modules.IsInvertible L) :
    (RigidifiedLineBundle.ofInvertible (ε := ε) L hL).L =
      L ⊗ (Scheme.Modules.pullback (pullback.snd c t)).obj (rigCorrection ε t L)
theorem

nonempty_ofInvertible_iso_of_iso

L112 ↗
AlgebraicGeometry.RelPicard.RigidifiedLineBundle.nonempty_ofInvertible_iso_of_iso
Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
    AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {T T' : Scheme.{u}}
  {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)}
namespace RigidifiedLineBundle
Lean source · statement
theorem nonempty_ofInvertible_iso_of_iso {L L' : (Limits.pullback c t).Modules} (hL :
    Scheme.Modules.IsInvertible L)
    (hL' : Scheme.Modules.IsInvertible L') (e : L ≅ L') :
    Nonempty ((ofInvertible (ε := ε) L hL).L ≅ (ofInvertible (ε := ε) L' hL').L)
theorem

nonempty_ofInvertible_iso_of_rigidified

L118 ↗
AlgebraicGeometry.RelPicard.RigidifiedLineBundle.nonempty_ofInvertible_iso_of_rigidified
Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
    AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {T T' : Scheme.{u}}
  {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)}
namespace RigidifiedLineBundle
Lean source · statement
theorem nonempty_ofInvertible_iso_of_rigidified (M : RigidifiedLineBundle c ε t) :
    Nonempty ((ofInvertible (ε := ε) M.L M.isInvertible).L ≅ M.L)
theorem

nonempty_ofInvertible_tensor_iso

L126 ↗
AlgebraicGeometry.RelPicard.RigidifiedLineBundle.nonempty_ofInvertible_tensor_iso
Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
    AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {T T' : Scheme.{u}}
  {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)}
namespace RigidifiedLineBundle
Lean source · statement
theorem nonempty_ofInvertible_tensor_iso {L L' : (Limits.pullback c t).Modules} (hL :
    Scheme.Modules.IsInvertible L)
    (hL' : Scheme.Modules.IsInvertible L') :
    Nonempty ((ofInvertible (ε := ε) (L ⊗ L') (hL.tensor hL')).L ≅
      ((ofInvertible (ε := ε) L hL).tensor (ofInvertible (ε := ε) L' hL')).L)
theorem

nonempty_ofInvertible_pullbackSnd_tensor_iso

L139 ↗
AlgebraicGeometry.RelPicard.RigidifiedLineBundle.nonempty_ofInvertible_pullbackSnd_tensor_iso
Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
    AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {T T' : Scheme.{u}}
  {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)}
namespace RigidifiedLineBundle
Lean source · statement
theorem nonempty_ofInvertible_pullbackSnd_tensor_iso {N : T.Modules} (hN :
    Scheme.Modules.IsInvertible N)
    {L : (Limits.pullback c t).Modules} (hL : Scheme.Modules.IsInvertible L) :
    Nonempty ((ofInvertible (ε := ε) ((Scheme.Modules.pullback (pullback.snd c t)).obj N ⊗ L)
      ((hN.pullback _).tensor hL)).L ≅
      (ofInvertible (ε := ε) L hL).L)
theorem

nonempty_ofInvertible_pullbackAlong_iso

L157 ↗
AlgebraicGeometry.RelPicard.RigidifiedLineBundle.nonempty_ofInvertible_pullbackAlong_iso
Source context 7 commands

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

universe u
open CategoryTheory CategoryTheory.Limits MonoidalCategory AlgebraicGeometry
    AlgebraicGeometry.RelPicard
  NeronModelInfra GoodReductionJacobian
noncomputable section
namespace AlgebraicGeometry
namespace RelPicard
variable {R : Type u} [CommRing R] {C : Scheme.{u}} {c : C ⟶ Spec (CommRingCat.of R)}
  {ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c} {T T' : Scheme.{u}}
  {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)}
namespace RigidifiedLineBundle
Lean source · statement
theorem nonempty_ofInvertible_pullbackAlong_iso (ψ : SchemeHomOver t' t) {L : (Limits.pullback c
    t).Modules}
    (hL : Scheme.Modules.IsInvertible L) :
    Nonempty (((ofInvertible (ε := ε) L hL).pullbackAlong ψ).L ≅
      (ofInvertible (ε := ε) ((Scheme.Modules.pullback (baseChangeSnd c ψ)).obj L) (hL.pullback
        _)).L)

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