Factors of a nonzero homogeneous element in an algebra without zero divisors graded by a `linear_ordered_cancel_add_comm_monoid` are also homogeneous.

factor_homogeneous.lean

import ring_theory.graded_algebra.basic

abbreviation saturated {α : Type*} [monoid_with_zero α] (s : submonoid α) : Prop :=
∀ ⦃a b : α⦄, a ∈ s → a ≠ 0 → b ∣ a → b ∈ s

variables {ι R A : Type*} [comm_semiring R] [semiring A] [algebra R A] 

namespace graded_algebra

variables [decidable_eq ι] [add_monoid ι] (𝒜 : ι → submodule R A) [graded_algebra 𝒜]
  [Π (i : ι) (x : ↥(𝒜 i)), decidable (x ≠ 0)]

lemma support_empty_iff {a : A} : support 𝒜 a = ∅ ↔ a = 0 :=
⟨ λ h0, by rw [← sum_support_decompose 𝒜 a, h0, finset.sum_empty],
  λ h0, by { ext i, simp [mem_support_iff, h0] } ⟩

lemma support_nonempty_iff {a : A} : (support 𝒜 a).nonempty ↔ a ≠ 0 :=
by rw [finset.nonempty_iff_ne_empty, ne.def, support_empty_iff]

lemma eq_of_mem_support_of_mem {a : A} {i j : ι} (ha : a ∈ 𝒜 i) (hi : j ∈ support 𝒜 a) : i = j :=
by { by_contra, rw mem_support_iff at hi, exact hi (decompose_of_mem_ne 𝒜 ha h) }

lemma support_subsingleton_iff_homogeneous {a : A} (h : a ≠ 0) :
  subsingleton (support 𝒜 a) ↔ set_like.is_homogeneous 𝒜 a :=
begin
  rw ← support_nonempty_iff 𝒜 at h,
  split,
  { rintro ⟨hs⟩, obtain ⟨i,hi⟩ := h,
    have : support 𝒜 a = {i},
    { ext j, rw finset.mem_singleton,
      exact ⟨ λ h, subtype.ext_iff.1 (hs ⟨j,h⟩ ⟨i,hi⟩),  λ h, h.symm ▸ hi ⟩ },
    use i, rw [← sum_support_decompose 𝒜 a, this, finset.sum_singleton], apply submodule.coe_mem },
  { rintro ⟨i,hi⟩, split, rintro ⟨j,hj⟩ ⟨k,hk⟩, rw [mem_support_iff, proj_apply] at hj hk,
    suffices : i = j ∧ i = k, { rw [subtype.mk_eq_mk, ← this.1, ← this.2] },
    by_contra, cases not_and_distrib.1 h with h h,
    { exact hj (decompose_of_mem_ne 𝒜 hi h) },
    { exact hk (decompose_of_mem_ne 𝒜 hi h) } },
end

lemma support_sum (f : Π i, 𝒜 i) (s : finset ι) : support 𝒜 (s.sum (λ i, f i)) ⊆ s :=
begin
  intros i hi, rw [mem_support_iff, (proj 𝒜 i).map_sum] at hi, by_contra, apply hi,
  apply finset.sum_eq_zero, intros j hj, apply decompose_of_mem_ne,
  { apply submodule.coe_mem },
  { intro he, rw he at hj, exact h hj },
end
--finsupp.support_finset_sum

lemma support_add (a b : A) : support 𝒜 (a + b) ⊆ support 𝒜 a ∪ support 𝒜 b := 
by { rw [support, map_add], exact dfinsupp.support_add }

lemma mem_support_add (a b : A) (i : ι) (ha : i ∈ support 𝒜 a) (hb : i ∉ support 𝒜 b) :
  i ∈ support 𝒜 (a + b) :=
by { rw mem_support_iff at ha hb ⊢, rw [map_add, not_ne_iff.1 hb], convert ha, simp }

lemma decompose_max [partial_order ι] (a : A) (m : ι) (ha : is_greatest ↑(support 𝒜 a) m) :
  ∃ b c : A, b ≠ 0 ∧ a = b + c ∧ b ∈ 𝒜 m ∧ ∀ i ∈ support 𝒜 c, i < m :=
begin
  use proj 𝒜 m a, split, split,
  { exact (mem_support_iff 𝒜 a m).1 ha.1 }, split,
  { rw (support 𝒜 a).add_sum_erase _ ha.1, exact (sum_support_decompose 𝒜 a).symm },
  split, { apply submodule.coe_mem },
  { intros i hi, have h := finset.mem_erase.1 (support_sum 𝒜 _ _ hi),
    exact lt_of_le_of_ne (ha.2 h.2) h.1 },
end

lemma decompose_min [partial_order ι] (a : A) (m : ι) (ha : is_least ↑(support 𝒜 a) m) :
  ∃ b c : A, b ≠ 0 ∧ a = b + c ∧ b ∈ 𝒜 m ∧ ∀ i ∈ support 𝒜 c, i > m :=
@decompose_max (order_dual ι) R A _ _ _ _ _ 𝒜 _ _ _ a m ha

