AlgebraicGeometry.RelPicard.subsingleton_H1_fibre_of_subsingleton_H1_residueField_chart
Source context 13 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs
namespace Subsingleton_H1_fibre_of_subsingleton_H1_residueField_chart
attribute [-instance] AlgebraicGeometry.OModulePresheaf.isScalarTower
AlgebraicGeometry.Scheme.OrderedAffineCover.instLinearOrder
AlgebraicGeometry.OModulePresheaf.module
AlgebraicGeometry.Scheme.OrderedAffineCover.instFintype
AlgebraicGeometry.Scheme.OrderedAffineCover.instFintypeIdx
AlgebraicGeometry.OModulePresheaf.addCommGroup
AlgebraicGeometry.Scheme.OrderedAffineCover.instDecidableEqIdx
AlgebraicGeometry.OModulePresheaf.moduleSections
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instDecidableEqIdx
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintype
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instLinearOrder
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.instFintypeIdx
attribute [-simp] AlgebraicGeometry.Scheme.OrderedAffineCover.mk.injEq
AlgebraicGeometry.OModulePresheaf.mk.sizeOf_spec
AlgebraicGeometry.Scheme.OrderedAffineCover.mk.sizeOf_spec
AlgebraicGeometry.OModulePresheaf.mk.injEq
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
AlgebraicGeometry.Scheme.Modules.tensorPow_zero
AlgebraicGeometry.Scheme.Modules.tensorPow_succ
AlgebraicGeometry.Scheme.OrderedAffineCover.toCoverOf_U
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.sizeOf_spec
AlgebraicGeometry.Scheme.OrderedAffineCoverOf.mk.injEq
AlgebraicGeometry.Scheme.OrderedAffineCover.restrict_U
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.tilde.functorCompPullbackSpecIso_app
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.AlgebraicGeometry.SmoothProperCurveLean source · statement
theorem
_root_.AlgebraicGeometry.RelPicard.subsingleton_H1_fibre_of_subsingleton_H1_residueField_chart
{R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) [IsSeparated c]
{T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (M : (pullback c t).Modules) (hM :
Scheme.Modules.IsInvertible M)
{A : Type u} [CommRing A] (j : Spec (CommRingCat.of A) ⟶ T) [IsOpenImmersion j]
{CA : Scheme.{u}} (πA : CA ⟶ Spec (CommRingCat.of A)) (g' : CA ⟶ pullback c t)
(hcart : IsPullback g' πA (pullback.snd c t) j)
(𝒱 : CA.TwoAffineOpenCover) (𝔭 : PrimeSpectrum A)
(hO : Subsingleton ((𝒱.pullback πA 𝔭.asIdeal.ResidueField).sectionsOf
(pullback.snd πA (Scheme.TwoAffineOpenCover.specMap A 𝔭.asIdeal.ResidueField))
((Scheme.Modules.pullback (pullback.fst πA (Scheme.TwoAffineOpenCover.specMap A
𝔭.asIdeal.ResidueField))).obj
((Scheme.Modules.pullback g').obj M))).H1)
{k : Type u} [Field k] (s : Spec (CommRingCat.of k) ⟶ T)
(hs : s.base (IsLocalRing.closedPoint k) = j.base 𝔭)
(𝒲 : (pullback (pullback.snd c t) s).TwoAffineOpenCover) :
Subsingleton (𝒲.sectionsOf (fibreAt c t s) (fibreModule c t s M)).H1