text:
import algebra.category.Module.abelian
import sheaves_of_modules.defs
import algebraic_geometry.AffineScheme
import algebra.module.localized_module

/-

# Construction of sheaf of modules on Spec(R) associated to a module

-/

-- last week we defined sheaves of modules on a sheaf of rings
-- and gave them the structure of a category
-- this week let's make an example of a sheaf of modules

-- remark: there's a Lean repository where I push stuff
-- git@github.com:ImperialCollegeLondon/tcc-lean-alg-geom-2022.git

-- `leanproject get ImperialCollegeLondon/tcc-lean-alg-geom-2022`
-- should get it you

-- Let R be a ring and let M be an R-module

-- this says "let R be a commutative ring which is also a set"
variables {R : Type} [comm_ring R] -- zero means "it's a set"
-- let M be a module over R which is also a set
variable (M : Module.{0} R)

-- goal: to make a sheaf of modules over Spec(R)

-- two distinct (as far as I know) constructions.
/-

-- (1) (Stacks project, EGA) : If U=D(f) is a basic open subset
-- then define 𝓜(U) := M[1/f]
-- Now use some formal nonsense to extend to all open subsets

Problem with (1) is that can have U=D(f)=D(g) but strictly speaking
M[1/f] ≠ M[1/g]

  (2) (Hartshorne): define on all open sets at once:
  𝓜(U) := {f : U → disjoint union of M_P such that
   (a) f(P) ∈ M_P (i.e. f is a dependent function: f : Π (P : U), M_P )
   (b) f is "locally a fraction" i.e. for all P there exists some nhd V
   of P and elements m ∈ M and r ∈ R non-vanishing on V such that
   f(Q)=m/r for all Q in V

   Hartshorne defines structure sheaf on Spec(R) in this way
   and mathlib defines it like this too.
  }

We're going to go for (2) becuase it avoids "canonical isomorphism"
  nonsense which is hard to make rigorous in Lean's type theory

