AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_split.AlgebraicGeometry.RelEffCartierDiv.SplitProof.exists_split
Source context 16 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.RelativeDivisors.Proofs.RelEffCartierDiv_exists_split
universe u
open _root_.CategoryTheory
open _root_.CategoryTheory.Limits
open _root_.AlgebraicGeometry
namespace AlgebraicGeometry
open _root_.AlgebraicGeometry
namespace RelEffCartierDiv
open _root_.AlgebraicGeometry.RelEffCartierDiv
namespace SplitProof
open _root_.AlgebraicGeometry.RelEffCartierDiv
open _root_.AlgebraicGeometry
open _root_.AlgebraicGeometry.RelEffCartierDiv
variable {𝒞 S : Scheme.{u}} {f : 𝒞 ⟶ S}
variable [IsSeparated f] [SmoothOfRelativeDimension 1 f]
Lean source · full declarationtheorem exists_split : ∀ (r : ℕ) {T : Scheme.{u}} {g : T ⟶ S} (D : RelEffCartierDiv f r g),
∃ (P : Scheme.{u}) (gP : P ⟶ S) (p : P ⟶ T) (hp : p ≫ g = gP)
(b : Fin r → (P ⟶ 𝒞)) (hb : ∀ i, b i ≫ f = gP),
IsFinite p ∧ Flat p ∧ LocallyOfFinitePresentation p ∧ Surjective p ∧
(∀ t : T, p.finrank t = r.factorial) ∧
(D.pullbackAlong p hp).I = prodKerGraph f b hb ∧
∀ ⦃T' : Scheme.{u}⦄ (g' : T' ⟶ S) (q : T' ⟶ T) (hq : q ≫ g = g')
(b' : Fin r → (T' ⟶ 𝒞)) (hb' : ∀ i, b' i ≫ f = g'),
(D.pullbackAlong q hq).I = prodKerGraph f b' hb' →
∃! u : T' ⟶ P, u ≫ p = q ∧ ∀ i, u ≫ b i = b' i
| 0, T, g, D => by
refine ⟨T, g, 𝟙 T, Category.id_comp g, Fin.elim0, fun i => i.elim0, inferInstance,
inferInstance, inferInstance, inferInstance, fun t => ?_, ?_, ?_⟩
· rw [Nat.factorial_zero, Scheme.Hom.finrank_eq_one_of_isIso (𝟙 T)]
rfl
· change D.I.comap _ = _
rw [RelEffCartierDiv.I_eq_top_of_degree_zero D, Scheme.IdealSheafData.comap_top,
prodKerGraph_zero]
· intro T' g' q hq b' hb' _
refine ⟨q, ⟨Category.comp_id q, fun i => i.elim0⟩, fun u hu => ?_⟩
simpa only [Category.comp_id] using hu.1
| r + 1, T, g, D => by
have := D.isFinite
have := D.flat
have := D.locallyOfFinitePresentation
let π : D.I.subscheme ⟶ T := D.I.subschemeι ≫ pullback.snd f g
let gZ : D.I.subscheme ⟶ S := π ≫ g
have hπ : π ≫ g = gZ := rfl
let a : D.I.subscheme ⟶ 𝒞 := D.I.subschemeι ≫ pullback.fst f g
have ha : a ≫ f = gZ := by
simp only [a, gZ, π, Category.assoc, pullback.condition]
have hπsurj : Surjective π := surjective_of_finrank_eq_succ π D.finrank_eq
have htaut : (D.pullbackAlong π hπ).I ≤ (graphOver f a ha).ker :=
D.pullbackAlong_I_le_ker_graphOver_taut hπ
obtain ⟨E, hE⟩ := RelEffCartierDiv.exists_I_eq_ker_graphOver_mul (D.pullbackAlong π hπ) a ha
htaut
obtain ⟨P, gP, pE, hpE, bE, hbE, hfin, hflat, hlfp, hsurj, hrank, hsplit, huniv⟩ :=
exists_split r E
have hp : (pE ≫ π) ≫ g = gP := by rw [Category.assoc]; exact hpE
have hb : ∀ i, (Fin.cons (pE ≫ a) bE : Fin (r + 1) → (P ⟶ 𝒞)) i ≫ f = gP :=
Fin.cases (by rw [Fin.cons_zero, Category.assoc, ha]; exact hpE)
(fun i => by rw [Fin.cons_succ]; exact hbE i)
refine ⟨P, gP, pE ≫ π, hp, Fin.cons (pE ≫ a) bE, hb, inferInstance, inferInstance,
inferInstance, inferInstance, fun t => ?_, ?_, ?_⟩
· rw [Scheme.Hom.finrank_comp_of_finrank_eq_const pE π r.factorial hrank t,
show π.finrank t = r + 1 from D.finrank_eq t, Nat.factorial_succ, Nat.mul_comm]
· have hcomp : D.pullbackAlong (pE ≫ π) hp = (D.pullbackAlong π hπ).pullbackAlong pE hpE :=
(RelEffCartierDiv.pullbackAlong_comp D π hπ pE hpE).symm
rw [hcomp]
change (D.pullbackAlong π hπ).I.comap (mapOnProdOver f pE hpE) = _
rw [hE, Scheme.IdealSheafData.comap_mul, ker_graphOver_comap]
change _ * (E.pullbackAlong pE hpE).I = _
rw [hsplit]
exact (prodKerGraph_cons (pE ≫ a) _ bE hbE).symm
· intro T' g' q hq b' hb' hsplit'
have hle : (D.pullbackAlong q hq).I ≤ (graphOver f (b' 0) (hb' 0)).ker := by
rw [hsplit', prodKerGraph_succ]
exact mul_le_of_le_one_right bot_le le_top
let z : T' ⟶ D.I.subscheme := D.liftOfLE q hq (b' 0) (hb' 0) hle
have hzπ : z ≫ π = q := D.liftOfLE_ι_snd q hq (b' 0) (hb' 0) hle
have hza : z ≫ a = b' 0 := D.liftOfLE_ι_fst q hq (b' 0) (hb' 0) hle
have hz : z ≫ gZ = g' := by
change z ≫ (π ≫ g) = g'
rw [← Category.assoc, hzπ, hq]
have hEz : (E.pullbackAlong z hz).I = prodKerGraph f (fun i => b' i.succ) (fun i => hb'
i.succ) := by
have h1 : ((D.pullbackAlong π hπ).pullbackAlong z hz).I =
(graphOver f (b' 0) (hb' 0)).ker * (E.pullbackAlong z hz).I := by
change (D.pullbackAlong π hπ).I.comap (mapOnProdOver f z hz) = _
rw [hE, Scheme.IdealSheafData.comap_mul, ker_graphOver_comap,
graphOver_congr hza _ (hb' 0)]
rfl
have h2 : ((D.pullbackAlong π hπ).pullbackAlong z hz).I =
(graphOver f (b' 0) (hb' 0)).ker * prodKerGraph f (fun i => b' i.succ) (fun i => hb'
i.succ) := by
rw [RelEffCartierDiv.pullbackAlong_comp D π hπ z hz,
pullbackAlong_congr D hzπ _ hq, hsplit', prodKerGraph_succ]
have hinv : (graphOver f (b' 0) (hb' 0)).ker.IsInvertible :=
RelEffCartierDiv.isInvertible_I (RelEffCartierDiv.ofPoint f (b' 0) (hb' 0))
exact hinv.mul_left_cancel (h1.symm.trans h2)
obtain ⟨u, ⟨hu1, hu2⟩, huniq⟩ := huniv g' z hz (fun i => b' i.succ) (fun i => hb' i.succ) hEz
refine ⟨u, ⟨?_, ?_⟩, ?_⟩
· rw [← Category.assoc, hu1, hzπ]
· refine Fin.cases ?_ (fun i => ?_)
· rw [Fin.cons_zero, ← Category.assoc, hu1, hza]
· rw [Fin.cons_succ]
exact hu2 i
· intro u' ⟨hu'1, hu'2⟩
have hz' : u' ≫ pE = z := by
apply D.hom_subscheme_ext
· change (u' ≫ pE) ≫ a = z ≫ a
rw [hza, Category.assoc]
have := hu'2 0
rwa [Fin.cons_zero] at this
· change (u' ≫ pE) ≫ π = z ≫ π
rw [hzπ, Category.assoc]
exact hu'1
exact huniq u' ⟨hz', fun i => by have := hu'2 i.succ; rwa [Fin.cons_succ] at this⟩