NYLL
Module

isFinite_and_finrank_subscheme_comap_sectionIdeal_pow_and_comap_I.lean

Nyll.JacobianVarieties.Picard.isFinite_and_finrank_subscheme_comap_sectionIdeal_pow_and_comap_I
11 declarations indexed from sourceView source ↗

Module documentation

Finite intersections with powers of the section ideal

The supported section-ideal intersection is finite of the specified fibre rank.

Imports24
Imported by2

Declarations

def

fibreIso

L83 ↗
JacobianVarieties.Picard.Proofs.SectionIntersectionFinite.ChildB.fibreIso
Documentation

The comparison between the iterated base-change fibre and the original fibre.

Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.SectionIntersectionFinite
attribute [-instance] AlgebraicGeometry.RelEffCartierDiv.subsingleton_of_degree_zero
attribute [-simp]
  AlgebraicGeometry.prodKerGraph_one
  AlgebraicGeometry.fibrePowOver.proj_comp
  AlgebraicGeometry.prodKerGraph_zero
  AlgebraicGeometry.RelEffCartierDiv.empty_I
  AlgebraicGeometry.fibrePowOver.proj_comp_assoc
  AlgebraicCurve.SymmetricPowerPackage.mk.sizeOf_spec
  AlgebraicCurve.SymmetricPowerPackage.mk.injEq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicCurve
open _root_.NeronModelInfra
noncomputable section
namespace ChildB
variable {R : Type u} [CommRing R]
section FibreIso
variable {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) {T : Scheme.{u}} (t : T ⟶ Spec
  (CommRingCat.of R))
  {k : Type u} [Field k] (s : Spec (CommRingCat.of k) ⟶ T) (x : Spec (CommRingCat.of k) ⟶ Spec
    (CommRingCat.of R))
  (hx : s ≫ t = x)
Lean source · statement
def fibreIso : pullback (pullback.snd c t) s ≅ pullback c x
theorem

fibreIso_hom_snd

L87 ↗
JacobianVarieties.Picard.Proofs.SectionIntersectionFinite.ChildB.fibreIso_hom_snd
Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.SectionIntersectionFinite
attribute [-instance] AlgebraicGeometry.RelEffCartierDiv.subsingleton_of_degree_zero
attribute [-simp]
  AlgebraicGeometry.prodKerGraph_one
  AlgebraicGeometry.fibrePowOver.proj_comp
  AlgebraicGeometry.prodKerGraph_zero
  AlgebraicGeometry.RelEffCartierDiv.empty_I
  AlgebraicGeometry.fibrePowOver.proj_comp_assoc
  AlgebraicCurve.SymmetricPowerPackage.mk.sizeOf_spec
  AlgebraicCurve.SymmetricPowerPackage.mk.injEq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicCurve
open _root_.NeronModelInfra
noncomputable section
namespace ChildB
variable {R : Type u} [CommRing R]
section FibreIso
variable {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) {T : Scheme.{u}} (t : T ⟶ Spec
  (CommRingCat.of R))
  {k : Type u} [Field k] (s : Spec (CommRingCat.of k) ⟶ T) (x : Spec (CommRingCat.of k) ⟶ Spec
    (CommRingCat.of R))
  (hx : s ≫ t = x)
Lean source · statement
theorem fibreIso_hom_snd : (fibreIso c t s x hx).hom ≫ pullback.snd c x = fibreAt c t s
theorem

fibreIso_hom_fst

L94 ↗
JacobianVarieties.Picard.Proofs.SectionIntersectionFinite.ChildB.fibreIso_hom_fst
Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.SectionIntersectionFinite
attribute [-instance] AlgebraicGeometry.RelEffCartierDiv.subsingleton_of_degree_zero
attribute [-simp]
  AlgebraicGeometry.prodKerGraph_one
  AlgebraicGeometry.fibrePowOver.proj_comp
  AlgebraicGeometry.prodKerGraph_zero
  AlgebraicGeometry.RelEffCartierDiv.empty_I
  AlgebraicGeometry.fibrePowOver.proj_comp_assoc
  AlgebraicCurve.SymmetricPowerPackage.mk.sizeOf_spec
  AlgebraicCurve.SymmetricPowerPackage.mk.injEq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicCurve
open _root_.NeronModelInfra
noncomputable section
namespace ChildB
variable {R : Type u} [CommRing R]
section FibreIso
variable {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) {T : Scheme.{u}} (t : T ⟶ Spec
  (CommRingCat.of R))
  {k : Type u} [Field k] (s : Spec (CommRingCat.of k) ⟶ T) (x : Spec (CommRingCat.of k) ⟶ Spec
    (CommRingCat.of R))
  (hx : s ≫ t = x)
