AlgebraicGeometry.RelPicard.RepresentsRelSubPic.kerPoints_baseChange_surjective_and_fibre
Source context 15 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicGeometry.RelPicard.RepresentsRelSubPic
open _root_.JacobianVarieties.Picard.Proofs.KernelBaseChange
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelPicard
open _root_.NeronModelInfra
open _root_.GoodReductionJacobian
open _root_.AlgebraicGeometry.Scheme.TwoAffineOpenCover
open _root_.JacobianVarieties.Picard.Proofs
attribute [local simp] sigmaK_val_val
open _root_.JacobianVarieties.Picard.Proofs
open KernelBaseChange.AlgebraicGeometry.RelPicard.KerBC in
Lean source · full declarationtheorem kerPoints_baseChange_surjective_and_fibre
{R : Type u} [CommRing R]
{X : Scheme.{u}} (c : X ⟶ Spec (CommRingCat.of R)) [IsProper c]
[SmoothOfRelativeDimension 1 c] [GeometricallyIntegral c]
(ε : SchemeHomOver (𝟙 (Spec (CommRingCat.of R))) c)
(D : RelativePic0Designation R c)
(hD : RepresentsRelSubPic c ε (algEquivZeroCut c ε) D)
(𝒱 : X.TwoAffineOpenCover)
(A : Type u) [CommRing A] [Algebra R A] (hA : Function.Surjective (algebraMap R A))
(q : ℕ) (hq : RingHom.ker (algebraMap R A) = Ideal.span {(q : R)}) :
let L : RelativeGroupLaw R D.toBase := RepresentsRelSubPic.relativeGroupLaw (P :=
algEquivZeroGroupCut c ε) hD
let tR : Spec (CommRingCat.of (DualNumber R)) ⟶ Spec (CommRingCat.of R) :=
Scheme.TwoAffineOpenCover.specMap R (DualNumber R)
let tA : Spec (CommRingCat.of (DualNumber A)) ⟶ Spec (CommRingCat.of R) :=
Scheme.TwoAffineOpenCover.specMap R (DualNumber A)
let σ : Spec (CommRingCat.of (DualNumber A)) ⟶ Spec (CommRingCat.of (DualNumber R)) :=
(RelPicard.LFP.stageHom R (DualNumber.lift ⟨(Algebra.ofId R (DualNumber A), DualNumber.eps),
DualNumber.eps_mul_eps, fun _ => Commute.all _ _⟩)).1
(∀ x : SchemeHomOver tR D.toBase,
dualNumberReduction R R ≫ x.1 = (L.one (Scheme.TwoAffineOpenCover.specMap R R)).1 →
dualNumberReduction R A ≫ (σ ≫ x.1) = (L.one (Scheme.TwoAffineOpenCover.specMap R A)).1) ∧
(∀ x y : SchemeHomOver tR D.toBase,
σ ≫ (L.mul tR x y).1 =
(L.mul tA ⟨σ ≫ x.1, by
rw [Category.assoc, x.2]
exact (RelPicard.LFP.stageHom R (DualNumber.lift ⟨(Algebra.ofId R (DualNumber A),
DualNumber.eps), DualNumber.eps_mul_eps, fun _ => Commute.all _ _⟩)).2⟩
⟨σ ≫ y.1, by
rw [Category.assoc, y.2]
exact (RelPicard.LFP.stageHom R (DualNumber.lift ⟨(Algebra.ofId R (DualNumber A),
DualNumber.eps), DualNumber.eps_mul_eps, fun _ => Commute.all _ _⟩)).2⟩).1) ∧
(∀ (φ : SchemeHomOver D.toBase D.toBase) (x : SchemeHomOver tR D.toBase), σ ≫ (x.1 ≫ φ.1) = (σ
≫ x.1) ≫ φ.1) ∧
(∀ y : SchemeHomOver tA D.toBase,
dualNumberReduction R A ≫ y.1 = (L.one (Scheme.TwoAffineOpenCover.specMap R A)).1 →
∃ x : SchemeHomOver tR D.toBase,
dualNumberReduction R R ≫ x.1 = (L.one (Scheme.TwoAffineOpenCover.specMap R R)).1 ∧ σ ≫
x.1 = y.1) ∧
(∀ x x' : SchemeHomOver tR D.toBase,
dualNumberReduction R R ≫ x.1 = (L.one (Scheme.TwoAffineOpenCover.specMap R R)).1 →
dualNumberReduction R R ≫ x'.1 = (L.one (Scheme.TwoAffineOpenCover.specMap R R)).1 →
(σ ≫ x.1 = σ ≫ x'.1 ↔
∃ z : SchemeHomOver tR D.toBase,
dualNumberReduction R R ≫ z.1 = (L.one (Scheme.TwoAffineOpenCover.specMap R R)).1 ∧
x' = L.mul tR x (L.nsmul tR q z))) := by
intro L tR tA σ
obtain ⟨δR, hδR⟩ := exists_isDeformationClassMap c ε R 𝒱
obtain ⟨δA, hδA⟩ := exists_isDeformationClassMap c ε A 𝒱
have hΔR := Δ_bijective hD hδR
have hΔA := Δ_bijective hD hδA
have hbcA := H1baseChangeMap_surjective_and_eq_iff_of_surjective 𝒱 c A hA
have hbcR := H1baseChangeMap_surjective_and_eq_iff_of_surjective 𝒱 c R (fun r => ⟨r, rfl⟩)
have hq0 : algebraMap R A q = 0 := by
rw [← RingHom.mem_ker, hq]; exact Ideal.mem_span_singleton_self _
have hstage_q : ∀ m : H1StructureSheaf c R 𝒱,
𝒱.H1stageMap c (Algebra.ofId R A) ((q : R) • m) = 0 := fun m => by
have h' : (Algebra.ofId R A).toRingHom (q : R) = 0 := hq0
rw [LinearMap.map_smulₛₗ, h', zero_smul]
refine ⟨fun x hx => sigma_mem hD A x hx, fun x y => ?_, fun φ x => (Category.assoc _ _ _).symm,
fun y hy => ?_,
fun x x' hx hx' => ?_⟩
· exact congrArg Subtype.val
((RepresentsRelSubPic.relativeGroupLaw (P := algEquivZeroGroupCut c ε) hD).mul_natural tR tA
σ (sigmaOver R A).2 x y)
· obtain ⟨u, hu⟩ := hbcA.1 (Δ hD (δ := δA) ⟨y, hy⟩)
obtain ⟨xK, hxK⟩ := hΔR.2 (𝒱.H1baseChangeMap c R u)
refine ⟨xK.1, xK.2, ?_⟩
have key : Δ hD (δ := δA) (sigmaK hD A xK) = Δ hD (δ := δA) ⟨y, hy⟩ := by
rw [Δ_sigmaK hD hδR hδA, hxK, H1stageMap_H1baseChangeMap, hu]
exact congrArg (fun z : K hD A => z.1.1) (hΔA.1 key)
· constructor
· intro hσ
have hK : sigmaK hD A ⟨x, hx⟩ = sigmaK hD A ⟨x', hx'⟩ := Subtype.ext (Subtype.ext hσ)
obtain ⟨u, hu⟩ := hbcR.1 (Δ hD (δ := δR) ⟨x, hx⟩)
obtain ⟨u', hu'⟩ := hbcR.1 (Δ hD (δ := δR) ⟨x', hx'⟩)
have h1 : 𝒱.H1baseChangeMap c A u = 𝒱.H1baseChangeMap c A u' := by
rw [← H1stageMap_H1baseChangeMap 𝒱 c (Algebra.ofId R A) u, ← H1stageMap_H1baseChangeMap 𝒱 c
(Algebra.ofId R A) u',
hu, hu', ← Δ_sigmaK hD hδR hδA, ← Δ_sigmaK hD hδR hδA, hK]
have h2 : u - u' ∈ RingHom.ker (algebraMap R A) • (⊤ : Submodule R _) := (hbcA.2 u u').mp h1
rw [hq, Submodule.ideal_span_singleton_smul, Submodule.mem_smul_pointwise_iff_exists] at h2
obtain ⟨v, -, hv⟩ := h2
obtain ⟨zK, hzK⟩ := hΔR.2 (𝒱.H1baseChangeMap c R (-v))
refine ⟨zK.1, zK.2, ?_⟩
have huu : u' = u + (q : R) • (-v) := by
rw [smul_neg, hv]; abel
have key : Δ hD (δ := δR) ⟨x', hx'⟩ =
Δ hD (δ := δR) (mulK hD R ⟨x, hx⟩ (nsmulK hD R q zK)) := by
rw [Δ_mulK hD hδR, Δ_nsmulK hD hδR, hzK, ← hu, ← hu', huu, map_add, LinearMap.map_smulₛₗ]
congr 1
exact Nat.cast_smul_eq_nsmul R q _
have h3 := congrArg (fun z : K hD R => z.1) (hΔR.1 key)
simp only at h3
rw [h3]
change (RepresentsRelSubPic.relativeGroupLaw (P := algEquivZeroGroupCut c ε) hD).mul _ x
(nsmulK hD R q zK).1 = _
rw [nsmulK_val]
· rintro ⟨z, hz, rfl⟩
have key : Δ hD (δ := δA) (sigmaK hD A (mulK hD R ⟨x, hx⟩ (nsmulK hD R q ⟨z, hz⟩))) =
Δ hD (δ := δA) (sigmaK hD A ⟨x, hx⟩) := by
rw [Δ_sigmaK hD hδR hδA, Δ_sigmaK hD hδR hδA, Δ_mulK hD hδR, Δ_nsmulK hD hδR, map_add,
← Nat.cast_smul_eq_nsmul R, hstage_q, add_zero]
have h := congrArg (fun z : K hD A => z.1.1) (hΔA.1 key)
simp only [sigmaK_val_val] at h
rw [← h]
change σ ≫ ((RepresentsRelSubPic.relativeGroupLaw (P := algEquivZeroGroupCut c ε) hD).mul _ x
(nsmulK hD R q ⟨z, hz⟩).1).1 = _
rw [nsmulK_val]