QuasicoherentKernel.lean

theorem isLocalizedModule_of_commuting_isos
    {R : CommRingCat.{u}} (S : Submonoid R)
    {A B C D : ModuleCat.{u} R} (eA : A ≅ C) (eB : B ≅ D)
    (f : A ⟶ B) (g : C ⟶ D)
    (h : f ≫ eB.hom = eA.hom ≫ g)
    (hg : IsLocalizedModule S g.hom) : IsLocalizedModule S f.hom

def affineModulePresheaf {R : CommRingCat.{u}} (M : (Spec R).Modules) :
    (Spec R).Opensᵒᵖ ⥤ ModuleCat.{u} R

def affineModuleMap {R : CommRingCat.{u}} {M N : (Spec R).Modules}
    (φ : M ⟶ N) : affineModulePresheaf M ⟶ affineModulePresheaf N

def affineBasicOpen (R : CommRingCat.{u}) (r : R) : (Spec R).Opens

def affineBasicOpenInclusion (R : CommRingCat.{u}) (r : R) :
    affineBasicOpen R r ⟶ (⊤ : (Spec R).Opens)

def nativeAffineSectionFunctor (R : CommRingCat.{u}) (U : (Spec R).Opens) :
    (Spec R).Modules ⥤ ModuleCat.{u} R

theorem restrictScalars_preservesFiniteLimits_native
    {A B : Type u} [Ring A] [Ring B] (f : A →+* B) :
    PreservesFiniteLimits (ModuleCat.restrictScalars.{u} f) where
  preservesFiniteLimits _ _ _ :=
    { preservesLimit := fun {D} => ModuleCat.preservesLimit_restrictScalars f D }

instance nativeAffineSectionFunctor_preservesFiniteLimits
    (R : CommRingCat.{u}) (U : (Spec R).Opens) :
    PreservesFiniteLimits (nativeAffineSectionFunctor R U)

abbrev affineSectionFunctor (R : CommRingCat.{u}) (U : (Spec R).Opens) :
    (Spec R).Modules ⥤ ModuleCat.{u} R where
  obj M := (affineModulePresheaf M).obj (op U)
  map φ := (affineModuleMap φ).app (op U)
  map_id _ := rfl
  map_comp _ _ := rfl

def nativeAffineSectionFunctorIso
    (R : CommRingCat.{u}) (U : (Spec R).Opens) :
    nativeAffineSectionFunctor R U ≅ affineSectionFunctor R U

instance affineSectionFunctor_preservesFiniteLimits
    (R : CommRingCat.{u}) (U : (Spec R).Opens) :
    PreservesFiniteLimits (affineSectionFunctor R U)

instance affineSectionFunctor_preservesZeroMorphisms
    (R : CommRingCat.{u}) (U : (Spec R).Opens) :
    (affineSectionFunctor R U).PreservesZeroMorphisms where
  map_zero _ _ := rfl

def sectionKernel {R : CommRingCat.{u}} {M N : (Spec R).Modules}
    (φ : M ⟶ N) (U : (Spec R).Opens) : ModuleCat.{u} R

def kernelSectionIso {R : CommRingCat.{u}} {M N : (Spec R).Modules}
    {φ : M ⟶ N} (c : KernelFork φ) (hc : IsLimit c) (U : (Spec R).Opens) :
    (affineSectionFunctor R U).obj c.pt ≅
      sectionKernel φ U

lemma kernelSectionIso_comp_subtype
    {R : CommRingCat.{u}} {M N : (Spec R).Modules}
    {φ : M ⟶ N} (c : KernelFork φ) (hc : IsLimit c) (U : (Spec R).Opens) :
    (kernelSectionIso c hc U).hom ≫
      ModuleCat.ofHom ((affineSectionFunctor R U).map φ).hom.ker.subtype =
        (affineSectionFunctor R U).map c.ι

lemma kernelSectionIso_hom_apply_val
    {R : CommRingCat.{u}} {M N : (Spec R).Modules}
    {φ : M ⟶ N} (c : KernelFork φ) (hc : IsLimit c) (U : (Spec R).Opens)
    (x : (affineSectionFunctor R U).obj c.pt) :
    ((kernelSectionIso c hc U).hom.hom x).val =
      ((affineSectionFunctor R U).map c.ι).hom x

