Graded rings and the irrelevant ideal

graded-rings.lean

import data.finsupp
import data.dfinsupp
import data.polynomial
import algebra.module
import algebra.direct_sum
import tactic.equiv_rw

universes u v
variables (M : Type v) (α : Type u)
variables [add_monoid M] [decidable_eq M]

section graded_abelian_group

class graded_abelian_group [add_comm_group α] :=
(piece : M → Type u) (group : ∀ m : M, add_comm_group (piece m))
(iso : α ≃+ direct_sum M piece)

open graded_abelian_group

variables [add_comm_group α] [graded_abelian_group M α]

instance group_instances (m : M) : add_comm_group (piece α m) := group m

def embed_piece {m : M} (r : piece α m) : α :=
add_equiv.symm iso (direct_sum.of (piece α) m r)

def grade (m : M) : set α := λ a, ∃ s : piece α m, a = embed_piece M α s

lemma embed_piece_grade {m : M} (r : piece α m) : embed_piece M α r ∈ grade M α m := by use r

def embed_piece' {m : M} (r : piece α m) : grade M α m := ⟨embed_piece M α r, embed_piece_grade M α r⟩

def homogeneous_element (r : α) := ∃ m : M, r ∈ grade M α m

def proj_on_degree (m : M) : α →+ piece α m :=
{ to_fun := λ r, iso r m,
  map_zero' := by { rw add_equiv.map_zero iso, refl },
  map_add' := by { intros x y, rw add_equiv.map_add iso x y, simp }
 }

def proj_on_degree' {m : M} (r : grade M α m) : piece α m :=
proj_on_degree M α m r

def binary_op_respects_grading (β γ : Type*)
[add_comm_group β] [add_comm_group γ] [graded_abelian_group M β] [graded_abelian_group M γ]
(op : α → β → γ) :=
∀ (m m' : M) (r : grade M α m) (r' : grade M β m'),
  op r r' ∈ grade M γ (m + m')

-- todo: morphisms, quotients

end graded_abelian_group

section graded_ring

variable [ring α]

class graded_ring extends graded_abelian_group M α :=
(mul_respects_grading : binary_op_respects_grading M α α α (λ x y, x * y))

open graded_abelian_group

def mul_on_pieces [graded_ring M α] {m m' : M} : piece α m -> piece α m' -> piece α (m + m') :=
λ r r', let H := graded_ring.mul_respects_grading m m' (embed_piece' M α r) (embed_piece' M α r')
  in proj_on_degree' M α ⟨_, H⟩

lemma mul_on_pieces' [graded_ring M α] {m m' : M} (r : piece α m) (r' : piece α m') :
(embed_piece M α r) * (embed_piece M α r') = embed_piece M α (mul_on_pieces M α r r') :=
begin
sorry
end

end graded_ring

section homogeneous_module

variables [ring α] [graded_ring M α]

class homogeneous_module (m : Type u) [add_comm_group m] [module α m] [graded_abelian_group M m] :=
(mul_respects_grading : binary_op_respects_grading M α m m (λ x y, x • y))

end homogeneous_module

instance graded_ring.to_module [ring α] [graded_ring M α] : homogeneous_module M α α :=
{ mul_respects_grading := graded_ring.mul_respects_grading }

section homogeneous_submodule

variables [ring α] [graded_ring M α]
variables (N : Type u) [add_comm_group N] [module α N] [graded_abelian_group M N] [homogeneous_module M α N]

-- a submodule is homogeneous if x ∈ N => x^(m) ∈ N
structure homogeneous_submodule extends submodule α N :=
(has_hom_parts : Π m n, n ∈ carrier → embed_piece M N (proj_on_degree M N m n) ∈ carrier)

def homogeneous_ideal [decidable_eq α] := homogeneous_submodule M α α

end homogeneous_submodule

section irrelevant_ideal

variables [ring α] [graded_ring ℕ α] [decidable_eq α]

open graded_abelian_group

def smul_mem_helper : ∀ (c : α) {x : α}, iso x 0 = 0 → iso (c * x) 0 = 0 :=
begin
  -- massage the goal
  equiv_rw add_equiv.to_equiv (@iso ℕ α _ _ _ _), intros r r',
  have H : ∀ x, ((id iso.to_equiv).symm) x = iso.symm x, { intro x, refl }, rw [H r, H r'], clear H,
   -- is there an easier way to the previous two lines?
  rw add_equiv.apply_symm_apply,

  apply dfinsupp.induction r',
    -- base case is essentially trivial, is there a tactic that can deal with this?
    { rw [add_equiv.map_zero (add_equiv.symm iso), mul_zero, add_equiv.map_zero iso], tauto },

  intros d b f Hfd Hb Hrf H,

  -- need f 0 = 0 to remove f from H and as an assumption for Hrf
  have Hf0 : f 0 = 0, { simp at H, split_ifs at H, rw h at Hfd, assumption, simp at H, assumption },
  simp [Hf0] at H,

  -- need this for later
  have Hd : d ≠ 0, { intro H', cases d, simp at H, apply Hb H, injection H' },

  -- we can now get rid of f in the goal
  simp [add_equiv.map_add (add_equiv.symm iso), left_distrib, add_equiv.map_add iso, Hrf Hf0],
  clear' f Hfd Hb Hrf Hf0 H,

  apply dfinsupp.induction r,
    -- almost the same base case
    { rw [add_equiv.map_zero (add_equiv.symm iso), zero_mul, add_equiv.map_zero iso], tauto },

  intros d' b' f' Hf'd' Hb' Hf'b, clear Hf'd' Hb', -- don't need Hf'd' and Hb'
  -- this time we can get rid of f' right away
  simp [add_equiv.map_add (add_equiv.symm iso), right_distrib, add_equiv.map_add iso, Hf'b],
  clear Hf'b f',

  -- rewrite the product as a single element of degree d' + d
  have H := mul_on_pieces' ℕ α b' b, simp [embed_piece, direct_sum.of] at H, rw H, clear H,
  rw [add_equiv.apply_symm_apply],
  -- conclude because d' + d ≠ 0
  simp, split_ifs, { exfalso, apply Hd, tauto }, refl
end

def irrelevant_ideal : homogeneous_ideal ℕ α :=
{ carrier := λ x, proj_on_degree ℕ α 0 x = 0,
  zero_mem' := by simp [has_mem.mem, set.mem],
  add_mem' := by { simp [has_mem.mem, set.mem], intros x y Hx Hy, simp [Hx, Hy] },
  smul_mem' := by { simp [proj_on_degree], apply smul_mem_helper },
  has_hom_parts :=
begin
  simp [has_mem.mem, set.mem, proj_on_degree, embed_piece], intros n r H,
  cases n, { rw H, refl }, refl
end }

end irrelevant_ideal