Lean source · statement
theorem fibreIso_hom_fst :
    (fibreIso c t s x hx).hom ≫ pullback.fst c x = pullback.fst (pullback.snd c t) s ≫ pullback.fst
      c t
theorem

fibreIso_inv_fibreAt

L101 ↗
JacobianVarieties.Picard.Proofs.SectionIntersectionFinite.ChildB.fibreIso_inv_fibreAt
Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.SectionIntersectionFinite
attribute [-instance] AlgebraicGeometry.RelEffCartierDiv.subsingleton_of_degree_zero
attribute [-simp]
  AlgebraicGeometry.prodKerGraph_one
  AlgebraicGeometry.fibrePowOver.proj_comp
  AlgebraicGeometry.prodKerGraph_zero
  AlgebraicGeometry.RelEffCartierDiv.empty_I
  AlgebraicGeometry.fibrePowOver.proj_comp_assoc
  AlgebraicCurve.SymmetricPowerPackage.mk.sizeOf_spec
  AlgebraicCurve.SymmetricPowerPackage.mk.injEq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicCurve
open _root_.NeronModelInfra
noncomputable section
namespace ChildB
variable {R : Type u} [CommRing R]
section FibreIso
variable {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) {T : Scheme.{u}} (t : T ⟶ Spec
  (CommRingCat.of R))
  {k : Type u} [Field k] (s : Spec (CommRingCat.of k) ⟶ T) (x : Spec (CommRingCat.of k) ⟶ Spec
    (CommRingCat.of R))
  (hx : s ≫ t = x)
Lean source · statement
theorem fibreIso_inv_fibreAt : (fibreIso c t s x hx).inv ≫ fibreAt c t s = pullback.snd c x
theorem

fibreIso_hom_baseChangeSnd

L104 ↗
JacobianVarieties.Picard.Proofs.SectionIntersectionFinite.ChildB.fibreIso_hom_baseChangeSnd
Source context 18 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.SectionIntersectionFinite
attribute [-instance] AlgebraicGeometry.RelEffCartierDiv.subsingleton_of_degree_zero
attribute [-simp]
  AlgebraicGeometry.prodKerGraph_one
  AlgebraicGeometry.fibrePowOver.proj_comp
  AlgebraicGeometry.prodKerGraph_zero
  AlgebraicGeometry.RelEffCartierDiv.empty_I
  AlgebraicGeometry.fibrePowOver.proj_comp_assoc
  AlgebraicCurve.SymmetricPowerPackage.mk.sizeOf_spec
  AlgebraicCurve.SymmetricPowerPackage.mk.injEq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicCurve
open _root_.NeronModelInfra
noncomputable section
namespace ChildB
variable {R : Type u} [CommRing R]
section FibreIso
variable {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) {T : Scheme.{u}} (t : T ⟶ Spec
  (CommRingCat.of R))
  {k : Type u} [Field k] (s : Spec (CommRingCat.of k) ⟶ T) (x : Spec (CommRingCat.of k) ⟶ Spec
    (CommRingCat.of R))
  (hx : s ≫ t = x)
Lean source · statement
theorem fibreIso_hom_baseChangeSnd :
    (fibreIso c t s x hx).hom ≫ baseChangeSnd c (⟨s, hx⟩ : SchemeHomOver x t)
      = pullback.fst (pullback.snd c t) s
theorem

comap_pow

L118 ↗
JacobianVarieties.Picard.Proofs.SectionIntersectionFinite.ChildB.comap_pow
Source context 16 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.SectionIntersectionFinite
attribute [-instance] AlgebraicGeometry.RelEffCartierDiv.subsingleton_of_degree_zero
attribute [-simp]
  AlgebraicGeometry.prodKerGraph_one
  AlgebraicGeometry.fibrePowOver.proj_comp
  AlgebraicGeometry.prodKerGraph_zero
  AlgebraicGeometry.RelEffCartierDiv.empty_I
  AlgebraicGeometry.fibrePowOver.proj_comp_assoc
  AlgebraicCurve.SymmetricPowerPackage.mk.sizeOf_spec
  AlgebraicCurve.SymmetricPowerPackage.mk.injEq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicCurve
open _root_.NeronModelInfra
noncomputable section
namespace ChildB
variable {R : Type u} [CommRing R]
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

