AlgebraicGeometry.RelPicard.eulerChar_pullback_firstLine_sectionTwist_tensor_idealModule_eq
The first rational component has Euler characteristic equal to the prescribed genus plus one.
Source context 12 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicGeometry.RelPicard
open _root_.JacobianVarieties.Picard.Proofs.FirstLineTwistEuler
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_.NeronModelInfra
open _root_.AlgebraicCurveLean source · statement
theorem eulerChar_pullback_firstLine_sectionTwist_tensor_idealModule_eq
(R : Type u) [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) [IsProper c]
(U : C.Opens) [SmoothOfRelativeDimension 1 (U.ι ≫ c)]
(ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (hεU : Set.range ε.1 ⊆ (U : Set C))
(e r : ℕ) (g : ℕ) (hr : g + e = r)
(Dγ : RelEffCartierDiv c e (𝟙 (Spec (CommRingCat.of R)))) (hDγU : Dγ.SupportedIn U)
(k : Type u) [Field k] [IsAlgClosed k] [DecidableEq (RatFunc k)]
(s : Spec (CommRingCat.of k) ⟶ Spec (CommRingCat.of R)) [IsReduced (pullback c s)]
(M₁ M₂ : CurveModel k (RatFunc k)) (i₁ : M₁.C ⟶ pullback c s) (i₂ : M₂.C ⟶ pullback c s)
[IsClosedImmersion i₁] [IsClosedImmersion i₂]
(n : ℕ) (a b : Fin n → kˣ) (hi₁ : i₁ ≫ pullback.snd c s = M₁.toBase)
(hcover : Set.range i₁.base ∪ Set.range i₂.base = Set.univ)
(hinter : ∀ (p : M₁.C) (q : M₂.C), i₁.base p = i₂.base q →
∃ i, p = (M₁.placeEquiv.symm (RationalFunctionField.placeOfPoint k (a i : k))).1 ∧
q = (M₂.placeEquiv.symm (RationalFunctionField.placeOfPoint k (b i : k))).1)
(hεinf : i₁.base (M₁.placeEquiv.symm (RationalFunctionField.placeInfty k)).1 =
((sectionFibrePoint ε s).1).base (IsLocalRing.closedPoint k))
(hcomp : Set.range i₁.base ∩ ((pullback.fst c s ⁻¹ᵁ U : (pullback c s).Opens) : Set ↥(pullback
c s)) =
connectedComponentIn ((pullback.fst c s ⁻¹ᵁ U : (pullback c s).Opens) : Set ↥(pullback c
s)) (((sectionFibrePoint ε s).1).base (IsLocalRing.closedPoint k)))
(hnodesU : ∀ i, i₁.base (M₁.placeEquiv.symm (RationalFunctionField.placeOfPoint k (a i : k))).1
∉
(pullback.fst c s ⁻¹ᵁ U : (pullback c s).Opens))
(hW₁ : ∃ W₁ : (pullback c s).Opens, (W₁ : Set ↥(pullback c s)) = (Set.range i₂.base)ᶜ ∧
IsOpenImmersion ((i₁ ⁻¹ᵁ W₁).ι ≫ i₁))
(hDγcomp : (pullback.fst c s).base ⁻¹' ((Dγ.I.subschemeι ≫ pullback.fst c (𝟙 _)).base ''
Set.univ) ⊆
connectedComponentIn ((pullback.fst c s ⁻¹ᵁ U : (pullback c s).Opens) : Set ↥(pullback c s))
(((sectionFibrePoint ε s).1).base (IsLocalRing.closedPoint k))) :
∀ 𝒲' : M₁.C.TwoAffineOpenCover,
(Module.finrank k ↥(𝒲'.sectionsOf M₁.toBase ((Scheme.Modules.pullback i₁).obj
(sectionTwist c ε s r ⊗ (Dγ.pullbackAlong s (Category.comp_id s)).idealModule))).H0 : ℤ) -
Module.finrank k (𝒲'.sectionsOf M₁.toBase ((Scheme.Modules.pullback i₁).obj
(sectionTwist c ε s r ⊗ (Dγ.pullbackAlong s (Category.comp_id s)).idealModule))).H1 = g +
1