JacobianVarieties.Picard.Proofs.FlatFibreUnitClosed.H0UnitAux.finrank_H0_unit_eq_finrank_sections
Source context 20 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FlatFibreUnitClosed
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
AlgebraicGeometry.ChowDatum.hι_closed
AlgebraicGeometry.ChowDatumProj.hιN_closed
AlgebraicGeometry.ChowDatumProj.hp_proper
AlgebraicGeometry.ChowDatum.hp_isoU
AlgebraicGeometry.ChowDatum.hp_proper
AlgebraicGeometry.ProjSpace.algebraAway
AlgebraicGeometry.ProjSpace.instIsProperProdOverπ
AlgebraicGeometry.ChowDatumProj.hp_isoU
AlgebraicGeometry.ProjSpace.isProper_π
AlgebraicGeometry.ProjSpace.finiteType_mvPolynomial
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
attribute [-instance]
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.tilde.functorCompPullbackSpecIso_app
CoherentBaseChange.FibreH0Family.mk.sizeOf_spec
CoherentBaseChange.FibreH0Family.mk.injEq
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
attribute [-simp]
DoubleComplex.SubQuot.mk.sizeOf_spec
DoubleComplex.SubQuot.mk.injEq
AlgebraicGeometry.ChowDatumProj.mk.sizeOf_spec
AlgebraicGeometry.ChowDatum.mk.sizeOf_spec
AlgebraicGeometry.ChowDatumProj.mk.injEq
AlgebraicGeometry.ChowDatum.mk.injEq
ProjSpaceCech.GradedModule.mk.injEq
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
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.CategoryTheory.MonoidalCategory
namespace H0UnitAux
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.Opposite
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
variable {R : Type u} [CommRing R]Lean source · full declaration
theorem finrank_H0_unit_eq_finrank_sections {X : Scheme.{u}} (𝒱 : X.TwoAffineOpenCover)
(x : X ⟶ Spec (.of R)) :
let : Algebra R Γ(X, ⊤) := algebraOfHom x ⊤
Module.finrank R (𝒱.sectionsOf x (SheafOfModules.unit X.ringCatSheaf)).H0 =
Module.finrank R Γ(X, ⊤) := by
intro algTop
let : Module R Γ(SheafOfModules.unit X.ringCatSheaf, ⊤) :=
moduleSectionsOfHom x (SheafOfModules.unit X.ringCatSheaf) ⊤
obtain ⟨e, -⟩ := exists_linearEquiv_sectionsOf_H0 𝒱 x (SheafOfModules.unit X.ringCatSheaf)
let e0 : Γ(SheafOfModules.unit X.ringCatSheaf, ⊤) ≃ₗ[R] Γ(X, ⊤) :=
{ toFun := fun m => (m : Γ(X, ⊤))
invFun := fun a => (a : Γ(SheafOfModules.unit X.ringCatSheaf, ⊤))
map_add' := fun _ _ => rfl
map_smul' := fun _ _ => rfl
left_inv := fun _ => rfl
right_inv := fun _ => rfl }
rw [← e.finrank_eq, e0.finrank_eq]