NYLL
Module

exists_forall_geomFibreH0Finrank_tensorPow_eq_hilbertFunctionOf_of_point_geomFibre.lean

Nyll.AlgebraicCurves.Geometry.Schemes.exists_forall_geomFibreH0Finrank_tensorPow_eq_hilbertFunctionOf_of_point_geomFibre
4 declarations indexed from sourceView source ↗

Module documentation

exists forall geom Fibre H0 Finrank tensor Pow eq hilbert Function Of of point geom Fibre

Imports13
Imported by2

Declarations

theorem

smul_map_eq_of_eq

L87 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_forall_geomFibreH0Finrank_tensorPow_eq_hilbertFunctionOf_of_point_geomFibre.F3Sol.smul_map_eq_of_eq
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_forall_geomFibreH0Finrank_tensorPow_eq_hilbertFunctionOf_of_point_geomFibre
attribute [-instance] AlgebraicGeometry.OModulePresheaf.instSubsingletonObjZero
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.Modules.tensorPow_zero
  AlgebraicGeometry.Scheme.Modules.tensorPow_succ AlgebraicGeometry.OModulePresheaf.prod_obj
  AlgebraicGeometry.OModulePresheaf.restrOpen_obj
  AlgebraicGeometry.OModulePresheaf.DevissageStep.mk.injEq
  AlgebraicGeometry.OModulePresheaf.pushforward_obj AlgebraicGeometry.OModulePresheaf.im_obj
  AlgebraicGeometry.OModulePresheaf.pow_obj AlgebraicGeometry.OModulePresheaf.fstHom_app
  AlgebraicGeometry.OModulePresheaf.ker_obj AlgebraicGeometry.OModulePresheaf.coker_obj
  AlgebraicGeometry.OModulePresheaf.DevissageStep.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCover.preimage_U
  AlgebraicGeometry.OModulePresheaf.sndHom_app AlgebraicGeometry.OModulePresheaf.Hom.mk.injEq
  AlgebraicGeometry.OModulePresheaf.Hom.id_app
  AlgebraicGeometry.OModulePresheaf.AffHom.appSections_apply
  AlgebraicGeometry.OModulePresheaf.AffHom.comp_app
  AlgebraicGeometry.OModulePresheaf.AffSES.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.AffHom.kerMap_coe
  AlgebraicGeometry.OModulePresheaf.AffHom.id_app
  AlgebraicGeometry.OModulePresheaf.Hom.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.Hom.toAffHom_app
  AlgebraicGeometry.OModulePresheaf.SES.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.AffHom.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.Hom.comp_app AlgebraicGeometry.OModulePresheaf.SES.mk.injEq
  AlgebraicGeometry.OModulePresheaf.AffHom.mk.injEq
  AlgebraicGeometry.OModulePresheaf.Hom.appSections_apply
  AlgebraicGeometry.OModulePresheaf.AffSES.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
  AlgebraicGeometry.Scheme.Modules.tensorSections_zero_right
  AlgebraicGeometry.Scheme.Modules.map_unitSection
  AlgebraicGeometry.Scheme.Modules.tensorSectionsBilin_apply
  AlgebraicGeometry.Scheme.Modules.tensorPowSection_zero
  AlgebraicGeometry.Scheme.Modules.tensorSections_zero_left
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor NeronModelInfra GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace F3Sol
universe u
Lean source · statement
theorem smul_map_eq_of_eq {X : Scheme.{u}} (M : X.Modules) {W W' : X.Opens} (ρ : W' ⟶ W) (e : W =
  W')
    (s t : Γ(M, ⊤)) (g : Γ(X, W))
    (h : g • M.presheaf.map (homOfLE (le_top : W ≤ ⊤)).op s = M.presheaf.map (homOfLE (le_top : W ≤
      ⊤)).op t) :
    (X.presheaf.map ρ.op g) • M.presheaf.map (homOfLE (le_top : W' ≤ ⊤)).op s =
      M.presheaf.map (homOfLE (le_top : W' ≤ ⊤)).op t
theorem

descend

L99 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_forall_geomFibreH0Finrank_tensorPow_eq_hilbertFunctionOf_of_point_geomFibre.F3Sol.descend
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_forall_geomFibreH0Finrank_tensorPow_eq_hilbertFunctionOf_of_point_geomFibre
attribute [-instance] AlgebraicGeometry.OModulePresheaf.instSubsingletonObjZero
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.Modules.tensorPow_zero
  AlgebraicGeometry.Scheme.Modules.tensorPow_succ AlgebraicGeometry.OModulePresheaf.prod_obj
  AlgebraicGeometry.OModulePresheaf.restrOpen_obj
  AlgebraicGeometry.OModulePresheaf.DevissageStep.mk.injEq
  AlgebraicGeometry.OModulePresheaf.pushforward_obj AlgebraicGeometry.OModulePresheaf.im_obj
  AlgebraicGeometry.OModulePresheaf.pow_obj AlgebraicGeometry.OModulePresheaf.fstHom_app
  AlgebraicGeometry.OModulePresheaf.ker_obj AlgebraicGeometry.OModulePresheaf.coker_obj
  AlgebraicGeometry.OModulePresheaf.DevissageStep.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCover.preimage_U
  AlgebraicGeometry.OModulePresheaf.sndHom_app AlgebraicGeometry.OModulePresheaf.Hom.mk.injEq
  AlgebraicGeometry.OModulePresheaf.Hom.id_app
  AlgebraicGeometry.OModulePresheaf.AffHom.appSections_apply
  AlgebraicGeometry.OModulePresheaf.AffHom.comp_app
  AlgebraicGeometry.OModulePresheaf.AffSES.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.AffHom.kerMap_coe
  AlgebraicGeometry.OModulePresheaf.AffHom.id_app
  AlgebraicGeometry.OModulePresheaf.Hom.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.Hom.toAffHom_app
  AlgebraicGeometry.OModulePresheaf.SES.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.AffHom.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.Hom.comp_app AlgebraicGeometry.OModulePresheaf.SES.mk.injEq
  AlgebraicGeometry.OModulePresheaf.AffHom.mk.injEq
  AlgebraicGeometry.OModulePresheaf.Hom.appSections_apply
  AlgebraicGeometry.OModulePresheaf.AffSES.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
  AlgebraicGeometry.Scheme.Modules.tensorSections_zero_right
  AlgebraicGeometry.Scheme.Modules.map_unitSection
  AlgebraicGeometry.Scheme.Modules.tensorSectionsBilin_apply
  AlgebraicGeometry.Scheme.Modules.tensorPowSection_zero
  AlgebraicGeometry.Scheme.Modules.tensorSections_zero_left
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor NeronModelInfra GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace F3Sol
universe u
Lean source · statement
theorem descend {R A : Type u} [CommRing R] [CommRing A] [Algebra R A] {X : Scheme.{u}}
    {f₁ : X ⟶ Spec (.of R)} {M : X.Modules} {N : ℕ} (𝔓 : M.ProjPresentation f₁ N)
    (φ : X ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (N + 1)) A))
    (hφ : 𝔓.toProj = φ ≫ ProjSpace.map R A N) :
    ∃ 𝔓' : M.ProjPresentation (φ ≫ ProjSpace.π A N) N, (∀ i, 𝔓'.σ i = 𝔓.σ i) ∧ 𝔓'.toProj = φ
def

powIso

L164 ↗
AlgebraicCurves.Geometry.Schemes.Proofs.exists_forall_geomFibreH0Finrank_tensorPow_eq_hilbertFunctionOf_of_point_geomFibre.F3Sol.powIso
Documentation

The pullback comparison for iterated tensor powers, transported through the given module isomorphism.

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs
namespace exists_forall_geomFibreH0Finrank_tensorPow_eq_hilbertFunctionOf_of_point_geomFibre
attribute [-instance] AlgebraicGeometry.OModulePresheaf.instSubsingletonObjZero
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.Modules.tensorPow_zero
  AlgebraicGeometry.Scheme.Modules.tensorPow_succ AlgebraicGeometry.OModulePresheaf.prod_obj
  AlgebraicGeometry.OModulePresheaf.restrOpen_obj
  AlgebraicGeometry.OModulePresheaf.DevissageStep.mk.injEq
  AlgebraicGeometry.OModulePresheaf.pushforward_obj AlgebraicGeometry.OModulePresheaf.im_obj
  AlgebraicGeometry.OModulePresheaf.pow_obj AlgebraicGeometry.OModulePresheaf.fstHom_app
  AlgebraicGeometry.OModulePresheaf.ker_obj AlgebraicGeometry.OModulePresheaf.coker_obj
  AlgebraicGeometry.OModulePresheaf.DevissageStep.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCover.preimage_U
  AlgebraicGeometry.OModulePresheaf.sndHom_app AlgebraicGeometry.OModulePresheaf.Hom.mk.injEq
  AlgebraicGeometry.OModulePresheaf.Hom.id_app
  AlgebraicGeometry.OModulePresheaf.AffHom.appSections_apply
  AlgebraicGeometry.OModulePresheaf.AffHom.comp_app
  AlgebraicGeometry.OModulePresheaf.AffSES.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.AffHom.kerMap_coe
  AlgebraicGeometry.OModulePresheaf.AffHom.id_app
  AlgebraicGeometry.OModulePresheaf.Hom.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.Hom.toAffHom_app
  AlgebraicGeometry.OModulePresheaf.SES.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.AffHom.mk.sizeOf_spec
  AlgebraicGeometry.OModulePresheaf.Hom.comp_app AlgebraicGeometry.OModulePresheaf.SES.mk.injEq
  AlgebraicGeometry.OModulePresheaf.AffHom.mk.injEq
  AlgebraicGeometry.OModulePresheaf.Hom.appSections_apply
  AlgebraicGeometry.OModulePresheaf.AffSES.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
  AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
  AlgebraicGeometry.Scheme.Modules.tensorSections_zero_right
  AlgebraicGeometry.Scheme.Modules.map_unitSection
  AlgebraicGeometry.Scheme.Modules.tensorSectionsBilin_apply
  AlgebraicGeometry.Scheme.Modules.tensorPowSection_zero
  AlgebraicGeometry.Scheme.Modules.tensorSections_zero_left
open MvPolynomial CategoryTheory CategoryTheory.Limits AlgebraicGeometry
  AlgebraicGeometry.HilbertFunctor NeronModelInfra GoodReductionJacobian
open _root_.CategoryTheory.MonoidalCategory
attribute [local instance] MvPolynomial.gradedAlgebra
noncomputable section
namespace F3Sol
universe u
Lean source · full declaration
def powIso {X Y : Scheme.{u}} (p : X ⟶ Y) (𝓜 : Y.Modules) (𝓜' : X.Modules)
    (η : (Scheme.Modules.pullback p).obj 𝓜 ≅ 𝓜') :
    ∀ d : ℕ, (Scheme.Modules.pullback p).obj
        (Nat.rec (motive := fun _ => Y.Modules) (𝟙_ Y.Modules) (fun _ M => M ⊗ 𝓜) d) ≅
        Nat.rec (motive := fun _ => X.Modules) (𝟙_ X.Modules) (fun _ M => M ⊗ 𝓜') d
  | 0 => Scheme.Modules.pullbackTensorUnitObjIso p
  | d + 1 => Scheme.Modules.pullbackTensorObjIso p _ 𝓜 ≪≫ (powIso p 𝓜 𝓜' η d ⊗ᵢ η)
theorem

exists_forall_geomFibreH0Finrank_tensorPow_eq_hilbertFunctionOf_of_point_geomFibre

L189 ↗
AlgebraicGeometry.exists_forall_geomFibreH0Finrank_tensorPow_eq_hilbertFunctionOf_of_point_geomFibre
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicGeometry
open MvPolynomial CategoryTheory CategoryTheory.Limits CategoryTheory.MonoidalCategory
open AlgebraicGeometry.HilbertFunctor NeronModelInfra GoodReductionJacobian
attribute [local instance] MvPolynomial.gradedAlgebra
open _root_.AlgebraicCurves.Geometry.Schemes.Proofs in
open exists_forall_geomFibreH0Finrank_tensorPow_eq_hilbertFunctionOf_of_point_geomFibre in
open F3Sol in
Lean source · full declaration
theorem exists_forall_geomFibreH0Finrank_tensorPow_eq_hilbertFunctionOf_of_point_geomFibre
    (S : Type) [CommRing S] {X : Scheme.{0}} (f : X ⟶ Spec (CommRingCat.of S))
    (𝓛X : X.Modules) (hX₁ : Scheme.Modules.IsInvertible 𝓛X)
    {n : ℕ} (𝔓 : Scheme.Modules.ProjPresentation 𝓛X f n)
    (S' : Type) [CommRing S'] (ψ : S →+* S')
    (Z : Scheme.{0}) (ι : Z ⟶ pullback f (Spec.map (CommRingCat.ofHom ψ)))
    (j : pullback f (Spec.map (CommRingCat.ofHom ψ)) ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin
      (n + 1)) S'))
    (hj₂ : (letI : Algebra S S' := ψ.toAlgebra; j ≫ ProjSpace.map S S' n) =
      pullback.fst f (Spec.map (CommRingCat.ofHom ψ)) ≫ 𝔓.toProj)
    (k : Type) [Field k] [IsAlgClosed k] (sk : S' →+* k)
    (P' : Polynomial ℚ) (m' : ℕ) (q : Point k n (hilbertFunctionOf n P' m'))
    (Zk : Scheme.{0}) (ιk : Zk ⟶ Proj (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k)) (hιk :
      IsClosedImmersion ιk)
    (e : Zk ⟶ Z)
    (he₁ : IsPullback e (ιk ≫ ProjSpace.π k n) (ι ≫ pullback.snd f (Spec.map (CommRingCat.ofHom ψ)))
      (Spec.map (CommRingCat.ofHom sk)))
    (he₂ : (letI : Algebra S' k := sk.toAlgebra; ιk ≫ ProjSpace.map S' k n) = e ≫ ι ≫ j)
    (hZk : ∀ d : ℕ, m' ≤ d → ∀ (F : MvPolynomial (Fin (n + 1)) k) (hF : F.IsHomogeneous d),
      (F ∈ q.I ↔ ∀ i : Fin (n + 1),
        (ιk.app (Proj.basicOpen (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k) (MvPolynomial.X
          i)))
          ((Proj.awayToSection (MvPolynomial.homogeneousSubmodule (Fin (n + 1)) k) (MvPolynomial.X
            i))
            (HomogeneousLocalization.mk
              { deg := d
                num := ⟨F, (MvPolynomial.mem_homogeneousSubmodule d F).mpr hF⟩
                den := ⟨MvPolynomial.X i ^ d, (MvPolynomial.mem_homogeneousSubmodule d _).mpr
                  (MvPolynomial.isHomogeneous_X_pow i d)⟩
                den_mem := ⟨d, rfl⟩ })) = 0)) :
    ∃ d₀ : ℕ, ∀ d : ℕ, d₀ ≤ d →
      Scheme.Modules.geomFibreH0Finrank (ι ≫ pullback.snd f (Spec.map (CommRingCat.ofHom ψ)))
        (Nat.rec (motive := fun _ => Z.Modules) (𝟙_ Z.Modules)
          (fun _ M => M ⊗ (Scheme.Modules.pullback (ι ≫ pullback.fst f (Spec.map (CommRingCat.ofHom
            ψ)))).obj 𝓛X) d) k sk =
      hilbertFunctionOf n P' m' d := by
  let instSS' : Algebra S S' := ψ.toAlgebra
  let instS'k : Algebra S' k := sk.toAlgebra
  obtain ⟨𝔓a, -, h𝔓a⟩ :=
    Scheme.Modules.ProjPresentation.exists_projPresentation_pullback_sigma_eq_toProj_eq
      (pullback.fst f (Spec.map (CommRingCat.ofHom ψ))) 𝔓
  obtain ⟨𝔓b, -, h𝔓b⟩ := descend 𝔓a j (by rw [h𝔓a]; exact hj₂.symm)
  obtain ⟨𝔓c, -, h𝔓c⟩ :=
    Scheme.Modules.ProjPresentation.exists_projPresentation_pullback_sigma_eq_toProj_eq
      (e ≫ ι) 𝔓b
  obtain ⟨𝔓d, -, h𝔓d⟩ := descend 𝔓c ιk (by rw [h𝔓c, h𝔓b, Category.assoc]; exact he₂.symm)
  have h𝓛k : Scheme.Modules.IsInvertible
      ((Scheme.Modules.pullback (e ≫ ι)).obj
        ((Scheme.Modules.pullback (pullback.fst f (Spec.map (CommRingCat.ofHom ψ)))).obj 𝓛X)) :=
    (hX₁.pullback _).pullback _
  obtain ⟨d₀, hd₀⟩ :=
    exists_forall_geomFibreH0Finrank_tensorPow_eq_hilbertFunctionOf_of_point
      n P' m' k q Zk ιk hιk hZk _ h𝓛k 𝔓d h𝔓d
  refine ⟨d₀, fun d hd => ?_⟩
  have η : (Scheme.Modules.pullback e).obj
        ((Scheme.Modules.pullback (ι ≫ pullback.fst f (Spec.map (CommRingCat.ofHom ψ)))).obj 𝓛X) ≅
      (Scheme.Modules.pullback (e ≫ ι)).obj
        ((Scheme.Modules.pullback (pullback.fst f (Spec.map (CommRingCat.ofHom ψ)))).obj 𝓛X) :=
    (Scheme.Modules.pullbackComp e (ι ≫ pullback.fst f (Spec.map (CommRingCat.ofHom ψ)))).app 𝓛X ≪≫
      eqToIso (by rw [Category.assoc]) ≪≫
      ((Scheme.Modules.pullbackComp (e ≫ ι) (pullback.fst f (Spec.map (CommRingCat.ofHom ψ)))).app
        𝓛X).symm
  have key := AlgebraicGeometry.Scheme.Modules.geomFibreH0Finrank_eq_of_isPullback sk
    (ι ≫ pullback.snd f (Spec.map (CommRingCat.ofHom ψ))) (ιk ≫ ProjSpace.π k n) e he₁ _ _
    (powIso e _ _ η d) k (RingHom.id k)
  rw [RingHom.id_comp] at key
  rw [← key]
  exact hd₀ d hd

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