L126 ↗
JacobianVarieties.Picard.Proofs.SectionIntersectionFinite.ChildB.sectionIdeal_comap
Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.SectionIntersectionFinite
attribute [-instance] AlgebraicGeometry.RelEffCartierDiv.subsingleton_of_degree_zero
attribute [-simp]
  AlgebraicGeometry.prodKerGraph_one
  AlgebraicGeometry.fibrePowOver.proj_comp
  AlgebraicGeometry.prodKerGraph_zero
  AlgebraicGeometry.RelEffCartierDiv.empty_I
  AlgebraicGeometry.fibrePowOver.proj_comp_assoc
  AlgebraicCurve.SymmetricPowerPackage.mk.sizeOf_spec
  AlgebraicCurve.SymmetricPowerPackage.mk.injEq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicCurve
open _root_.NeronModelInfra
noncomputable section
namespace ChildB
variable {R : Type u} [CommRing R]
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

exists_sectionU

L144 ↗
JacobianVarieties.Picard.Proofs.SectionIntersectionFinite.ChildB.exists_sectionU
Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.SectionIntersectionFinite
attribute [-instance] AlgebraicGeometry.RelEffCartierDiv.subsingleton_of_degree_zero
attribute [-simp]
  AlgebraicGeometry.prodKerGraph_one
  AlgebraicGeometry.fibrePowOver.proj_comp
  AlgebraicGeometry.prodKerGraph_zero
  AlgebraicGeometry.RelEffCartierDiv.empty_I
  AlgebraicGeometry.fibrePowOver.proj_comp_assoc
  AlgebraicCurve.SymmetricPowerPackage.mk.sizeOf_spec
  AlgebraicCurve.SymmetricPowerPackage.mk.injEq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicCurve
