AlgebraicGeometry.Scheme.Modules.IsInvertible.finite_sections_of_isProper
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Cohomology.Proofs
namespace S_AlgebraicGeometry_Scheme_Modules_IsInvertible_finite_sections_of_isProper
attribute [-instance] AlgebraicGeometry.OModulePresheaf.instSubsingletonObjZero
AlgebraicGeometry.OModulePresheaf.Leray.relAltC_scalarTower
AlgebraicGeometry.OModulePresheaf.Leray.ker_relAltd_modΓ
AlgebraicGeometry.OModulePresheaf.Leray.relAltC_modΓ
AlgebraicGeometry.OModulePresheaf.Leray.biC_abGrp
AlgebraicGeometry.OModulePresheaf.Leray.relAltH_modΓ
AlgebraicGeometry.OModulePresheaf.Leray.ker_relAltd_smul
AlgebraicGeometry.OModulePresheaf.Leray.relAltH_scalarTower
AlgebraicGeometry.OModulePresheaf.Leray.relAltH_smul
AlgebraicGeometry.OModulePresheaf.Leray.biC_module
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx DoubleComplex.instModuleE₂I
DoubleComplex.Bounded.modR DoubleComplex.instModuleE₂II DoubleComplex.instAddCommGroupE₂II
DoubleComplex.Bounded.abGrp DoubleComplex.instAddCommGroupE₂I ProjSpaceCech.GradedModule.H.module
ProjSpaceCech.GradedModule.H.addCommGroup ProjSpaceCech.GradedModule.sec.instAdd
ProjSpaceCech.GradedModule.sec.instNeg ProjSpaceCech.GradedModule.acg
ProjSpaceCech.GradedModule.Frac.setoid ProjSpaceCech.GradedModule.modR
ProjSpaceCech.GradedModule.sec.instModule ProjSpaceCech.GradedModule.sec.instAddCommGroup
ProjSpaceCech.GradedModule.sec.instZero ProjSpaceCech.GradedModule.Presentation.fJ
ProjSpaceCech.GradedModule.sec.instSMul ProjSpaceCech.Twist.H.module
ProjSpaceCech.Idx.instFintype ProjSpaceCech.Twist.H.addCommGroup
ProjSpaceCech.Idx.instDecidableEq ProjSpaceCech.Twist.Mon.instDecidableEq
ProjSpaceCech.Twist.cochain.instAddCommGroup ProjSpaceCech.Twist.cochain.instModule
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.OModulePresheaf.Leray.restrictToPreimage_U
AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U DoubleComplex.Bounded.mk.injEq
DoubleComplex.Bounded.mk.sizeOf_spec DoubleComplex.Convergence.mk.injEq
DoubleComplex.Convergence.mk.sizeOf_spec DoubleComplex.SubQuot.mk.sizeOf_spec
DoubleComplex.SubQuot.mk.injEq ProjSpaceCech.GradedModule.mk.injEq
attribute [-simp] ProjSpaceCech.GradedModule.mk.sizeOf_spec
ProjSpaceCech.GradedModule.Frac.mk.sizeOf_spec ProjSpaceCech.GradedModule.Presentation.mk.injEq
ProjSpaceCech.GradedModule.Frac.mk.injEq ProjSpaceCech.GradedModule.Presentation.mk.sizeOf_spec
ProjSpaceCech.GradedModule.Hom.shift_toLinearMap ProjSpaceCech.GradedModule.Hom.mk.sizeOf_spec
ProjSpaceCech.GradedModule.Hom.mk.injEq
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry
universe uLean source · full declaration
theorem _root_.AlgebraicGeometry.Scheme.Modules.IsInvertible.finite_sections_of_isProper
(k : Type u) [Field k] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of k)) [IsProper f]
(𝓝 : X.Modules) (h𝓝 : Scheme.Modules.IsInvertible 𝓝) :
letI : Algebra k Γ(X, ⊤) := ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appLE ⊤ ⊤ le_top).hom.toAlgebra
letI : Module k Γ(𝓝, ⊤) := Module.compHom _ (algebraMap k Γ(X, ⊤))
Module.Finite k Γ(𝓝, ⊤) := by
let instA : Algebra k Γ(X, ⊤) := ((Scheme.ΓSpecIso (.of k)).inv ≫ f.appLE ⊤ ⊤
le_top).hom.toAlgebra
let instM : Module k Γ(𝓝, ⊤) := Module.compHom _ (algebraMap k Γ(X, ⊤))
change Module.Finite k Γ(𝓝, ⊤)
have : CompactSpace ↥X := QuasiCompact.compactSpace_of_compactSpace f
obtain ⟨𝒦⟩ := AlgebraicGeometry.Scheme.OrderedAffineCover.nonempty_of_compactSpace X
have hfin := AlgebraicGeometry.OModulePresheaf.cechFinite_ofModules_of_locallyTrivial f 𝓝
h𝓝.exists_trivialization 𝒦
obtain ⟨e⟩ := AlgebraicGeometry.OModulePresheaf.nonempty_sections_top_equiv_H0_ofModules f 𝓝 𝒦
have : Module.Finite k ↥((OModulePresheaf.ofModules f 𝓝).H0 𝒦) := hfin.1
exact Module.Finite.equiv e.symm