NB variant (1') : If U is a basic open then you can define
 𝓜(U)=M[1/S] where S is all the elements of R which are nonvanishing on U
 and this avoids the problem; it's much more functorial and this
 is what we did in the initial schemes project.

-/

-- In the below we just copy what they do for rings

-- apparently this API is missing from mathlib
def prime_spectrum.prime_compl (Q : prime_spectrum R) : submonoid R := Q.as_ideal.prime_compl

open algebraic_geometry category_theory

namespace Module

/--
`M.localizations P` : The type family over `(P : prime_spectrum.Top R)` consisting of the localization
`M_P` of the module `R`-module `M` over each point.
-/
@[reducible, derive add_comm_group]
def localizations (P : prime_spectrum R) : Type := localized_module (P.prime_compl) M

-- Jujian says
-- * Redefine `localization` for monoids and rings to coincide with `localized_module`.
-- is a project

/-
protected abbreviation localization.at_prime := localization I.prime_compl
-/

/-- Let type class inference see through the `M.localizations` definition and
  recognise the `R_P`-module structure on `M.localizations P := M_P` -/
instance (P : prime_spectrum R) : module (structure_sheaf.localizations R P) (M.localizations P) :=
localized_module.is_module -- definitional equality.

/-
Then we'll define a predicate called "is_locally_fraction"
-/

open topological_space

/--
The predicate saying that a dependent function on an open `U` is realised as a fixed fraction
`m / s` in each of the stalks (which are localizations of a fixed module at various prime ideals).
-/
def is_fraction {U : opens (prime_spectrum R)} (f : Π (P : U), M.localizations P) : Prop :=
∃ (m : M) (s : R), ∀ P : U, ∃ (hs : s ∈ (P.1 : prime_spectrum R).prime_compl),
  f P = localized_module.mk m ⟨s, hs⟩

open Top

/--
The predicate `is_fraction` is "prelocal",
in the sense that if it holds on `U` it holds on any open subset `V` of `U`.
-/
def is_fraction_prelocal : prelocal_predicate (id (M.localizations) : (prime_spectrum.Top R : Type) → Type) :=
{ pred := λ U f, M.is_fraction f,
  res := by { rintro V U i f ⟨r, s, w⟩, exact ⟨r, s, λ x, w (i x)⟩ } }

/-- A dependent section f : Π (P : U), M_P is locally a fraction
if U has an open cover such that the restriction of f to the cover
is a fraction m/s -/
def is_locally_fraction : local_predicate (id (M.localizations): (prime_spectrum.Top R : Type) → Type) :=
(M.is_fraction_prelocal).sheafify

/-
Then we'll make a sheaf of tyhpes
-/
/--
The sheaf of modules associated to M (valued in `Type`, not yet `Ab`) is the subsheaf consisting of
functions satisfying `is_locally_fraction`.
-/
def sheaf_in_Type : sheaf (Type) (prime_spectrum.Top R):=
subsheaf_to_Types (M.is_locally_fraction)

open opposite

/-
Then we'll show that each of these types is an abelian group
-/

def Spec.structure_sheaf' (R : Type) [comm_ring R] : sheaf CommRing (bundled.mk (prime_spectrum R) : Top.{0}) :=
Spec.structure_sheaf R

noncomputable def algebraic_geometry.structure_sheaf.to_stalk' (R : Type*) [comm_ring R]
  (x : prime_spectrum R) :
  CommRing.of R ⟶ (Spec.structure_sheaf R).presheaf.stalk x :=
algebraic_geometry.structure_sheaf.to_stalk R x

--#print algebraic_geometry.structure_sheaf.to_stalk
-- : Π (R : Type u) [_inst_1 : comm_ring R] (x : ↥(prime_spectrum.Top R)), CommRing.of R ⟶ (structure_sheaf R).presheaf.stalk x

--#check comm_ring
--#check CommRing.comm_ring

--set_option pp.all true
instance sections_module (U : (opens (prime_spectrum R))ᵒᵖ) :
  module ((Spec.structure_sheaf' R).val.obj U) (Π P : unop U, M.localizations P) :=
{ smul := λ f m P, (f.1 P) • m P,
--begin
--  change ↥((Spec.structure_sheaf' R).val.obj U) at f,
--  let moo : _ →+* _ := algebraic_geometry.structure_sheaf.to_stalk' R P,
  --simp at moo,
  -- exact (f.stalk P) • m P,
--  sorry,
--end,
  one_smul := begin
    intro f,
    ext,
    simp,
--    norm_cast,
--    simp only [subtype.val_eq_coe],
    let foo : structure_sheaf.localizations R (x.1 : (prime_spectrum R)) := 1,
    --change foo • f x = f x,--    simp,
    delta has_one.one,
    sorry,
  end,
  mul_smul := sorry,
  smul_zero := sorry,
  smul_add := sorry,
  add_smul := sorry,
  zero_smul := sorry }

#exit
/--
The functions satisfying `is_locally_fraction` form a subgroup.
-/
def sections_submodule' (U : (opens (prime_spectrum R))ᵒᵖ) :
  submodule ((structure_presheaf_in_CommRing R).obj U) (Π P : unop U, M.localizations P) :=
{ carrier := { f | (M.is_locally_fraction).pred f },
  zero_mem' :=
  begin
    refine λ x, ⟨unop U, x.2, 𝟙 _, 0, 1, λ y, ⟨_, _⟩⟩,
    { change (1 : R) ∉ prime_spectrum.as_ideal y.val,
      rw ←ideal.ne_top_iff_one, exact y.1.is_prime.1, },
    { simp, },
  end,
  -- neg_mem' :=
  -- begin
  --   intros a ha x,
  --   rcases ha x with ⟨V, hxV, i, m, s, hm⟩,
  --   refine ⟨V, hxV, i, -m, s, _⟩,
  --   intro y,
  --   rcases hm y with ⟨hs, w⟩,
  --   use hs,
  --   dsimp only at w ⊢,
  --   simp only [w, pi.neg_apply],
  --   apply localized_module.mk_neg,
  -- end,
  add_mem' :=
  begin
    intros a b ha hb x,
    rcases ha x with ⟨Va, ma, ia, ra, sa, wa⟩,
    rcases hb x with ⟨Vb, mb, ib, rb, sb, wb⟩,
    refine ⟨Va ⊓ Vb, ⟨ma, mb⟩, opens.inf_le_left _ _ ≫ ia, sb • ra + sa • rb, sa * sb, _⟩,
    intro y,
    rcases wa (opens.inf_le_left _ _ y) with ⟨nma, wa'⟩,
    rcases wb (opens.inf_le_right _ _ y) with ⟨nmb, wb'⟩,
    fsplit,
    { intro H, cases y.1.is_prime.mem_or_mem H; contradiction, },
    dsimp only at wa' wb' ⊢,
    change a (ia ((Va.inf_le_left Vb) y)) + b (ib ((Va.inf_le_right Vb) y)) = _,
    rw [wa', wb'],
    refl,
  end,
  smul_mem' :=
  begin
    sorry
  end, }

instance add_comm_group_sheaf_in_Type_obj (U : (opens (prime_spectrum.Top R))ᵒᵖ) :
  add_comm_group ((M.sheaf_in_Type).1.obj U) :=
(M.sections_submodule' U).to_add_subgroup.to_add_comm_group

instance module_sheaf_in_Type_obj (U : (opens (prime_spectrum.Top R))ᵒᵖ) :
  module ((structure_presheaf_in_CommRing R).obj U) ((M.sheaf_in_Type).1.obj U) :=
submodule_class.to_module (M.sections_submodule' U)

/-
Then we'll make a presheaf of abelian groups
-/

/--
The presheaf, valued in `Ab`, constructed by dressing up the `Type` valued
presheaf associated to an R-module.
-/
@[simps]
def presheaf_in_Ab : presheaf Ab (prime_spectrum.Top R) :=
{ obj := λ U, AddCommGroup.of ((M.sheaf_in_Type).1.obj U),
  map := λ U V i,
  { to_fun := ((M.sheaf_in_Type).1.map i),
    map_zero' := rfl,
    map_add' := λ x y, rfl, }, }

/--
Some glue, verifying that that structure presheaf valued in `CommRing` agrees
with the `Type` valued structure presheaf.
-/
def presheaf_comp_forget :
  M.presheaf_in_Ab ⋙ (category_theory.forget Ab) ≅ (M.sheaf_in_Type).1 :=
nat_iso.of_components
  (λ U, iso.refl _)
  (by tidy)

open Top.presheaf

/--
The structure sheaf on $Spec R$, valued in `CommRing`.

This is provided as a bundled `SheafedSpace` as `Spec.SheafedSpace R` later.
-/
def sheaf : sheaf Ab (prime_spectrum.Top R) :=
⟨M.presheaf_in_Ab,
  -- We check the sheaf condition under `forget CommRing`.
  (is_sheaf_iff_is_sheaf_comp _ _).mpr
    (is_sheaf_of_iso (M.presheaf_comp_forget).symm
      (M.sheaf_in_Type).cond)⟩

/-
and then we'll beef it up into a sheaf of modules
-/

--#check Scheme

def sheaf_of_modules: SHEAF_OF_MODULES (Spec.to_LocallyRingedSpace.obj (op R)).to_SheafedSpace :=
{ ab_sheaf := M.sheaf,
  module_structure := M.module_sheaf_in_Type_obj,
  compatibility_bit := sorry
}

end Module

author: ImperialCollegeLondon


text:
/-
Copyright (c) 2017 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl, Yury Kudryashov

! This file was ported from Lean 3 source module data.finsupp.antidiagonal
! leanprover-community/mathlib commit 0a0ec35061ed9960bf0e7ffb0335f44447b58977
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Finsupp.Multiset
import Mathlib.Data.Multiset.Antidiagonal

/-!
# The `Finsupp` counterpart of `Multiset.antidiagonal`.

The antidiagonal of `s : α →₀ ℕ` consists of
all pairs `(t₁, t₂) : (α →₀ ℕ) × (α →₀ ℕ)` such that `t₁ + t₂ = s`.
-/

noncomputable section

open Classical BigOperators

namespace Finsupp

open Finset

universe u

variable {α : Type u}

/-- The `Finsupp` counterpart of `Multiset.antidiagonal`: the antidiagonal of
`s : α →₀ ℕ` consists of all pairs `(t₁, t₂) : (α →₀ ℕ) × (α →₀ ℕ)` such that `t₁ + t₂ = s`.
The finitely supported function `antidiagonal s` is equal to the multiplicities of these pairs. -/
def antidiagonal' (f : α →₀ ℕ) : (α →₀ ℕ) × (α →₀ ℕ) →₀ ℕ :=
  Multiset.toFinsupp
    ((Finsupp.toMultiset f).antidiagonal.map (Prod.map Multiset.toFinsupp Multiset.toFinsupp))
#align finsupp.antidiagonal' Finsupp.antidiagonal'

/-- The antidiagonal of `s : α →₀ ℕ` is the finset of all pairs `(t₁, t₂) : (α →₀ ℕ) × (α →₀ ℕ)`
such that `t₁ + t₂ = s`. -/
def antidiagonal (f : α →₀ ℕ) : Finset ((α →₀ ℕ) × (α →₀ ℕ)) := f.antidiagonal'.support
#align finsupp.antidiagonal Finsupp.antidiagonal

@[simp]
theorem mem_antidiagonal {f : α →₀ ℕ} {p : (α →₀ ℕ) × (α →₀ ℕ)} :
    p ∈ antidiagonal f ↔ p.1 + p.2 = f := by
  rcases p with ⟨p₁, p₂⟩
  simp [antidiagonal, antidiagonal', ← and_assoc, ← Finsupp.toMultiset.apply_eq_iff_eq]
#align finsupp.mem_antidiagonal Finsupp.mem_antidiagonal

theorem swap_mem_antidiagonal {n : α →₀ ℕ} {f : (α →₀ ℕ) × (α →₀ ℕ)} :
    f.swap ∈ antidiagonal n ↔ f ∈ antidiagonal n := by
  simp only [mem_antidiagonal, add_comm, Prod.swap]
#align finsupp.swap_mem_antidiagonal Finsupp.swap_mem_antidiagonal

theorem antidiagonal_filter_fst_eq (f g : α →₀ ℕ)
    [D : ∀ p : (α →₀ ℕ) × (α →₀ ℕ), Decidable (p.1 = g)] :
    ((antidiagonal f).filter fun p ↦ p.1 = g) = if g ≤ f then {(g, f - g)} else ∅ := by
  ext ⟨a, b⟩
  suffices a = g → (a + b = f ↔ g ≤ f ∧ b = f - g) by
    have h₁ : (if g ≤ f then a = g ∧ b = f - g else False) ↔ g ≤ f ∧ a = g ∧ b = f - g := by
      by_cases h : g ≤ f <;> simp [h]
    simpa [apply_ite (fun f ↦ (a, b) ∈ f), mem_filter, mem_antidiagonal, mem_singleton,
      Prod.mk.inj_iff, h₁, ← and_assoc, @and_right_comm _ (a = _), and_congr_left_iff]
  rintro rfl
  constructor
  · rintro rfl
    exact ⟨le_add_right le_rfl, (add_tsub_cancel_left _ _).symm⟩
  · rintro ⟨h, rfl⟩
    exact add_tsub_cancel_of_le h
#align finsupp.antidiagonal_filter_fst_eq Finsupp.antidiagonal_filter_fst_eq

theorem antidiagonal_filter_snd_eq (f g : α →₀ ℕ)
    [D : ∀ p : (α →₀ ℕ) × (α →₀ ℕ), Decidable (p.2 = g)] :
    ((antidiagonal f).filter fun p ↦ p.2 = g) = if g ≤ f then {(f - g, g)} else ∅ := by
  ext ⟨a, b⟩
  suffices b = g → (a + b = f ↔ g ≤ f ∧ a = f - g) by
    have h₁ : (if g ≤ f then a = f - g ∧ b = g else False) ↔ g ≤ f ∧ a = f - g ∧ b = g := by
      by_cases h : g ≤ f <;> simp [h]
    simpa [apply_ite (fun f ↦ (a, b) ∈ f), mem_filter, mem_antidiagonal, mem_singleton,
      Prod.mk.inj_iff, h₁, ← and_assoc, and_congr_left_iff]
  rintro rfl
  constructor
  · rintro rfl
    exact ⟨le_add_left le_rfl, (add_tsub_cancel_right _ _).symm⟩
  · rintro ⟨h, rfl⟩
    exact tsub_add_cancel_of_le h
#align finsupp.antidiagonal_filter_snd_eq Finsupp.antidiagonal_filter_snd_eq

@[simp]
theorem antidiagonal_zero : antidiagonal (0 : α →₀ ℕ) = singleton (0, 0) := by
  rw [antidiagonal, antidiagonal', Multiset.toFinsupp_support]; rfl
#align finsupp.antidiagonal_zero Finsupp.antidiagonal_zero

@[to_additive]
theorem prod_antidiagonal_swap {M : Type _} [CommMonoid M] (n : α →₀ ℕ)
    (f : (α →₀ ℕ) → (α →₀ ℕ) → M) :
    (∏ p in antidiagonal n, f p.1 p.2) = ∏ p in antidiagonal n, f p.2 p.1 :=
  Finset.prod_bij (fun p _hp ↦ p.swap) (fun _p ↦ swap_mem_antidiagonal.2) (fun _p _hp ↦ rfl)
    (fun _p₁ _p₂ _ _ h ↦ Prod.swap_injective h) fun p hp ↦
    ⟨p.swap, swap_mem_antidiagonal.2 hp, p.swap_swap.symm⟩
#align finsupp.prod_antidiagonal_swap Finsupp.prod_antidiagonal_swap
#align finsupp.sum_antidiagonal_swap Finsupp.sum_antidiagonal_swap

end Finsupp

author: leanprover-community