NYLL
Module

isInvertible_comap_sectionIdeal_and_finrank_eq_one_of_ideal_eq_bot.lean

Nyll.JacobianVarieties.Picard.isInvertible_comap_sectionIdeal_and_finrank_eq_one_of_ideal_eq_bot
8 declarations indexed from sourceView source ↗

Module documentation

Section ideals on a subscheme near a section

If a subscheme ideal vanishes near the section, the pulled-back section ideal is invertible and its zero scheme is finite of rank one over the field.

Imports29
Imported by1

Declarations

theorem

map_germ_ideal_eq

L111 ↗
JacobianVarieties.Picard.Proofs.SectionIdealRankOne.AlgebraicGeometry.SecDegS17.map_germ_ideal_eq
Documentation

The image of an ideal sheaf in a stalk is independent of the affine neighbourhood.

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.SectionIdealRankOne
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
namespace AlgebraicGeometry
namespace SecDegS17
open _root_.AlgebraicGeometry
Lean source · statement
theorem map_germ_ideal_eq {X : Scheme.{u}} (I : X.IdealSheafData) {x : X} (V W : X.affineOpens)
    (hV : x ∈ (V : X.Opens)) (hW : x ∈ (W : X.Opens)) :
    Ideal.map (X.presheaf.germ (V : X.Opens) x hV).hom (I.ideal V) =
      Ideal.map (X.presheaf.germ (W : X.Opens) x hW).hom (I.ideal W)
theorem

ideal_eq_bot_of_basicOpen_eq

L132 ↗
JacobianVarieties.Picard.Proofs.SectionIdealRankOne.AlgebraicGeometry.SecDegS17.ideal_eq_bot_of_basicOpen_eq
Documentation

Vanishing of an ideal on an affine open passes to an equal basic open.

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.SectionIdealRankOne
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
namespace AlgebraicGeometry
namespace SecDegS17
open _root_.AlgebraicGeometry
Lean source · statement
theorem ideal_eq_bot_of_basicOpen_eq {X : Scheme.{u}} (J : X.IdealSheafData) {V U : X.affineOpens}
    (hJV : J.ideal V = ⊥) (f : Γ(X, U)) (g : Γ(X, V)) (hfg : X.basicOpen f = X.basicOpen g) :
    J.ideal (X.affineBasicOpen f) = ⊥
theorem

map_mem_nonZeroDivisors_basicOpen

L140 ↗
JacobianVarieties.Picard.Proofs.SectionIdealRankOne.AlgebraicGeometry.SecDegS17.map_mem_nonZeroDivisors_basicOpen
Documentation

Restriction to a basic open preserves a non-zero-divisor.

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.SectionIdealRankOne
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
namespace AlgebraicGeometry
namespace SecDegS17
open _root_.AlgebraicGeometry
Lean source · statement
theorem map_mem_nonZeroDivisors_basicOpen {X : Scheme.{u}} (U : X.affineOpens) (f : Γ(X, U))
    {g : Γ(X, U)} (hg : g ∈ nonZeroDivisors Γ(X, U)) :
    (X.presheaf.map (homOfLE (X.basicOpen_le f)).op).hom g ∈
      nonZeroDivisors Γ(X, X.affineBasicOpen f)
theorem

subschemeι_app_injective_of_ideal_eq_bot

L148 ↗
JacobianVarieties.Picard.Proofs.SectionIdealRankOne.AlgebraicGeometry.SecDegS17.subschemeι_app_injective_of_ideal_eq_bot
Documentation

The subscheme inclusion is injective on sections where its ideal vanishes.

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.SectionIdealRankOne
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
namespace AlgebraicGeometry
namespace SecDegS17
open _root_.AlgebraicGeometry
Lean source · statement
theorem subschemeι_app_injective_of_ideal_eq_bot {X : Scheme.{u}} (J : X.IdealSheafData)
    (U : X.affineOpens)
    (hJ : J.ideal U = ⊥) : Function.Injective (J.subschemeι.app (U : X.Opens)).hom
theorem

map_mem_nonZeroDivisors_of_bijective

