Source context 16 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_polarisation_pair_of_block
attribute [-instance]
pullback_monoidal
isIso_δ
PresheafOfModules.pushforward_laxMonoidal
isIso_η
PresheafOfModules.free_monoidal
PresheafOfModules.restrictScalars_laxMonoidal
isIso_δ_gS
PresheafOfModules.pullback_oplaxMonoidal
instPreservesColimitsOfSizeCompOppositeCommRingCatRingCatForget₂RingHomCarrierCarrierPb
PresheafOfModules.pullback_monoidal'
AlgebraicGeometry.Scheme.Modules.preservesBinaryProducts_opensMap
AlgebraicGeometry.Scheme.Modules.pullback_monoidal
AlgebraicGeometry.Scheme.Modules.sheafify_isLocalization'
AlgebraicGeometry.Scheme.Modules.preservesTerminal_opensMap
AlgebraicGeometry.Scheme.Modules.pullback₀_monoidal
AlgebraicGeometry.Scheme.Modules.preservesFiniteProducts_opensMap
AlgebraicGeometry.Scheme.Modules.sheafifyPullback_lifting
attribute [-simp] PresheafOfModules.freeεIso_hom_app PresheafOfModules.freeμIso_hom_app
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 _root_.TensorProduct
attribute [local simp] AlgebraicGeometry.RelPicard.N12.castDeg_I
attribute [local instance] AlgebraicGeometry.RelPicard.N12.isClosedImmersion_rigSection
open AlgebraicGeometry.RelPicard.N12 in
Lean source · full declarationtheorem _root_.AlgebraicGeometry.RelEffCartierDiv.exists_polarisation_pair_of_block
(R : Type u) [CommRing R] {C : Scheme.{u}} (c : C ⟶ Spec (CommRingCat.of R)) [IsSeparated c]
(U : C.Opens) [SmoothOfRelativeDimension 1 (U.ι ≫ c)]
(ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c) (hεU : Set.range ε.1.base ⊆ (U : Set C))
(A : Type u) [CommRing A] [Algebra R A] [Module.Finite R A] [Module.FaithfullyFlat R A]
(B₀ : Type u) [CommRing B₀] [Algebra R B₀] [Module.Finite R B₀] [Algebra.Etale R B₀]
(d : ℕ) (φ₀ : TensorProduct R A B₀ ≃ₐ[A] (Fin d → A))
(z₀ : Spec (CommRingCat.of B₀) ⟶ C) [IsClosedImmersion z₀]
(hz₀ : z₀ ≫ c = Spec.map (CommRingCat.ofHom (algebraMap R B₀)))
(hz₀U : Set.range z₀.base ⊆ (U : Set C))
(r r' ρ : ℕ) (hρ : ρ = r + r' * d) :
∃ (zA : Spec (CommRingCat.of (TensorProduct R A B₀)) ⟶ pullback (baseChange R c A) (𝟙 (Spec
(CommRingCat.of A))))
(_ : IsClosedImmersion zA)
(_ : zA ≫ pullback.fst (baseChange R c A) (𝟙 (Spec (CommRingCat.of A))) ≫ pullback.fst c
(specMap R A) =
Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.includeRight (R := R) (A := A) (B :=
B₀)).toRingHom) ≫ z₀)
(_ : zA ≫ pullback.snd (baseChange R c A) (𝟙 (Spec (CommRingCat.of A))) =
Spec.map (CommRingCat.ofHom (algebraMap A (TensorProduct R A B₀))))
(E : RelEffCartierDiv c ρ (𝟙 (Spec (CommRingCat.of R))))
(E' : RelEffCartierDiv (baseChange R c A) ρ (𝟙 (Spec (CommRingCat.of A)))),
E.SupportedIn U ∧ E'.SupportedIn (pullback.fst c (specMap R A) ⁻¹ᵁ U) ∧
E.I = (sectionIdeal c ε (𝟙 (Spec (CommRingCat.of R)))) ^ r *
((pullback.lift z₀ (Spec.map (CommRingCat.ofHom (algebraMap R B₀)))
(by rw [Category.comp_id]; exact hz₀)).ker) ^ r' ∧
E'.I = (sectionIdeal (baseChange R c A) (sectionBaseChange A ε) (𝟙 (Spec (CommRingCat.of
A)))) ^ r * zA.ker ^ r' ∧
(∀ ⦃T : Scheme.{u}⦄ (t : T ⟶ Spec (CommRingCat.of A)), ((E'.pullbackAlong t (Category.comp_id
t)).I).IsInvertible) ∧
(∀ ⦃T T' : Scheme.{u}⦄ {t : T ⟶ Spec (CommRingCat.of A)} {t' : T' ⟶ Spec (CommRingCat.of A)}
(ψ : SchemeHomOver t' t),
Nonempty ((Scheme.Modules.pullback (baseChangeSnd (baseChange R c A) ψ)).obj
(E'.pullbackAlong t (Category.comp_id t)).lineBundle ≅ (E'.pullbackAlong t'
(Category.comp_id t')).lineBundle)) ∧
(∀ (Ω : Type u) [Field Ω] [IsAlgClosed Ω] (sΩ : Spec (CommRingCat.of Ω) ⟶ Spec
(CommRingCat.of A))
(φ : pullback (baseChange R c A) sΩ ≅ pullback c (sΩ ≫ specMap R A)),
φ.hom ≫ pullback.fst c (sΩ ≫ specMap R A) =
pullback.fst (baseChange R c A) sΩ ≫ pullback.fst c (specMap R A) →
Nonempty ((Scheme.Modules.pullback φ.hom).obj
(E.pullbackAlong (sΩ ≫ specMap R A) (Category.comp_id _)).lineBundle ≅
(E'.pullbackAlong sΩ (Category.comp_id sΩ)).lineBundle)) := by
have : IsSeparated (baseChange R c A) :=
inferInstanceAs (_root_.AlgebraicGeometry.IsSeparated (pullback.snd c (specMap R A)))
have : SmoothOfRelativeDimension 1 ((pullback.fst c (specMap R A) ⁻¹ᵁ U).ι ≫ baseChange R c A) :=
smoothOfRelativeDimension_one_preimage_ι_comp_snd c U (specMap R A)
let i2 : pullback (specMap R A) (z₀ ≫ c) ≅
pullback (Spec.map (CommRingCat.ofHom (algebraMap R A))) (Spec.map (CommRingCat.ofHom
(algebraMap R B₀))) :=
pullback.congrHom rfl hz₀
let e : Spec (CommRingCat.of (TensorProduct R A B₀)) ≅ pullback z₀ (pullback.fst c (specMap R A))
:=
(pullbackSpecIso R A B₀).symm ≪≫ i2.symm ≪≫ (pullbackSymmetry (z₀ ≫ c) (specMap R A)).symm ≪≫
(pullbackRightPullbackFstIso c (specMap R A) z₀).symm
let x : Spec (CommRingCat.of (TensorProduct R A B₀)) ⟶ pullback c (specMap R A) :=
e.hom ≫ pullback.snd z₀ (pullback.fst c (specMap R A))
have hxe : x = e.hom ≫ pullback.snd z₀ (pullback.fst c (specMap R A)) := rfl
have : IsClosedImmersion (pullback.snd z₀ (pullback.fst c (specMap R A))) :=
inferInstanceAs (_root_.AlgebraicGeometry.IsClosedImmersion
(pullback.snd z₀ (pullback.fst c (specMap R A))))
have hxci : IsClosedImmersion x := inferInstance
have hx_fst : x ≫ pullback.fst c (specMap R A) =
Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.includeRight (R := R) (A := A) (B :=
B₀)).toRingHom) ≫ z₀ := by
simp only [x, e, i2, Iso.trans_hom, Iso.symm_hom, Category.assoc]
rw [← pullback.condition, pullbackRightPullbackFstIso_inv_fst_assoc,
pullbackSymmetry_inv_comp_fst_assoc,
pullback.congrHom_inv, pullback.lift_snd_assoc, Category.comp_id,
pullbackSpecIso_inv_snd_assoc]
rfl
have hx_snd : x ≫ baseChange R c A = Spec.map (CommRingCat.ofHom (algebraMap A (TensorProduct R A
B₀))) := by
simp only [x, e, i2, Iso.trans_hom, Iso.symm_hom, Category.assoc]
rw [show baseChange R c A = pullback.snd c (specMap R A) from rfl,
pullbackRightPullbackFstIso_inv_snd_snd,
pullbackSymmetry_inv_comp_snd, pullback.congrHom_inv, pullback.lift_fst, Category.comp_id,
pullbackSpecIso_inv_fst']
let zA : Spec (CommRingCat.of (TensorProduct R A B₀)) ⟶ pullback (baseChange R c A) (𝟙 (Spec
(CommRingCat.of A))) :=
pullback.lift x (Spec.map (CommRingCat.ofHom (algebraMap A (TensorProduct R A B₀))))
(by rw [Category.comp_id]; exact hx_snd)
have hzA_fst : zA ≫ pullback.fst (baseChange R c A) (𝟙 (Spec (CommRingCat.of A))) = x :=
pullback.lift_fst _ _ _
have hzAci : IsClosedImmersion zA := by
rw [← MorphismProperty.cancel_right_of_respectsIso @IsClosedImmersion zA
(pullback.fst (baseChange R c A) (𝟙 (Spec (CommRingCat.of A)))), hzA_fst]
exact hxci
have hzA1 : zA ≫ pullback.fst (baseChange R c A) (𝟙 (Spec (CommRingCat.of A))) ≫ pullback.fst c
(specMap R A) =
Spec.map (CommRingCat.ofHom (Algebra.TensorProduct.includeRight (R := R) (A := A) (B :=
B₀)).toRingHom) ≫ z₀ := by
rw [← Category.assoc, hzA_fst, hx_fst]
have hzA2 : zA ≫ pullback.snd (baseChange R c A) (𝟙 (Spec (CommRingCat.of A))) =
Spec.map (CommRingCat.ofHom (algebraMap A (TensorProduct R A B₀))) := pullback.lift_snd _ _ _
obtain ⟨Zblk, hZI, hZU⟩ := RelEffCartierDiv.exists_I_eq_ker_lift_and_supportedIn_of_finite_etale
R c U A B₀ d φ₀ z₀ hz₀ hz₀U
obtain ⟨E₀, hE₀U, hE₀I⟩ := exists_sectionIdeal_pow_mul_pow c U ε hεU Zblk hZU r r'
have hεAU : Set.range (sectionBaseChange A ε).1.base ⊆
((pullback.fst c (specMap R A) ⁻¹ᵁ U : (pullback c (specMap R A)).Opens) : Set ↥(pullback c
(specMap R A))) :=
range_subset_preimage_of_comp_eq _ _ _ _ (sectionBaseChange_coe_fst A ε) U hεU
have hxU : Set.range x.base ⊆
((pullback.fst c (specMap R A) ⁻¹ᵁ U : (pullback c (specMap R A)).Opens) : Set ↥(pullback c
(specMap R A))) :=
range_subset_preimage_of_comp_eq _ _ _ _ hx_fst U hz₀U
obtain ⟨Zblk', hZ'I, hZ'U⟩ :=
RelEffCartierDiv.exists_I_eq_ker_lift_and_supportedIn_of_finite_etale
A (baseChange R c A) (pullback.fst c (specMap R A) ⁻¹ᵁ U) A (TensorProduct R A B₀) d
((Algebra.TensorProduct.lid A (TensorProduct R A B₀)).trans φ₀) x hx_snd hxU
have hZ'I' : Zblk'.I = zA.ker := hZ'I
obtain ⟨E₀', hE₀'U, hE₀'I⟩ := exists_sectionIdeal_pow_mul_pow (baseChange R c A) (pullback.fst c
(specMap R A) ⁻¹ᵁ U)
(sectionBaseChange A ε) hεAU Zblk' hZ'U r r'
refine ⟨zA, hzAci, hzA1, hzA2, castDeg hρ.symm E₀, castDeg hρ.symm E₀', castDeg_supportedIn _ _
hE₀U,
castDeg_supportedIn _ _ hE₀'U, ?_, ?_, ?_, ?_, ?_⟩
· rw [castDeg_I, hE₀I, hZI]
· rw [castDeg_I, hE₀'I, hZ'I']
· intro T t
exact RelEffCartierDiv.isInvertible_I_of_supportedIn (pullback.fst c (specMap R A) ⁻¹ᵁ U) _
((castDeg_supportedIn _ _ hE₀'U).pullbackAlong t _)
· intro T T' t t' ψ
exact RelEffCartierDiv.nonempty_pullback_lineBundle_pullbackAlong_iso_of_supportedIn A
(baseChange R c A)
(pullback.fst c (specMap R A) ⁻¹ᵁ U) (castDeg hρ.symm E₀') (castDeg_supportedIn _ _ hE₀'U) ψ
· have fibreCompat : ∀ (Ω : Type u) [Field Ω] [IsAlgClosed Ω] (sΩ : Spec (CommRingCat.of Ω) ⟶
Spec (CommRingCat.of A))
(φ : pullback (baseChange R c A) sΩ ≅ pullback c (sΩ ≫ specMap R A)),
φ.hom ≫ pullback.fst c (sΩ ≫ specMap R A) =
pullback.fst (baseChange R c A) sΩ ≫ pullback.fst c (specMap R A) →
Nonempty ((Scheme.Modules.pullback φ.hom).obj
((castDeg hρ.symm E₀).pullbackAlong (sΩ ≫ specMap R A) (Category.comp_id _)).lineBundle
≅
((castDeg hρ.symm E₀').pullbackAlong sΩ (Category.comp_id sΩ)).lineBundle) := by
intro Ω _ _ sΩ φ hφ
have hinv : ((castDeg hρ.symm E₀).pullbackAlong (sΩ ≫ specMap R A) (Category.comp_id
_)).I.IsInvertible :=
RelEffCartierDiv.isInvertible_I_of_supportedIn U _ ((castDeg_supportedIn _ _
hE₀U).pullbackAlong _ _)
obtain ⟨eT⟩ := hinv.nonempty_pullback_invModule_iso φ.hom (hinv.comap_of_isOpenImmersion
φ.hom)
have hE'g : E₀'.I = E₀.I.comap (gMap c A) := by
rw [hE₀'I, hZ'I', hE₀I, hZI, Scheme.IdealSheafData.comap_mul, comap_pow, comap_pow,
comap_gMap_sectionIdeal,
ker_lift_eq_comap_gMap_ker_lift c A z₀ hz₀ e x hxe hx_snd]
have hsq : φ.hom ≫ mapOnProdOver c (sΩ ≫ specMap R A) (Category.comp_id _) =
mapOnProdOver (baseChange R c A) sΩ (Category.comp_id sΩ) ≫ gMap c A := by
apply pullback.hom_ext
· rw [Category.assoc, mapOnProdOver_fst, hφ, Category.assoc, gMap_fst,
mapOnProdOver_fst_assoc]
· rw [snd_eq_fst_comp, ← Category.assoc, ← Category.assoc, Category.assoc φ.hom,
mapOnProdOver_fst, hφ,
Category.assoc (mapOnProdOver _ _ _), gMap_fst, mapOnProdOver_fst_assoc]
have key : ((castDeg hρ.symm E₀).pullbackAlong (sΩ ≫ specMap R A) (Category.comp_id
_)).I.comap φ.hom =
((castDeg hρ.symm E₀').pullbackAlong sΩ (Category.comp_id sΩ)).I := by
change (E₀.I.comap (mapOnProdOver c (sΩ ≫ specMap R A) (Category.comp_id _))).comap φ.hom =
E₀'.I.comap (mapOnProdOver (baseChange R c A) sΩ (Category.comp_id sΩ))
rw [← Scheme.IdealSheafData.comap_comp, hsq, Scheme.IdealSheafData.comap_comp, hE'g]
exact ⟨eT ≪≫ eqToIso (by rw [key])⟩
exact fibreCompat