Module

IsIso_baseChangeHom_pushforward_of_forall_fibre.lean

Nyll.AlgebraicCurves.Cohomology.Sheaves.IsIso_baseChangeHom_pushforward_of_forall_fibre

3 declarations indexed from sourceView source ↗

Module documentation

Is Iso base Change Hom pushforward of forall fibre

Imports17

Imported by3

theorem

isPullback_baseChangeSnd

L56 ↗

JacobianVarieties.Picard.Proofs.IsIso_baseChangeHom_pushforward_of_forall_fibre.PFBCSketch.isPullback_baseChangeSnd

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.IsIso_baseChangeHom_pushforward_of_forall_fibre
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
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.SmoothProperCurve
namespace PFBCSketch
variable {R : Type u} [CommRing R]

Lean source · statement

theorem isPullback_baseChangeSnd {C T T' : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R))
    {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)} (ψ : SchemeHomOver t' t) :
    IsPullback (baseChangeSnd c ψ) (pullback.snd c t') (pullback.snd c t) ψ.1

theorem

fromSpec_comp_eq_specMap

L64 ↗

JacobianVarieties.Picard.Proofs.IsIso_baseChangeHom_pushforward_of_forall_fibre.PFBCSketch.fromSpec_comp_eq_specMap

Source context 13 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.IsIso_baseChangeHom_pushforward_of_forall_fibre
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
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.SmoothProperCurve
namespace PFBCSketch
variable {R : Type u} [CommRing R]

Lean source · full declaration

theorem fromSpec_comp_eq_specMap {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (W : T.Opens)
    (hW : IsAffineOpen W) :
    letI := Scheme.TwoAffineOpenCover.algebraOfHom t W
    hW.fromSpec ≫ t = Scheme.TwoAffineOpenCover.specMap R Γ(T, W) := by
  let := Scheme.TwoAffineOpenCover.algebraOfHom t W
  have h := IsAffineOpen.SpecMap_appLE_fromSpec t (isAffineOpen_top _) hW (le_top (a := W))
  rw [IsAffineOpen.fromSpec_top, Scheme.isoSpec_Spec_inv, ← Spec.map_comp] at h
  change _ = Spec.map (CommRingCat.ofHom ((Scheme.ΓSpecIso (.of R)).inv ≫ t.appLE ⊤ W le_top).hom)
  rw [CommRingCat.ofHom_hom]
  exact h.symm

theorem

isIso_baseChangeHom_pushforward_of_forall_fibre

L78 ↗

AlgebraicGeometry.RelPicard.isIso_baseChangeHom_pushforward_of_forall_fibre

Source context 12 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.IsIso_baseChangeHom_pushforward_of_forall_fibre
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
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.SmoothProperCurve
open PFBCSketch in

Lean source · statement

theorem _root_.AlgebraicGeometry.RelPicard.isIso_baseChangeHom_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 T' : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)}
      [LocallyOfFiniteType t]
    (ψ : SchemeHomOver t' 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) :
    IsIso (Scheme.Modules.baseChangeHom
      (RelPicard.BaseChange.baseChangeSnd_snd' (cc := c) (ψ := ψ)) F)

Module documentation

Is Iso base Change Hom pushforward of forall fibre

Declarations

isPullback_baseChangeSnd

fromSpec_comp_eq_specMap

isIso_baseChangeHom_pushforward_of_forall_fibre