open_locale pointwise
lemma support_mul (a b : A) : support 𝒜 (a * b) ⊆ support 𝒜 a + support 𝒜 b :=
begin
  nth_rewrite 0 ← sum_support_decompose 𝒜 a,
  nth_rewrite 0 ← sum_support_decompose 𝒜 b,
  rw finset.sum_mul_sum,
  intros i hi, rw [mem_support_iff, (proj 𝒜 i).map_sum] at hi, by_contra, apply hi,
  apply finset.sum_eq_zero, intros j hj, apply decompose_of_mem_ne,
  { apply set_like.graded_monoid.mul_mem; apply submodule.coe_mem },
  { intro he, apply h, rw finset.mem_add, rw finset.mem_product at hj,
    exact ⟨j.1,j.2,hj.1,hj.2,he⟩ },
end

end graded_algebra

open graded_algebra

section

variables [decidable_eq ι] [ordered_cancel_add_comm_monoid ι] (𝒜 : ι → submodule R A) [graded_algebra 𝒜]
  [Π (i : ι) (x : ↥(𝒜 i)), decidable (x ≠ 0)]

lemma mul_is_greatest_support [no_zero_divisors A] (a b : A) {ma mb : ι}
  (ha : is_greatest ↑(support 𝒜 a) ma) (hb : is_greatest ↑(support 𝒜 b) mb) :
  is_greatest ↑(support 𝒜 (a * b)) (ma + mb) :=
begin
  split,
  { obtain ⟨am,ar,ha0,rfl,ham,har⟩ := decompose_max 𝒜 a ma ha,
    obtain ⟨bm,br,hb0,rfl,hbm,hbr⟩ := decompose_max 𝒜 b mb hb,
    rw [add_mul, mul_add, add_assoc], apply mem_support_add,
    { rw [mem_support_iff, proj_apply, decompose_of_mem_same],
      { exact mul_ne_zero ha0 hb0 }, { exact set_like.graded_monoid.mul_mem ham hbm } },
    { intro h, obtain (h'|h') := finset.mem_union.1 (support_add 𝒜 _ _ h),
      { obtain ⟨i₁,i₂,h₁,h₂,h₃⟩ := finset.mem_add.1 (support_mul 𝒜 _ _ h'),
        rw eq_of_mem_support_of_mem 𝒜 ham h₁ at h₃,
        exact ne_of_lt (hbr i₂ h₂) (add_left_cancel h₃) },
      { obtain ⟨i₁,i₂,h₁,h₂,h₃⟩ := finset.mem_add.1 (support_mul 𝒜 _ _ h'),
        exact ne_of_lt (add_lt_add_of_lt_of_le (har i₁ h₁) (hb.2 h₂)) h₃ } } },
  { intros i hi, obtain ⟨i₁,i₂,h₁,h₂,rfl⟩ := finset.mem_add.1 (support_mul 𝒜 a b hi),
    exact add_le_add (ha.2 h₁) (hb.2 h₂) },
end

lemma mul_is_least_support [no_zero_divisors A] (a b : A) {ma mb : ι}
  (ha : is_least ↑(support 𝒜 a) ma) (hb : is_least ↑(support 𝒜 b) mb) :
  is_least ↑(support 𝒜 (a * b)) (ma + mb) :=
@mul_is_greatest_support (order_dual ι) R A _ _ _ _ _ 𝒜 _ _ _ a b _ _ ha hb

end

variables [linear_ordered_cancel_add_comm_monoid ι] (𝒜 : ι → submodule R A) [graded_algebra 𝒜]
  [Π (i : ι) (x : ↥(𝒜 i)), decidable (x ≠ 0)]

lemma homogeneous_saturated [no_zero_divisors A] : saturated (set_like.homogeneous_submonoid 𝒜) :=
begin
  rintros _ b ha hn0 ⟨c,rfl⟩,
  let bsupp := support 𝒜 b, let csupp := support 𝒜 c,
  have hb0 : b ≠ 0 := λ h, hn0 $ by simp [h],
  have hb : bsupp.nonempty := (support_nonempty_iff 𝒜).2 hb0,
  have hc : csupp.nonempty := (support_nonempty_iff 𝒜).2 (λ h, hn0 $ by simp [h]),
  let bmax := bsupp.max' hb, let bmin := bsupp.min' hb,
  let cmax := csupp.max' hc, let cmin := csupp.min' hc,
  have smax : bmax + cmax ∈ support 𝒜 (b * c) :=
    (mul_is_greatest_support 𝒜 b c (bsupp.is_greatest_max' hb) (csupp.is_greatest_max' hc)).1,
  have smin : bmin + cmin ∈ support 𝒜 (b * c) :=
    (mul_is_least_support 𝒜 b c (bsupp.is_least_min' hb) (csupp.is_least_min' hc)).1,
  obtain ⟨ha⟩ := (support_subsingleton_iff_homogeneous 𝒜 hn0).2 ha,
  apply (support_subsingleton_iff_homogeneous 𝒜 hb0).1, split, rintro ⟨i₁,h₁⟩ ⟨i₂,h₂⟩,
  suffices he : bmin = bmax,
  { ext, exact ((he.substr $ bsupp.le_max' i₁ h₁).trans $ bsupp.min'_le i₂ h₂).antisymm
      ((he.substr $ bsupp.le_max' i₂ h₂).trans $ bsupp.min'_le i₁ h₁) },
  exact ((add_eq_add_iff_eq_and_eq (bsupp.le_max' _ $ bsupp.min'_mem _)
    (csupp.le_max' _ $ csupp.min'_mem _)).1 $ subtype.ext_iff.1 (ha ⟨_,smin⟩ ⟨_,smax⟩)).1,
end