NYLL
Module

Scheme_Modules_exists_away_finiteBySections_tensorPow_of_forall_geometricFibre.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_exists_away_finiteBySections_tensorPow_of_forall_geometricFibre
3 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules exists away finite By Sections tensor Pow of forall geometric Fibre

Imports22
Imported by2

Declarations

abbrev

ι

L78 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_away_finiteBySections_tensorPow_of_forall_geometricFibre.W2LOC.ι
Documentation

The morphism on spectra induced by the structure homomorphism of an algebra.

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_away_finiteBySections_tensorPow_of_forall_geometricFibre
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
  instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
  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
  TwoChartCech.Mumford.dK_apply TwoChartCech.Mumford.ι0_apply TwoChartCech.Mumford.ι1_apply
  TwoChartCech.KerCoprod.dK_apply TwoChartCech.KerCoprod.ι1_apply TwoChartCech.KerCoprod.ι0_apply
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
section W2LOC_assembly
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · statement
abbrev W2LOC.ι (R A : Type u) [CommRing R] [CommRing A] [Algebra R A] :
    Spec (.of A) ⟶ Spec (.of R)
theorem

exists_iso_forall_unit_eq

L82 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_exists_away_finiteBySections_tensorPow_of_forall_geometricFibre.W2LOC.exists_iso_forall_unit_eq
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_exists_away_finiteBySections_tensorPow_of_forall_geometricFibre
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
  instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
  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
  TwoChartCech.Mumford.dK_apply TwoChartCech.Mumford.ι0_apply TwoChartCech.Mumford.ι1_apply
  TwoChartCech.KerCoprod.dK_apply TwoChartCech.KerCoprod.ι1_apply TwoChartCech.KerCoprod.ι0_apply
  AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
section W2LOC_assembly
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.CategoryTheory.MonoidalCategory
attribute [local instance] MvPolynomial.gradedAlgebra
Lean source · full declaration
theorem W2LOC.exists_iso_forall_unit_eq {X Y Z : Scheme.{u}} (g : Z ⟶ Y) (f : Y ⟶ X) (h : Z ⟶ X)
    (hh : g ≫ f = h) (M : X.Modules) :
    ∃ e : (Scheme.Modules.pullback h).obj M ≅ (Scheme.Modules.pullback g).obj
      ((Scheme.Modules.pullback f).obj M),
      ∀ s : Γ(M, ⊤),
        (e.hom.app ⊤) ((((Scheme.Modules.pullbackPushforwardAdjunction h).unit.app M).app ⊤) s) =
          (show Γ((Scheme.Modules.pullback g).obj ((Scheme.Modules.pullback f).obj M), ⊤) from
            (((Scheme.Modules.pullbackPushforwardAdjunction g).unit.app ((Scheme.Modules.pullback
              f).obj M)).app ⊤)
              (show Γ((Scheme.Modules.pullback f).obj M, ⊤) from
                (((Scheme.Modules.pullbackPushforwardAdjunction f).unit.app M).app ⊤) s)) := by
  subst hh
  refine ⟨((Scheme.Modules.pullbackComp g f).app M).symm, fun s => ?_⟩
  exact CategoryTheory.ConcreteCategory.congr_hom (Scheme.Modules.unit_app_comp_pullbackComp_inv g
    f M ⊤) s
theorem

exists_away_finiteBySections_tensorPow_of_forall_geometricFibre

L111 ↗
AlgebraicGeometry.Scheme.Modules.exists_away_finiteBySections_tensorPow_of_forall_geometricFibre
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicGeometry.Scheme.Modules
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry CategoryTheory.MonoidalCategory
attribute [local instance] MvPolynomial.gradedAlgebra
open _root_.AlgebraicCurves.Geometry.Sheaves.Proofs in
open Scheme_Modules_exists_away_finiteBySections_tensorPow_of_forall_geometricFibre in
open W2LOC in
Lean source · statement
theorem exists_away_finiteBySections_tensorPow_of_forall_geometricFibre
    (R : Type u) [CommRing R] [IsNoetherianRing R] {X : Scheme.{u}} (f : X ⟶ Spec (.of R))
    [IsProper f] [Flat f] (L : X.Modules) (hL : Scheme.Modules.IsInvertible L)
    (hfin : ∀ (𝒰 : X.OrderedAffineCover) (n : ℕ), (OModulePresheaf.ofModules f (L.tensorPow
      n)).CechFinite 𝒰)
    (hfib : ∀ (K : Type u) [Field K] [IsAlgClosed K] [Algebra R K], ∃ n : ℕ,
      Scheme.Modules.FiniteBySections
          ((Scheme.Modules.pullback
              (Limits.pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap R K))))).obj
                (L.tensorPow n))
          (Limits.pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap R K)))) ∧
      ∀ 𝒲 : (Limits.pullback f (Spec.map (CommRingCat.ofHom (algebraMap R K)))).OrderedAffineCover,
        Subsingleton
          ((OModulePresheaf.ofModules (Limits.pullback.snd f (Spec.map (CommRingCat.ofHom
            (algebraMap R K))))
              ((Scheme.Modules.pullback
                  (Limits.pullback.fst f (Spec.map (CommRingCat.ofHom (algebraMap R K))))).obj
                (L.tensorPow n))).HSucc 𝒲 0))
    (𝔭 : PrimeSpectrum R) :
    ∃ g : R, g ∉ 𝔭.asIdeal ∧ ∃ n : ℕ, 0 < n ∧ Scheme.Modules.FiniteBySections
        ((Scheme.Modules.pullback (Limits.pullback.fst f
            (Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away g)))))).obj (L.tensorPow
              n))
        (Limits.pullback.snd f (Spec.map (CommRingCat.ofHom (algebraMap R (Localization.Away g)))))

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