NYLL
Module

support_zeroSchemeIdeal_fibre_subset_of_support_zeroSchemeIdeal_fibre_subset_extension.lean

Nyll.JacobianVarieties.Picard.support_zeroSchemeIdeal_fibre_subset_of_support_zeroSchemeIdeal_fibre_subset_extension
3 declarations indexed from sourceView source ↗

Module documentation

Descent of zero-scheme support under field extension

Faithfully flat pullback preserves nonzero sections of invertible modules. This descends a support bound from an extension of the residue field.

Imports29
Imported by1

Declarations

theorem

app_injective_of_flat_of_surjective

L139 ↗
JacobianVarieties.Picard.Proofs.ZeroSupportExtension.AlgebraicGeometry.ZerosDescent.app_injective_of_flat_of_surjective
Documentation

A flat surjective scheme morphism induces injective maps on sections.

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZeroSupportExtension
attribute [-instance]
  PresheafOfModules.PullbackMonoidal.pullback_monoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ
  PresheafOfModules.pushforward_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_η
  PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ_gS
  PresheafOfModules.pullback_oplaxMonoidal
attribute [-instance]
  instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
attribute [-instance]
  PresheafOfModules.pullback_monoidal'
  AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback_monoidal
  AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
  AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
  AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-simp] PresheafOfModules.freeεIso_hom_app PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
noncomputable section
namespace AlgebraicGeometry
namespace ZerosDescent
open _root_.AlgebraicGeometry
Lean source · statement
theorem app_injective_of_flat_of_surjective {X Y : Scheme.{u}} (π : Y ⟶ X) [Flat π] [Surjective π]
    (W : X.Opens) :
    Function.Injective (π.app W)
theorem

pullbackSection_ne_zero

L157 ↗
JacobianVarieties.Picard.Proofs.ZeroSupportExtension.AlgebraicGeometry.ZerosDescent.pullbackSection_ne_zero
Documentation

A nonzero section of an invertible module stays nonzero under flat surjective pullback.

Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.ZeroSupportExtension
attribute [-instance]
  PresheafOfModules.PullbackMonoidal.pullback_monoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ
  PresheafOfModules.pushforward_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_η
  PresheafOfModules.free_monoidal
  PresheafOfModules.restrictScalars_laxMonoidal
  PresheafOfModules.PullbackMonoidal.isIso_δ_gS
  PresheafOfModules.pullback_oplaxMonoidal
attribute [-instance]
  instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
attribute [-instance]
  PresheafOfModules.pullback_monoidal'
  AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback_monoidal
  AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
  AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
  AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
  AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
  AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-simp] PresheafOfModules.freeεIso_hom_app PresheafOfModules.freeμIso_hom_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
noncomputable section
namespace AlgebraicGeometry
namespace ZerosDescent
open _root_.AlgebraicGeometry
Lean source · statement
theorem pullbackSection_ne_zero {X Y : Scheme.{u}} (π : Y ⟶ X) [Flat π] [Surjective π]
    {N : X.Modules} (hN : Scheme.Modules.IsInvertible N) (τ : 𝟙_ X.Modules ⟶ N) (hτ : τ ≠ 0) :
    Scheme.Modules.pullbackSection π τ ≠ 0
theorem

support_zeroSchemeIdeal_fibre_subset_of_support_zeroSchemeIdeal_fibre_subset_extension

L246 ↗
AlgebraicGeometry.RelPicard.support_zeroSchemeIdeal_fibre_subset_of_support_zeroSchemeIdeal_fibre_subset_extension
Documentation

A bound on zero-scheme supports after a field extension descends to the original fibre.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicGeometry.RelPicard
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra
open CategoryTheory.MonoidalCategory
open JacobianVarieties.Picard.Proofs.ZeroSupportExtension.AlgebraicGeometry.ZerosDescent
Lean source · statement
theorem support_zeroSchemeIdeal_fibre_subset_of_support_zeroSchemeIdeal_fibre_subset_extension
    {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) (U : C.Opens)
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (M : (pullback c t).Modules)
    (hM : Scheme.Modules.IsInvertible M)
    {k : Type u} [Field k] (s : Spec (CommRingCat.of k) ⟶ T)
    (K : Type u) [Field K] [Algebra k K]
    (hK : ∀ τ : 𝟙_ (pullback c ((Scheme.TwoAffineOpenCover.specMap k K ≫ s) ≫ t)).Modules ⟶
        (Scheme.Modules.pullback (mapOnProdOver c (Scheme.TwoAffineOpenCover.specMap k K ≫ s)
          rfl)).obj M,
      τ ≠ 0 →
        ((Scheme.Modules.zeroSchemeIdeal τ).support : Set ↥(pullback c
          ((Scheme.TwoAffineOpenCover.specMap k K ≫ s) ≫ t))) ⊆
          ((pullback.fst c ((Scheme.TwoAffineOpenCover.specMap k K ≫ s) ≫ t)) ⁻¹ᵁ U :
            Set ↥(pullback c ((Scheme.TwoAffineOpenCover.specMap k K ≫ s) ≫ t)))) :
    ∀ τ : 𝟙_ (pullback c (s ≫ t)).Modules ⟶ (Scheme.Modules.pullback (mapOnProdOver c s rfl)).obj M,
      τ ≠ 0 →
        ((Scheme.Modules.zeroSchemeIdeal τ).support : Set ↥(pullback c (s ≫ t))) ⊆
          ((pullback.fst c (s ≫ t)) ⁻¹ᵁ U : Set ↥(pullback c (s ≫ t)))

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