AlgebraicGeometry.RelPicard.forall_subsingleton_H1_and_finrank_H0_fibreModule_of_iso
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.Forall_subsingleton_H1_and_finrank_H0_fibreModule_of_iso
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry AlgebraicGeometry.RelPicard
NeronModelInfraLean source · statement
theorem _root_.AlgebraicGeometry.RelPicard.forall_subsingleton_H1_and_finrank_H0_fibreModule_of_iso
{R : Type u} [CommRing R] {C T : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
(t : T ⟶ Spec (CommRingCat.of R)) {F F' : (pullback c t).Modules} (e : F ≅ F') (n : ℕ)
(h : ∀ (k : Type u) [Field k] (s : Spec (CommRingCat.of k) ⟶ T)
(𝒲 : (pullback (pullback.snd c t) s).TwoAffineOpenCover),
Subsingleton (𝒲.sectionsOf (fibreAt c t s) (fibreModule c t s F)).H1 ∧
Module.finrank k (𝒲.sectionsOf (fibreAt c t s) (fibreModule c t s F)).H0 = n) :
∀ (k : Type u) [Field k] (s : Spec (CommRingCat.of k) ⟶ T)
(𝒲 : (pullback (pullback.snd c t) s).TwoAffineOpenCover),
Subsingleton (𝒲.sectionsOf (fibreAt c t s) (fibreModule c t s F')).H1 ∧
Module.finrank k (𝒲.sectionsOf (fibreAt c t s) (fibreModule c t s F')).H0 = n