L157 ↗
JacobianVarieties.Picard.Proofs.SectionIdealRankOne.AlgebraicGeometry.SecDegS17.map_mem_nonZeroDivisors_of_bijective
Documentation

A bijective ring homomorphism preserves non-zero-divisors.

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.SectionIdealRankOne
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
namespace AlgebraicGeometry
namespace SecDegS17
open _root_.AlgebraicGeometry
Lean source · statement
theorem map_mem_nonZeroDivisors_of_bijective {A B : Type*} [CommRing A] [CommRing B] (φ : A →+* B)
    (hφ : Function.Bijective φ) {g : A} (hg : g ∈ nonZeroDivisors A) : φ g ∈ nonZeroDivisors B
theorem

isInvertible_comap_subschemeι

L166 ↗
JacobianVarieties.Picard.Proofs.SectionIdealRankOne.AlgebraicGeometry.SecDegS17.isInvertible_comap_subschemeι
Documentation

An invertible ideal stays invertible on a subscheme whose ideal vanishes near its support.

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.SectionIdealRankOne
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
namespace AlgebraicGeometry
namespace SecDegS17
open _root_.AlgebraicGeometry
Lean source · statement
theorem isInvertible_comap_subschemeι {X : Scheme.{u}} {I J : X.IdealSheafData}
    (hI : I.IsInvertible)
    (S : Set X) (hIS : ∀ x : X, x ∉ S → x ∉ I.support)
    (hJS : ∀ x ∈ S, ∃ V : X.affineOpens, x ∈ (V : X.Opens) ∧ J.ideal V = ⊥) :
    (I.comap J.subschemeι).IsInvertible
theorem

le_ker_of_ideal_eq_bot

L238 ↗
JacobianVarieties.Picard.Proofs.SectionIdealRankOne.AlgebraicGeometry.SecDegS17.le_ker_of_ideal_eq_bot
Documentation

An ideal vanishing on an affine neighbourhood of a field-valued point lies in its kernel.

Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.SectionIdealRankOne
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
namespace AlgebraicGeometry
namespace SecDegS17
open _root_.AlgebraicGeometry
Lean source · statement
theorem le_ker_of_ideal_eq_bot {X : Scheme.{u}} {k : Type u} [Field k]
    (s : Spec (CommRingCat.of k) ⟶ X)
    [QuasiCompact s] (J : X.IdealSheafData) (V : X.affineOpens)
    (hsV : Set.range s ⊆ ((V : X.Opens) : Set X)) (hJV : J.ideal V = ⊥) : J ≤ s.ker
theorem

isInvertible_comap_sectionIdeal_and_finrank_eq_one_of_ideal_eq_bot

L277 ↗
AlgebraicGeometry.RelPicard.isInvertible_comap_sectionIdeal_and_finrank_eq_one_of_ideal_eq_bot
Documentation

Near a section where the subscheme ideal vanishes, its section ideal defines a finite rank-one map.

Source context 5 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 JacobianVarieties.Picard.Proofs.SectionIdealRankOne.AlgebraicGeometry.SecDegS17
Lean source · statement
theorem isInvertible_comap_sectionIdeal_and_finrank_eq_one_of_ideal_eq_bot
    {R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) [IsSeparated c]
    (U : C.Opens) [SmoothOfRelativeDimension 1 (U.ι ≫ c)]
    (σ : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (hσ : Set.range σ.1 ⊆ (U : Set C))
    {k : Type u} [Field k] (t : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R))
    (J : (pullback c t).IdealSheafData)
    (hJ : ∃ V : (pullback c t).affineOpens,
      Set.range (rigSection c t σ) ⊆ ((V : (pullback c t).Opens) : Set ↥(pullback c t)) ∧
        J.ideal V = ⊥) :
    ((sectionIdeal c σ t).comap J.subschemeι).IsInvertible ∧
      IsFinite (((sectionIdeal c σ t).comap J.subschemeι).subschemeι ≫ J.subschemeι ≫
        pullback.snd c t) ∧
      ∀ q : Spec (CommRingCat.of k),
        (((sectionIdeal c σ t).comap J.subschemeι).subschemeι ≫ J.subschemeι ≫
          pullback.snd c t).finrank q = 1

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