lemma sectionRestriction_square
    {R : CommRingCat.{u}} {M N : (Spec R).Modules}
    (φ : M ⟶ N) {U V : (Spec R).Opens} (i : U ⟶ V) :
    ((affineSectionFunctor R U).map φ).hom.comp
        ((affineModulePresheaf M).map i.op).hom =
      ((affineModulePresheaf N).map i.op).hom.comp
        ((affineSectionFunctor R V).map φ).hom

def sectionKernelRestriction
    {R : CommRingCat.{u}} {M N : (Spec R).Modules}
    (φ : M ⟶ N) {U V : (Spec R).Opens} (i : U ⟶ V) :
    sectionKernel φ V ⟶ sectionKernel φ U

lemma kernelSectionIso_restriction
    {R : CommRingCat.{u}} {M N : (Spec R).Modules}
    {φ : M ⟶ N} (c : KernelFork φ) (hc : IsLimit c) {U V : (Spec R).Opens} (i : U ⟶ V) :
    (affineModulePresheaf c.pt).map i.op ≫ (kernelSectionIso c hc U).hom =
      (kernelSectionIso c hc V).hom ≫ sectionKernelRestriction φ i

theorem sectionKernelRestriction_localizes
    {R : CommRingCat.{u}} {M N : (Spec R).Modules}
    (φ : M ⟶ N) {U V : (Spec R).Opens} (i : U ⟶ V) (S : Submonoid R)
    (hM : IsLocalizedModule S ((affineModulePresheaf M).map i.op).hom)
    (hN : IsLocalizedModule S ((affineModulePresheaf N).map i.op).hom) :
    IsLocalizedModule S (sectionKernelRestriction φ i).hom

theorem kernelForkRestriction_localizes
    {R : CommRingCat.{u}} {M N : (Spec R).Modules}
    {φ : M ⟶ N} (c : KernelFork φ) (hc : IsLimit c)
    {U V : (Spec R).Opens} (i : U ⟶ V) (S : Submonoid R)
    (hM : IsLocalizedModule S ((affineModulePresheaf M).map i.op).hom)
    (hN : IsLocalizedModule S ((affineModulePresheaf N).map i.op).hom) :
    IsLocalizedModule S ((affineModulePresheaf c.pt).map i.op).hom

theorem isLocalizing_of_affineModulePresheaf
    {R : CommRingCat.{u}} (M : (Spec R).Modules)
    (h : ∀ r : R, IsLocalizedModule (Submonoid.powers r)
      ((affineModulePresheaf M).map (affineBasicOpenInclusion R r).op).hom) :
    IsLocalizing (modulesSpecToSheaf.obj M)

theorem affineModulePresheaf_localizes_of_isLocalizing
    {R : CommRingCat.{u}} (M : (Spec R).Modules)
    (hM : IsLocalizing (modulesSpecToSheaf.obj M)) (r : R) :
    IsLocalizedModule (Submonoid.powers r)
      ((affineModulePresheaf M).map (affineBasicOpenInclusion R r).op).hom

theorem isLocalizing_of_limitKernelFork
    {R : CommRingCat.{u}} {M N : (Spec R).Modules} {φ : M ⟶ N}
    (c : KernelFork φ) (hc : IsLimit c)
    (hM : IsLocalizing (modulesSpecToSheaf.obj M))
    (hN : IsLocalizing (modulesSpecToSheaf.obj N)) :
    IsLocalizing (modulesSpecToSheaf.obj c.pt)

theorem isLocalizing_kernel_toSpec
    {R : CommRingCat.{u}} {M N : (Spec R).Modules} (φ : M ⟶ N)
    (hM : IsLocalizing (modulesSpecToSheaf.obj M))
    (hN : IsLocalizing (modulesSpecToSheaf.obj N)) :
    IsLocalizing (modulesSpecToSheaf.obj (kernel φ))

theorem isQuasicoherent_kernel_toSpec
    {R : CommRingCat.{u}} {M N : (Spec R).Modules}
    [M.IsQuasicoherent] [N.IsQuasicoherent] (φ : M ⟶ N) :
    (kernel φ).IsQuasicoherent