AlgebraicGeometry.RelPicard.isLocallyFreeOfRank_pushforward_of_forall_fibre
Source context 12 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.IsLocallyFreeOfRank_pushforward_of_forall_fibre
attribute [-instance] AlgebraicGeometry.SmoothOfRelativeDimension.fiberToSpecResidueField
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_snd
AlgebraicGeometry.SmoothOfRelativeDimension.pullback_fst
AlgebraicGeometry.SmoothOfRelativeDimension.smooth_one
AlgebraicGeometry.SmoothProperCurve.isIntegral_pullback_Spec_field
AlgebraicGeometry.IsProper.fiberToSpecResidueField
attribute [-simp] AlgebraicGeometry.tilde.functorCompPullbackSpecIso_app
TwoChartCech.Mumford.dK_apply TwoChartCech.Mumford.ι0_apply TwoChartCech.Mumford.ι1_apply
TwoChartCech.KerCoprod.dK_apply TwoChartCech.KerCoprod.ι1_apply
TwoChartCech.KerCoprod.ι0_apply AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_snd
AlgebraicGeometry.SmoothProperCurve.sectionBaseChange_coe_fst
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry.SmoothProperCurveLean source · statement
theorem _root_.AlgebraicGeometry.RelPicard.isLocallyFreeOfRank_pushforward_of_forall_fibre
(R : Type u) [CommRing R] [IsNoetherianRing R] {C : Scheme.{u}} (c : C ⟶ Spec
(CommRingCat.of R))
[IsProper c] [SmoothOfRelativeDimension 1 c]
(ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
(h𝔉 : ∀ m₀ : ℕ, ∃ 𝔉 : SmoothProperCurve.FiniteMapData c ε, m₀ ≤ 𝔉.m)
{T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) [LocallyOfFiniteType t]
(F : (pullback c t).Modules) (hF : Scheme.Modules.IsInvertible F) (n : ℕ)
(hfib : ∀ (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) :
Scheme.Modules.IsLocallyFreeOfRank n ((Scheme.Modules.pushforward
(pullback.snd c t)).obj F)