open _root_.NeronModelInfra
noncomputable section
namespace ChildB
variable {R : Type u} [CommRing R]
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
Lean source · full declaration
theorem exists_sectionU (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)) :
    ∃ σU : T ⟶ pullback (U.ι ≫ c) t,
      σU ≫ pullback.snd (U.ι ≫ c) t = 𝟙 T ∧
      (RelPicard.sectionIdeal c ε t).comap (pullback.map (U.ι ≫ c) t c t U.ι (𝟙 T) (𝟙 _)
        (by rw [Category.comp_id]) (by rw [Category.id_comp, Category.comp_id])) = σU.ker ∧
      ((RelPicard.sectionIdeal c ε t).support : Set ↥(pullback c t)) ⊆
        Set.range (pullback.map (U.ι ≫ c) t c t U.ι (𝟙 T) (𝟙 _)
          (by rw [Category.comp_id]) (by rw [Category.id_comp, Category.comp_id])) := by
  set j := pullback.map (U.ι ≫ c) t c t U.ι (𝟙 T) (𝟙 _)
    (by rw [Category.comp_id]) (by rw [Category.id_comp, Category.comp_id]) with hj
  let εU : Spec (CommRingCat.of R) ⟶ (U : Scheme.{u}) :=
    IsOpenImmersion.lift U.ι ε.1 (by rwa [Scheme.Opens.range_ι])
  have hεU' : εU ≫ U.ι = ε.1 := IsOpenImmersion.lift_fac _ _ _
  set σU : T ⟶ pullback (U.ι ≫ c) t := pullback.lift (t ≫ εU) (𝟙 T)
    (by
      rw [Category.assoc, ← Category.assoc εU, hεU', ε.2, Category.comp_id,
        Category.id_comp]) with hσUdef
  have hσU : σU ≫ pullback.snd (U.ι ≫ c) t = 𝟙 T := by rw [hσUdef, pullback.lift_snd]
  have hσj : σU ≫ j = RelPicard.rigSection c t ε := by
    apply pullback.hom_ext
    · simp only [RelPicard.rigSection, hj, Category.assoc, pullback.lift_fst]
      rw [hσUdef, pullback.lift_fst_assoc, Category.assoc, hεU']
    · simp only [RelPicard.rigSection, hj, Category.assoc, pullback.lift_snd, Category.comp_id]
      exact hσU
  have : IsClosedImmersion (RelPicard.rigSection c t ε) := by
    have : IsClosedImmersion (RelPicard.rigSection c t ε ≫ pullback.snd c t) := by
      rw [RelPicard.rigSection, pullback.lift_snd]; infer_instance
    exact .of_comp (RelPicard.rigSection c t ε) (pullback.snd c t)
  have hcomap : (RelPicard.sectionIdeal c ε t).comap j = σU.ker := by
    change (RelPicard.rigSection c t ε).ker.comap j = σU.ker
    rw [← Scheme.IdealSheafData.ker_fst_of_isClosedImmersion]
    have hsurj : IsIso (pullback.snd j (RelPicard.rigSection c t ε)) := by
      refine isIso_of_isOpenImmersion_of_opensRange_eq_top _ ?_
      ext z
      simp only [Scheme.Hom.coe_opensRange, TopologicalSpace.Opens.coe_top, Set.mem_univ, iff_true]
      rw [Scheme.Pullback.range_snd, ← hσj]
      exact ⟨σU z, (Scheme.Hom.comp_apply _ _ z).symm⟩
    have hfst : pullback.fst j (RelPicard.rigSection c t ε) = pullback.snd j (RelPicard.rigSection
      c t ε) ≫ σU := by
      rw [← cancel_mono j, Category.assoc, hσj]
      exact pullback.condition
    rw [hfst, Scheme.Hom.ker_comp_of_isIso]
  refine ⟨σU, hσU, hcomap, ?_⟩
  change ((RelPicard.rigSection c t ε).ker.support : Set ↥(pullback c t)) ⊆ Set.range ⇑j
  rw [Scheme.Hom.support_ker,
    (RelPicard.rigSection c t ε).isClosedEmbedding.isClosed_range.closure_eq, ← hσj]
  rintro _ ⟨z, rfl⟩
  exact ⟨σU z, (Scheme.Hom.comp_apply _ _ z).symm⟩
theorem

transport_line

L196 ↗
JacobianVarieties.Picard.Proofs.SectionIntersectionFinite.ChildB.transport_line
Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.SectionIntersectionFinite
attribute [-instance] AlgebraicGeometry.RelEffCartierDiv.subsingleton_of_degree_zero
attribute [-simp]
  AlgebraicGeometry.prodKerGraph_one
  AlgebraicGeometry.fibrePowOver.proj_comp
  AlgebraicGeometry.prodKerGraph_zero
  AlgebraicGeometry.RelEffCartierDiv.empty_I
  AlgebraicGeometry.fibrePowOver.proj_comp_assoc
  AlgebraicCurve.SymmetricPowerPackage.mk.sizeOf_spec
  AlgebraicCurve.SymmetricPowerPackage.mk.injEq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicCurve
open _root_.NeronModelInfra
noncomputable section
namespace ChildB
variable {R : Type u} [CommRing R]
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
Lean source · statement
theorem transport_line {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) {k : Type u} [Field k] (pt : Spec
      (CommRingCat.of k) ⟶ T)
    {Y : Scheme.{u}} (y : Y ⟶ Spec (CommRingCat.of k)) (i₁ : Y ⟶ pullback (pullback.snd c t) pt)
    (hi₁ : i₁ ≫ fibreAt c t pt = y)
    (W₁ : (pullback (pullback.snd c t) pt).Opens) [IsOpenImmersion ((i₁ ⁻¹ᵁ W₁).ι ≫ i₁)]
    (hW₁ : (W₁ : Set ↥(pullback (pullback.snd c t) pt)) ⊆ Set.range i₁.base)
    (K : (pullback c t).IdealSheafData)
    (hW : ∀ z : ↥(pullback (pullback.snd c t) pt), (pullback.fst (pullback.snd c t) pt).base z ∈
      K.support → z ∈ W₁)
    (K' : (pullback (pullback.snd c t) pt).IdealSheafData) (hK' : K' = K.comap (pullback.fst
      (pullback.snd c t) pt))
    {n : ℕ} (hfin : IsFinite (K'.subschemeι ≫ fibreAt c t pt))
    (hdeg : ∀ q : Spec (CommRingCat.of k), (K'.subschemeι ≫ fibreAt c t pt).finrank q = n) :
    IsFinite ((K.comap (i₁ ≫ pullback.fst (pullback.snd c t) pt)).subschemeι ≫ y) ∧
      ∀ q : Spec (CommRingCat.of k), ((K.comap (i₁ ≫ pullback.fst (pullback.snd c t)
        pt)).subschemeι ≫ y).finrank q = n
theorem

transport_fibreIso

L256 ↗
JacobianVarieties.Picard.Proofs.SectionIntersectionFinite.ChildB.transport_fibreIso
Source context 17 commands

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

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.SectionIntersectionFinite
attribute [-instance] AlgebraicGeometry.RelEffCartierDiv.subsingleton_of_degree_zero
attribute [-simp]
  AlgebraicGeometry.prodKerGraph_one
  AlgebraicGeometry.fibrePowOver.proj_comp
  AlgebraicGeometry.prodKerGraph_zero
  AlgebraicGeometry.RelEffCartierDiv.empty_I
  AlgebraicGeometry.fibrePowOver.proj_comp_assoc
  AlgebraicCurve.SymmetricPowerPackage.mk.sizeOf_spec
  AlgebraicCurve.SymmetricPowerPackage.mk.injEq
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicCurve
open _root_.NeronModelInfra
noncomputable section
namespace ChildB
variable {R : Type u} [CommRing R]
variable {R : Type u} [CommRing R] {C : Scheme.{u}}
Lean source · statement
theorem transport_fibreIso {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) {k : Type u} [Field k] (pt : Spec
      (CommRingCat.of k) ⟶ T)
    (Kk : (pullback c (pt ≫ t)).IdealSheafData) {n : ℕ}
    (hfin : IsFinite (Kk.subschemeι ≫ pullback.snd c (pt ≫ t)))
    (hdeg : ∀ q : Spec (CommRingCat.of k), (Kk.subschemeι ≫ pullback.snd c (pt ≫ t)).finrank q = n)
      :
    IsFinite ((Kk.comap (fibreIso c t pt (pt ≫ t) rfl).hom).subschemeι ≫ fibreAt c t pt) ∧
      ∀ q : Spec (CommRingCat.of k),
        ((Kk.comap (fibreIso c t pt (pt ≫ t) rfl).hom).subschemeι ≫ fibreAt c t pt).finrank q = n
theorem

isFinite_and_finrank_subscheme_comap_sectionIdeal_pow_and_comap_I

L299 ↗
AlgebraicGeometry.RelPicard.isFinite_and_finrank_subscheme_comap_sectionIdeal_pow_and_comap_I
Documentation

The supported section-ideal intersection is finite of the specified fibre rank.

Source context 14 commands

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

section ProofImplementation
namespace AlgebraicGeometry.RelPicard
noncomputable section
open _root_.JacobianVarieties.Picard.Proofs.SectionIntersectionFinite
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.Opposite
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.AlgebraicCurve
open _root_.NeronModelInfra
open ChildB in
Lean source · statement
theorem isFinite_and_finrank_subscheme_comap_sectionIdeal_pow_and_comap_I
    (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εU : Set.range ε.1 ⊆ (U : Set C))
    {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (r : ℕ) {e : ℕ} (D : RelEffCartierDiv c e t)
    {k : Type u} [Field k] (pt : Spec (CommRingCat.of k) ⟶ T)
    {F₁ : Type u} [Field F₁] [Algebra k F₁] (M₁ : CurveModel k F₁)
    (i₁ : M₁.C ⟶ pullback (pullback.snd c t) pt) (hi₁ : i₁ ≫ fibreAt c t pt = M₁.toBase)
    (W₁ : (pullback (pullback.snd c t) pt).Opens) [IsOpenImmersion ((i₁ ⁻¹ᵁ W₁).ι ≫ i₁)]
    (hW₁ : (W₁ : Set ↥(pullback (pullback.snd c t) pt)) ⊆ Set.range i₁.base)
    (hD : ∀ y : ↥(pullback (pullback.snd c t) pt), (pullback.fst (pullback.snd c t) pt).base y ∈
      D.I.support → y ∈ W₁)
    (hε : ∀ y : ↥(pullback (pullback.snd c t) pt), (pullback.fst (pullback.snd c t) pt).base y ∈
      Set.range (rigSection c t ε).base → y ∈ W₁) :
    IsFinite ((((sectionIdeal c ε t) ^ r).comap (i₁ ≫ pullback.fst (pullback.snd c t)
      pt)).subschemeι ≫ M₁.toBase) ∧
      (∀ q : Spec (CommRingCat.of k),
        ((((sectionIdeal c ε t) ^ r).comap (i₁ ≫ pullback.fst (pullback.snd c t) pt)).subschemeι ≫
          M₁.toBase).finrank q = r) ∧
      IsFinite (((D.I.comap (i₁ ≫ pullback.fst (pullback.snd c t) pt))).subschemeι ≫ M₁.toBase) ∧
      (∀ q : Spec (CommRingCat.of k),
        (((D.I.comap (i₁ ≫ pullback.fst (pullback.snd c t) pt))).subschemeι ≫ M₁.toBase).finrank q
          = e)

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