AlgebraicGeometry.RelPicard.subsingleton_H1_fibre_of_subsingleton_H1_fibre_extension
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicGeometry.RelPicard
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfraLean source · statement
theorem subsingleton_H1_fibre_of_subsingleton_H1_fibre_extension
{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)
{k : Type u} [Field k] (s : Spec (CommRingCat.of k) ⟶ T)
(K : Type u) [Field K] [Algebra k K]
(hK : ∀ 𝒲' :
(pullback (pullback.snd c t) (Scheme.TwoAffineOpenCover.specMap k K ≫ s)).TwoAffineOpenCover,
Subsingleton (𝒲'.sectionsOf (fibreAt c t (Scheme.TwoAffineOpenCover.specMap k K ≫ s))
(fibreModule c t (Scheme.TwoAffineOpenCover.specMap k K ≫ s) M)).H1) :
∀ 𝒲 : (pullback (pullback.snd c t) s).TwoAffineOpenCover,
Subsingleton (𝒲.sectionsOf (fibreAt c t s) (fibreModule c t s M)).H1