AlgebraicGeometry.RelPicard.isInvertible_and_nonempty_pullback_iso_foldr_sectionTwist_tensor_of_range_subset
Source context 12 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Picard.Proofs.FoldedTwistPullback
attribute [-instance]
AlgebraicGeometry.RelEffCartierDiv.isIso_subschemeIota_snd_of_degree_one
AlgebraicGeometry.isIso_ker_graphOver_subschemeIota_snd
AlgebraicGeometry.isClosedImmersion_graphOver
attribute [-simp]
AlgebraicGeometry.graphOver_fst_assoc
AlgebraicGeometry.RelEffCartierDiv.toPoint_comp
AlgebraicGeometry.RelEffCartierDiv.toPoint_comp_assoc
AlgebraicGeometry.graphOver_fst
AlgebraicGeometry.RelEffCartierDiv.ofPoint_I
AlgebraicGeometry.graphOver_snd
AlgebraicGeometry.graphOver_snd_assoc
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.CategoryTheory.MonoidalCategory
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
with_weak_namespace _root_.AlgebraicGeometry.RelPicardLean source · full declaration
theorem isInvertible_and_nonempty_pullback_iso_foldr_sectionTwist_tensor_of_range_subset
{R : Type u} [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) [IsSeparated c]
(U : C.Opens) [SmoothOfRelativeDimension 1 (U.ι ≫ c)]
{m : ℕ} (σ : Fin m → SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
(hσ : ∀ j, Set.range (σ j).1 ⊆ (U : Set C)) (pos neg : Fin m → ℕ)
{T T' : Scheme.{u}} {t : T ⟶ Spec (CommRingCat.of R)} {t' : T' ⟶ Spec (CommRingCat.of R)}
(ψ : SchemeHomOver t' t) :
Scheme.Modules.IsInvertible
((List.finRange m).foldr
(fun j M =>
(sectionTwist c (σ j) t (pos j) ⊗ ((sectionIdeal c (σ j) t) ^ (neg j)).module) ⊗ M)
(𝟙_ (pullback c t).Modules)) ∧
Nonempty ((Scheme.Modules.pullback (baseChangeSnd c ψ)).obj
((List.finRange m).foldr
(fun j M =>
(sectionTwist c (σ j) t (pos j) ⊗ ((sectionIdeal c (σ j) t) ^ (neg j)).module) ⊗ M)
(𝟙_ (pullback c t).Modules)) ≅
(List.finRange m).foldr
(fun j M =>
(sectionTwist c (σ j) t' (pos j) ⊗ ((sectionIdeal c (σ j) t') ^ (neg j)).module) ⊗ M)
(𝟙_ (pullback c t').Modules)) := by
have hI : ∀ {T₀ : Scheme.{u}} (t₀ : T₀ ⟶ Spec (CommRingCat.of R)) (j : Fin m),
(sectionIdeal c (σ j) t₀).IsInvertible :=
fun t₀ j => isInvertible_sectionIdeal_of_range_subset c (σ j) U (hσ j) t₀
have hN : ∀ {T₀ : Scheme.{u}} (t₀ : T₀ ⟶ Spec (CommRingCat.of R)) (j : Fin m),
Scheme.Modules.IsInvertible
(sectionTwist c (σ j) t₀ (pos j) ⊗ ((sectionIdeal c (σ j) t₀) ^ (neg j)).module) :=
fun t₀ j => Scheme.Modules.IsInvertible.tensor
(Scheme.IdealSheafData.IsInvertible.isInvertible_invModule ((hI t₀ j).pow (pos j)))
(Scheme.IdealSheafData.IsInvertible.isInvertible_module ((hI t₀ j).pow (neg j)))
have eN : ∀ j : Fin m, Nonempty ((Scheme.Modules.pullback (baseChangeSnd c ψ)).obj
(sectionTwist c (σ j) t (pos j) ⊗ ((sectionIdeal c (σ j) t) ^ (neg j)).module) ≅
sectionTwist c (σ j) t' (pos j) ⊗ ((sectionIdeal c (σ j) t') ^ (neg j)).module) := fun j =>
⟨Scheme.Modules.pullbackTensorObjIso (baseChangeSnd c ψ) _ _ ≪≫
tensorIso (nonempty_pullback_sectionTwist_iso_of_range_subset
R c (σ j) U (hσ j) ψ (pos j)).some
(nonempty_pullback_sectionIdeal_pow_module_iso_of_smoothLocus
R c U (σ j) (hσ j) ψ (neg j)).some⟩
have key : ∀ l : List (Fin m),
Scheme.Modules.IsInvertible
(l.foldr (fun j M =>
(sectionTwist c (σ j) t (pos j) ⊗ ((sectionIdeal c (σ j) t) ^ (neg j)).module) ⊗ M)
(𝟙_ (pullback c t).Modules)) ∧
Nonempty ((Scheme.Modules.pullback (baseChangeSnd c ψ)).obj
(l.foldr (fun j M =>
(sectionTwist c (σ j) t (pos j) ⊗ ((sectionIdeal c (σ j) t) ^ (neg j)).module) ⊗ M)
(𝟙_ (pullback c t).Modules)) ≅
l.foldr (fun j M =>
(sectionTwist c (σ j) t' (pos j) ⊗ ((sectionIdeal c (σ j) t') ^ (neg j)).module) ⊗ M)
(𝟙_ (pullback c t').Modules)) := by
intro l
induction l with
| nil =>
exact ⟨Scheme.Modules.isInvertible_unit _,
⟨Scheme.Modules.pullbackTensorUnitObjIso (baseChangeSnd c ψ)⟩⟩
| cons j l ih =>
simp only [List.foldr_cons]
exact ⟨(hN t j).tensor ih.1,
⟨Scheme.Modules.pullbackTensorObjIso (baseChangeSnd c ψ) _ _ ≪≫
tensorIso (eN j).some ih.2.some⟩⟩
exact key (List.finRange m)