OModulePresheafIdealFiltration.lean

def IdealAnnihilates (I : V.IdealSheafData) (F : OModulePresheaf π) : Prop

def idealSections (I : V.IdealSheafData) (U : V.Opens) : Ideal Γ(V, U)

theorem idealSections_eq_ideal (I : V.IdealSheafData) (U : V.affineOpens) :
    idealSections I U.1 = I.ideal U

theorem idealSections_res (I : V.IdealSheafData) {U U' : V.Opens} (h : U ≤ U')
    (a : Γ(V, U')) (ha : a ∈ idealSections I U') :
    (V.presheaf.map (homOfLE h).op).hom a ∈ idealSections I U

theorem idealSections_pow_res (I : V.IdealSheafData) (k : ℕ)
    {U U' : V.Opens} (h : U ≤ U') (a : Γ(V, U'))
    (ha : a ∈ idealSections I U' ^ k) :
    (V.presheaf.map (homOfLE h).op).hom a ∈ idealSections I U ^ k

def idealPowSub (I : V.IdealSheafData) (F : OModulePresheaf π) (k : ℕ)
    (U : V.Opens) : Submodule R (F.obj U)

theorem idealPowSub_res (I : V.IdealSheafData) (F : OModulePresheaf π) (k : ℕ)
    {U U' : V.Opens} (h : U ≤ U') (x : F.obj U')
    (hx : x ∈ idealPowSub π I F k U') :
    F.res h x ∈ idealPowSub π I F k U

def idealPow (I : V.IdealSheafData) (F : OModulePresheaf π) (k : ℕ) :
    OModulePresheaf π where
  obj U := idealPowSub π I F k U
  addCommGroup U := inferInstance
  module U := inferInstance
  moduleSections U :=
    letI := (Scheme.TwoAffineOpenCover.algebraOfHom π U).toModule; haveI := F.isScalarTower U
    inferInstanceAs (Module Γ(V, U)
      ((idealSections I U ^ k • (⊤ : Submodule _ _)).restrictScalars R))
  isScalarTower U := by
    let := (Scheme.TwoAffineOpenCover.algebraOfHom π U).toModule; have := F.isScalarTower U
    exact inferInstanceAs (IsScalarTower R Γ(V, U)
      ((idealSections I U ^ k • (⊤ : Submodule _ _)).restrictScalars R))
  res {U U'} h := LinearMap.codRestrict (idealPowSub π I F k U)
    ((F.res h).comp (idealPowSub π I F k U').subtype)
    (fun x => idealPowSub_res π I F k h x.1 x.2)
  res_smul {U U'} h a x := by
    let := (Scheme.TwoAffineOpenCover.algebraOfHom π U').toModule; have := F.isScalarTower U'
    let := (Scheme.TwoAffineOpenCover.algebraOfHom π U).toModule; have := F.isScalarTower U
    exact Subtype.ext (F.res_smul h a x.1)
  res_refl U := LinearMap.ext fun x =>
    Subtype.ext (LinearMap.congr_fun (F.res_refl U) x.1)
  res_comp {U U' U''} h h' := LinearMap.ext fun x =>
    Subtype.ext (LinearMap.congr_fun (F.res_comp h h') x.1)

theorem mem_idealPowSub_iff_of_affine (I : V.IdealSheafData) (F : OModulePresheaf π)
    (k : ℕ) (U : V.affineOpens) (x : F.obj U.1) :
    (⟨x, Submodule.mem_top⟩ : (⊤ : Submodule R (F.obj U.1))).1 ∈
        idealPowSub π I F k U.1
      ↔ x ∈ (I.ideal U ^ k • (⊤ : Submodule Γ(V, U.1) (F.obj U.1)))

theorem idealPowSub_antitone (I : V.IdealSheafData) (F : OModulePresheaf π)
    {k k' : ℕ} (h : k ≤ k') (U : V.Opens) :
    idealPowSub π I F k' U ≤ idealPowSub π I F k U

def idealPowSuccSub (I : V.IdealSheafData) (F : OModulePresheaf π) (k : ℕ) (U : V.Opens) :
    Submodule R ((idealPow π I F k).obj U)

theorem idealPowSub_smul_mem (I : V.IdealSheafData) (F : OModulePresheaf π) (k : ℕ)
    (U : V.Opens) (a : Γ(V, U)) (x : F.obj U)
    (hx : x ∈ idealPowSub π I F k U) :
    a • x ∈ idealPowSub π I F k U

theorem idealPowSuccSub_smul_mem (I : V.IdealSheafData) (F : OModulePresheaf π) (k : ℕ)
    (U : V.Opens) (a : Γ(V, U)) (x : (idealPow π I F k).obj U)
    (hx : x ∈ idealPowSuccSub π I F k U) :
    a • x ∈ idealPowSuccSub π I F k U

def idealPowQuotModuleSections (I : V.IdealSheafData) (F : OModulePresheaf π) (k : ℕ) (U :
    V.Opens) :
    Module Γ(V, U) ((idealPow π I F k).obj U
      ⧸ idealPowSuccSub π I F k U)

theorem idealPowQuot_smul_mk (I : V.IdealSheafData) (F : OModulePresheaf π) (k : ℕ)
    (U : V.Opens) (a : Γ(V, U)) (y : (idealPow π I F k).obj U) :
    letI := idealPowQuotModuleSections π I F k U
    a • (idealPowSuccSub π I F k U).mkQ y
      = (idealPowSuccSub π I F k U).mkQ (a • y) :=
  rfl

def idealPowQuot (I : V.IdealSheafData) (F : OModulePresheaf π) (k : ℕ) :
    OModulePresheaf π where
  obj U := (idealPow π I F k).obj U ⧸ idealPowSuccSub π I F k U
  addCommGroup U := inferInstance
  module U := inferInstance
  moduleSections U := idealPowQuotModuleSections π I F k U
  isScalarTower U := by
    let := (Scheme.TwoAffineOpenCover.algebraOfHom π U).toModule; let :=
      idealPowQuotModuleSections π I F k U
    refine ⟨fun r a x => ?_⟩
    obtain ⟨y, rfl⟩ := (idealPowSuccSub π I F k U).mkQ_surjective x
    rw [idealPowQuot_smul_mk, idealPowQuot_smul_mk, ← map_smul]
    exact congrArg _
      ((idealPow π I F k).isScalarTower U |>.smul_assoc r a y)
  res {U U'} h := Submodule.mapQ _ _ ((idealPow π I F k).res h)
    (fun x hx => idealPowSub_res π I F (k + 1) h _ hx)
  res_smul {U U'} h a x := by
    let := idealPowQuotModuleSections π I F k U'
    let := idealPowQuotModuleSections π I F k U
    obtain ⟨y, rfl⟩ := (idealPowSuccSub π I F k U').mkQ_surjective x
    rw [idealPowQuot_smul_mk]
    change (idealPowSuccSub π I F k U).mkQ
        ((idealPow π I F k).res h (a • y)) = _
    rw [(idealPow π I F k).res_smul h a y, ← idealPowQuot_smul_mk]
    rfl
  res_refl U := LinearMap.ext fun x => by
    obtain ⟨y, rfl⟩ := (idealPowSuccSub π I F k U).mkQ_surjective x
    exact congrArg ((idealPowSuccSub π I F k U).mkQ)
      (LinearMap.congr_fun ((idealPow π I F k).res_refl U) y)
  res_comp {U U' U''} h h' := LinearMap.ext fun x => by
    obtain ⟨y, rfl⟩ := (idealPowSuccSub π I F k U'').mkQ_surjective x
    exact congrArg ((idealPowSuccSub π I F k U).mkQ)
      (LinearMap.congr_fun ((idealPow π I F k).res_comp h h') y)

def idealPowSuccInc (I : V.IdealSheafData) (F : OModulePresheaf π) (k : ℕ) :
    OModulePresheaf.AffHom (idealPow π I F (k + 1))
      (idealPow π I F k) where
  app U := Submodule.inclusion
    (idealPowSub_antitone π I F k.le_succ U.1)
  app_smul _U _a _x := rfl
  naturality {_U _U'} _h := LinearMap.ext fun _x => Subtype.ext rfl

def idealPowSES (I : V.IdealSheafData) (F : OModulePresheaf π) (k : ℕ) :
    OModulePresheaf.AffSES (idealPow π I F (k + 1))
      (idealPow π I F k) (idealPowQuot π I F k) where
  inc := idealPowSuccInc π I F k
  proj :=
    { app := fun U => (idealPowSuccSub π I F k U.1).mkQ
      app_smul := fun U a y => (idealPowQuot_smul_mk π I F k U.1 a y).symm
      naturality := fun {U U'} h => LinearMap.ext fun _ => rfl }
  injective U := Submodule.inclusion_injective
    (idealPowSub_antitone π I F k.le_succ U.1)
  surjective U := (idealPowSuccSub π I F k U.1).mkQ_surjective
  exact U := by
    refine le_antisymm (LinearMap.range_le_ker_iff.mpr (LinearMap.ext fun y => ?_)) fun x hx => ?_
    · change (idealPowSuccSub π I F k U.1).mkQ (Submodule.inclusion
        (idealPowSub_antitone π I F k.le_succ U.1) y) = 0
      exact (Submodule.Quotient.mk_eq_zero _).mpr y.2
    · have hx' : x ∈ idealPowSuccSub π I F k U.1 :=
        (Submodule.Quotient.mk_eq_zero _).mp (LinearMap.mem_ker.mp hx :
          (idealPowSuccSub π I F k U.1).mkQ x = 0)
      refine ⟨⟨(idealPowSub π I F k U.1).subtype x, hx'⟩, ?_⟩
      change Submodule.inclusion (idealPowSub_antitone π I F k.le_succ U.1) _ = x
      apply Subtype.ext
      change (idealPowSub π I F k U.1).subtype x
        = (idealPowSub π I F k U.1).subtype x
      rfl

theorem idealAnnihilates_idealPowQuot (I : V.IdealSheafData) (F : OModulePresheaf π) (k : ℕ) :
    IdealAnnihilates π I (idealPowQuot π I F k)

theorem idealPowSub_zero (I : V.IdealSheafData) (F : OModulePresheaf π)
    (U : V.Opens) : idealPowSub π I F 0 U = ⊤

def idealPowZeroSES (I : V.IdealSheafData) (F : OModulePresheaf π) :
    OModulePresheaf.AffSES (OModulePresheaf.zero π) (idealPow π I F 0) F where
  inc := OModulePresheaf.AffHom.zeroFrom _
  proj :=
    { app := fun U => (idealPowSub π I F 0 U.1).subtype
      app_smul := fun _ _ _ => rfl
      naturality := fun {_U _U'} _h => LinearMap.ext fun _x => rfl }
  injective _ _ _ _ := Subsingleton.elim _ _
  surjective U x := ⟨⟨x, idealPowSub_zero π I F U.1 ▸ Submodule.mem_top⟩, rfl⟩
  exact _U := le_antisymm (fun _ ⟨_, hz⟩ => hz ▸ LinearMap.mem_ker.mpr rfl)
    (fun _x hx => ⟨0, Subtype.ext (LinearMap.mem_ker.mp hx).symm⟩)