NYLL
Module

Scheme_Modules_geomFibreH0Finrank_id_eq_finrank_sections.lean

Nyll.AlgebraicCurves.Geometry.Sheaves.Scheme_Modules_geomFibreH0Finrank_id_eq_finrank_sections
2 declarations indexed from sourceView source ↗

Module documentation

Scheme Modules geom Fibre H0 Finrank id eq finrank sections

Imports8
Imported by2

Declarations

theorem

nonempty_orderedAffineCover

L74 ↗
AlgebraicCurves.Geometry.Sheaves.Proofs.Scheme_Modules_geomFibreH0Finrank_id_eq_finrank_sections.L4B5.nonempty_orderedAffineCover
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_geomFibreH0Finrank_id_eq_finrank_sections
attribute [-instance] AlgebraicGeometry.OModulePresheaf.instSubsingletonObjZero
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] 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
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
namespace L4B5
Lean source · statement
theorem nonempty_orderedAffineCover (X : Scheme.{u}) [CompactSpace X] : Nonempty
  X.OrderedAffineCover
theorem

geomFibreH0Finrank_id_eq_finrank_sections

L86 ↗
AlgebraicGeometry.Scheme.Modules.geomFibreH0Finrank_id_eq_finrank_sections
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Sheaves.Proofs
namespace Scheme_Modules_geomFibreH0Finrank_id_eq_finrank_sections
attribute [-instance] AlgebraicGeometry.OModulePresheaf.instSubsingletonObjZero
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
  AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] 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
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
open L4B5 _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover in
Lean source · full declaration
theorem _root_.AlgebraicGeometry.Scheme.Modules.geomFibreH0Finrank_id_eq_finrank_sections
    (k : Type u) [Field k] {A : Scheme.{u}} (f : A ⟶ Spec (CommRingCat.of k)) [IsProper f]
    (M : A.Modules) (hM : Scheme.Modules.IsInvertible M) :
    Scheme.Modules.geomFibreH0Finrank f M k (RingHom.id k) =
      (letI := Scheme.TwoAffineOpenCover.moduleSectionsOfHom f M ⊤; Module.finrank k Γ(M, ⊤)) := by
  have hι : Spec.map (CommRingCat.ofHom (RingHom.id k)) = 𝟙 (Spec (CommRingCat.of k)) := by
    rw [CommRingCat.ofHom_id]; exact Spec.map_id _
  have : IsIso (Spec.map (CommRingCat.ofHom (RingHom.id k))) := by rw [hι]; infer_instance
  have : IsIso (pullback.fst f (Spec.map (CommRingCat.ofHom (RingHom.id k)))) := inferInstance
  have hpf : pullback.fst f (Spec.map (CommRingCat.ofHom (RingHom.id k))) ≫ f =
      pullback.snd f (Spec.map (CommRingCat.ofHom (RingHom.id k))) := by
    rw [pullback.condition, hι, Category.comp_id]
  have : CompactSpace ↑A := QuasiCompact.compactSpace_of_compactSpace f
  have : CompactSpace ↑(pullback f (Spec.map (CommRingCat.ofHom (RingHom.id k)))) :=
    QuasiCompact.compactSpace_of_compactSpace (pullback.snd f (Spec.map (CommRingCat.ofHom
      (RingHom.id k))))
  obtain ⟨𝒰⟩ := nonempty_orderedAffineCover A
  obtain ⟨𝒰₀⟩ := nonempty_orderedAffineCover (pullback f (Spec.map (CommRingCat.ofHom (RingHom.id
    k))))
  change (letI := (moduleSectionsOfHom (pullback.snd f (Spec.map (CommRingCat.ofHom (RingHom.id
    k))))
      ((Scheme.Modules.pullback (pullback.fst f (Spec.map (CommRingCat.ofHom (RingHom.id k))))).obj
        M) ⊤);
    Module.finrank k Γ((Scheme.Modules.pullback (pullback.fst f (Spec.map (CommRingCat.ofHom
      (RingHom.id k))))).obj M, ⊤)) = _
  let i0 := moduleSectionsOfHom (pullback.snd f (Spec.map (CommRingCat.ofHom (RingHom.id k))))
      ((Scheme.Modules.pullback (pullback.fst f (Spec.map (CommRingCat.ofHom (RingHom.id k))))).obj
        M) ⊤
  let i1 := moduleSectionsOfHom f M ⊤
  obtain ⟨e₀⟩ := OModulePresheaf.nonempty_sections_top_equiv_H0_ofModules
    (pullback.snd f (Spec.map (CommRingCat.ofHom (RingHom.id k))))
    ((Scheme.Modules.pullback (pullback.fst f (Spec.map (CommRingCat.ofHom (RingHom.id k))))).obj
      M) 𝒰₀
  obtain ⟨e₁⟩ := OModulePresheaf.nonempty_sections_top_equiv_H0_ofModules f M 𝒰
  have h := OModulePresheaf.cechFinrank_ofModules_pullback_eq_of_isIso f
    (pullback.fst f (Spec.map (CommRingCat.ofHom (RingHom.id k)))) M hM 𝒰₀ 𝒰 0
  rw [hpf, OModulePresheaf.cechFinrank_zero, OModulePresheaf.cechFinrank_zero] at h
  exact e₀.finrank_eq.trans (h.trans e₁.finrank_eq.symm)

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