Module

nonempty_pullback_sectionIdeal_pow_module_iso_of_smoothLocus.lean

Nyll.JacobianVarieties.Picard.nonempty_pullback_sectionIdeal_pow_module_iso_of_smoothLocus

4 declarations indexed from sourceView source ↗

Module documentation

Powers of the section ideal under base change on the smooth locus

The section ideal is invertible when the section lies in the relative smooth curve locus. Its powers commute with base change, and the invertible-ideal comparison identifies the associated pulled-back modules.

Imports27

Mathlib.Util.WithWeakNamespace
Mathlib.AlgebraicGeometry.Scheme
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.AlgebraicGeometry.Pullbacks
Mathlib.AlgebraicGeometry.PullbackCarrier
Mathlib.AlgebraicGeometry.IdealSheaf.Basic
Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Mathlib.AlgebraicGeometry.Morphisms.Separated
Mathlib.AlgebraicGeometry.Morphisms.Smooth
Mathlib.CategoryTheory.MorphismProperty.Limits
Mathlib.CategoryTheory.Iso
Mathlib.CategoryTheory.EqToHom
Mathlib.Algebra.Group.Defs
Nyll.AlgebraicCurves.Geometry.Schemes.SchemeHomOver
Nyll.AlgebraicCurves.Geometry.Picard.Functor
Nyll.AlgebraicCurves.Geometry.Sheaves.IdealSheafModule
Nyll.JacobianVarieties.Picard.ThetaBundle
Nyll.AlgebraicCurves.Geometry.Sheaves.IdealSheafModuleMaps
Nyll.AlgebraicCurves.RelativeDivisors.Cartier
Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDivOfPoint
Nyll.AlgebraicCurves.RelativeDivisors.RelEffCartierDiv_pullbackAlong_ofPoint
Nyll.AlgebraicCurves.Geometry.Schemes.Scheme_Hom_isInvertible_ker_of_comp_eq_id
Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_IsInvertible_pow
Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_comap_mul
Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_IsInvertible_isIso_pullbackModuleComparison
Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_IdealSheafData_IsInvertible_of_comap_of_support_subset_range

Imported by2

theorem

comap_pow

L112 ↗

JacobianVarieties.Picard.Proofs.SmoothSectionPower.AlgebraicGeometry.RelPicard.IdealBC.comap_pow

Source context 13 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.SmoothSectionPower
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
namespace AlgebraicGeometry
namespace RelPicard
namespace IdealBC
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry

Lean source · statement

theorem comap_pow {X Y : Scheme.{u}} (I : Y.IdealSheafData) (f : X ⟶ Y) (n : ℕ) :
    (I ^ n).comap f = (I.comap f) ^ n

theorem

sectionIdeal_comap

L121 ↗

JacobianVarieties.Picard.Proofs.SmoothSectionPower.AlgebraicGeometry.RelPicard.IdealBC.sectionIdeal_comap

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.SmoothSectionPower
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
namespace AlgebraicGeometry
namespace RelPicard
namespace IdealBC
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}}

Lean source · statement

theorem sectionIdeal_comap (c : C ⟶ Spec (CommRingCat.of R)) [IsSeparated c]
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) {T T' : Scheme.{u}}
    {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)}
    (ψ : SchemeHomOver t' t) :
    (RelPicard.sectionIdeal c ε t).comap (RelPicard.baseChangeSnd c ψ) =
      RelPicard.sectionIdeal c ε t'

theorem

isInvertible_sectionIdeal

L139 ↗

JacobianVarieties.Picard.Proofs.SmoothSectionPower.AlgebraicGeometry.RelPicard.IdealBC.isInvertible_sectionIdeal

Source context 14 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.SmoothSectionPower
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
namespace AlgebraicGeometry
namespace RelPicard
namespace IdealBC
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicGeometry
variable {R : Type u} [CommRing R] {C : Scheme.{u}}

Lean source · statement

theorem isInvertible_sectionIdeal (c : C ⟶ Spec (CommRingCat.of R))
    [IsSeparated c] (U : C.Opens) [SmoothOfRelativeDimension 1 (U.ι ≫ c)]
    (ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (hεU : Set.range ε.1 ⊆ (U : Set C))
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) :
    (RelPicard.sectionIdeal c ε t).IsInvertible

theorem