feat(algebra/direct_sum/decomposition): add decompositions into a direct sum (#14626)

This is a constructive version of `direct_sum.is_internal`, and generalizes the existing `graded_algebra`.

The main user-facing changes are:
* `graded_algebra.decompose` is now spelt `direct_sum.decompose_alg_hom`
* The simp normal form of decomposition is now `direct_sum.decompose`.
* `graded_algebra.support 𝒜 x` is now spelt `(decompose 𝒜 x).support`
* `left_inv` and `right_inv` has swapped, now with meaning "the decomposition is the (left|right) inverse of the canonical map" rather than the other way around

To keep this from growing even larger, I've left `graded_algebra.proj` alone for a future refactor.



Co-authored-by: Jujian Zhang <jujian.zhang1998@outlook.com>

Author: eric-wieser

counterexamples/homogeneous_prime_not_prime.lean

@@ -83,15 +83,14 @@ def grading.decompose : (R × R) →+ direct_sum two (λ i, grading R i) :=
   map_zero' := by { ext1 (_|⟨⟨⟩⟩); refl },
   map_add' := begin
     rintros ⟨a1, b1⟩ ⟨a2, b2⟩,
-    have H : b1 + b2 - (a1 + a2) = b1 - a1 + (b2 - a2), by abel,
-    ext (_|⟨⟨⟩⟩) : 3;
-    simp only [prod.fst_add, prod.snd_add, add_apply, submodule.coe_add, prod.mk_add_mk, H];
-    repeat { erw of_eq_same }; repeat { erw of_eq_of_ne }; try { apply option.no_confusion };
-    dsimp; simp only [zero_add, add_zero]; refl,
+    rw [add_add_add_comm, ←map_add, ←map_add],
+    dsimp only [prod.mk_add_mk],
+    simp_rw [add_sub_add_comm],
+    congr,
   end }
 
-lemma grading.left_inv :
-  function.left_inverse grading.decompose (coe_linear_map (grading R)) := λ zz,
+lemma grading.right_inv :
+  function.right_inverse (coe_linear_map (grading R)) grading.decompose := λ zz,
 begin
   induction zz using direct_sum.induction_on with i zz d1 d2 ih1 ih2,
   { simp only [map_zero],},
@@ -100,8 +99,8 @@ begin
   { simp only [map_add, ih1, ih2], },
 end
 
-lemma grading.right_inv :
-  function.right_inverse grading.decompose (coe_linear_map (grading R)) := λ zz,
+lemma grading.left_inv :
+  function.left_inverse (coe_linear_map (grading R)) grading.decompose := λ zz,
 begin
   cases zz with a b,
   unfold grading.decompose,

src/algebra/direct_sum/decomposition.lean

@@ -0,0 +1,180 @@
+/-
+Copyright (c) 2022 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser, Jujian Zhang
+-/
+import algebra.direct_sum.module
+import algebra.module.submodule.basic
+
+/-!
+# Decompositions of additive monoids, groups, and modules into direct sums
+
+## Main definitions
+
+* `direct_sum.decomposition ℳ`: A typeclass to provide a constructive decomposition from
+  an additive monoid `M` into a family of additive submonoids `ℳ`
+* `direct_sum.decompose ℳ`: The canonical equivalence provided by the above typeclass
+
+
+## Main statements
+
+* `direct_sum.decomposition.is_internal`: The link to `direct_sum.is_internal`.
+
+## Implementation details
+
+As we want to talk about different types of decomposition (additive monoids, modules, rings, ...),
+we choose to avoid heavily bundling `direct_sum.decompose`, instead making copies for the
+`add_equiv`, `linear_equiv`, etc. This means we have to repeat statements that follow from these
+bundled homs, but means we don't have to repeat statements for different types of decomposition.
+-/
+
+
+variables {ι R M σ : Type*}
+open_locale direct_sum big_operators
+namespace direct_sum
+
+section add_comm_monoid
+variables [decidable_eq ι] [add_comm_monoid M]
+variables [set_like σ M] [add_submonoid_class σ M] (ℳ : ι → σ)
+
+/-- A decomposition is an equivalence between an additive monoid `M` and a direct sum of additive
+submonoids `ℳ i` of that `M`, such that the "recomposition" is canonical. This definition also
+works for additive groups and modules.
+
+This is a version of `direct_sum.is_internal` which comes with a constructive inverse to the
+canonical "recomposition" rather than just a proof that the "recomposition" is bijective. -/
+class decomposition :=
+(decompose' : M → ⨁ i, ℳ i)
+(left_inv : function.left_inverse (direct_sum.coe_add_monoid_hom ℳ) decompose' )
+(right_inv : function.right_inverse (direct_sum.coe_add_monoid_hom ℳ) decompose')
+
+include M
+
+/-- `direct_sum.decomposition` instances, while carrying data, are always equal. -/
+instance : subsingleton (decomposition ℳ) :=
+⟨λ x y, begin
+  cases x with x xl xr,
+  cases y with y yl yr,
+  congr',
+  exact function.left_inverse.eq_right_inverse xr yl,
+end⟩
+
+variables [decomposition ℳ]
+
+protected lemma decomposition.is_internal : direct_sum.is_internal ℳ :=
+⟨decomposition.right_inv.injective, decomposition.left_inv.surjective⟩
+
+/-- If `M` is graded by `ι` with degree `i` component `ℳ i`, then it is isomorphic as
+to a direct sum of components. This is the canonical spelling of the `decompose'` field. -/
+def decompose : M ≃ ⨁ i, ℳ i :=
+{ to_fun := decomposition.decompose',
+  inv_fun := direct_sum.coe_add_monoid_hom ℳ,
+  left_inv := decomposition.left_inv,
+  right_inv := decomposition.right_inv }
+
+@[simp] lemma decomposition.decompose'_eq : decomposition.decompose' = decompose ℳ := rfl
+
+@[simp] lemma decompose_symm_of {i : ι} (x : ℳ i) :
+  (decompose ℳ).symm (direct_sum.of _ i x) = x :=
+direct_sum.coe_add_monoid_hom_of ℳ _ _
+
+@[simp] lemma decompose_coe {i : ι} (x : ℳ i) :
+  decompose ℳ (x : M) = direct_sum.of _ i x :=
+by rw [←decompose_symm_of, equiv.apply_symm_apply]
+
+lemma decompose_of_mem {x : M} {i : ι} (hx : x ∈ ℳ i) :
+  decompose ℳ x = direct_sum.of (λ i, ℳ i) i ⟨x, hx⟩ :=
+decompose_coe _ ⟨x, hx⟩
+
+lemma decompose_of_mem_same {x : M} {i : ι} (hx : x ∈ ℳ i) :
+  (decompose ℳ x i : M) = x :=
+by rw [decompose_of_mem _ hx, direct_sum.of_eq_same, subtype.coe_mk]
+
+lemma decompose_of_mem_ne {x : M} {i j : ι} (hx : x ∈ ℳ i) (hij : i ≠ j):
+  (decompose ℳ x j : M) = 0 :=
+by rw [decompose_of_mem _ hx, direct_sum.of_eq_of_ne _ _ _ _ hij,
+  add_submonoid_class.coe_zero]
+
+/-- If `M` is graded by `ι` with degree `i` component `ℳ i`, then it is isomorphic as
+an additive monoid to a direct sum of components. -/
+@[simps {fully_applied := ff}]
+def decompose_add_equiv : M ≃+ ⨁ i, ℳ i := add_equiv.symm
+{ map_add' := map_add (direct_sum.coe_add_monoid_hom ℳ),
+  ..(decompose ℳ).symm }
+
+@[simp] lemma decompose_zero : decompose ℳ (0 : M) = 0 := map_zero (decompose_add_equiv ℳ)
+@[simp] lemma decompose_symm_zero : (decompose ℳ).symm 0 = (0 : M) :=
+map_zero (decompose_add_equiv ℳ).symm
+
+@[simp] lemma decompose_add (x y : M) : decompose ℳ (x + y) = decompose ℳ x + decompose ℳ y :=
+map_add (decompose_add_equiv ℳ) x y
+@[simp] lemma decompose_symm_add (x y : ⨁ i, ℳ i) :
+  (decompose ℳ).symm (x + y) = (decompose ℳ).symm x + (decompose ℳ).symm y :=
+map_add (decompose_add_equiv ℳ).symm x y
+
+@[simp] lemma decompose_sum {ι'} (s : finset ι') (f : ι' → M) :
+  decompose ℳ (∑ i in s, f i) = ∑ i in s, decompose ℳ (f i) :=
+map_sum (decompose_add_equiv ℳ) f s
+@[simp] lemma decompose_symm_sum {ι'} (s : finset ι') (f : ι' → ⨁ i, ℳ i) :
+  (decompose ℳ).symm (∑ i in s, f i) = ∑ i in s, (decompose ℳ).symm (f i) :=
+map_sum (decompose_add_equiv ℳ).symm f s
+
+lemma sum_support_decompose [Π i (x : ℳ i), decidable (x ≠ 0)] (r : M) :
+  ∑ i in (decompose ℳ r).support, (decompose ℳ r i : M) = r :=
+begin
+  conv_rhs { rw [←(decompose ℳ).symm_apply_apply r,
+    ←sum_support_of (λ i, (ℳ i)) (decompose ℳ r)] },
+  rw [decompose_symm_sum],
+  simp_rw decompose_symm_of,
+end
+
+end add_comm_monoid
+
+/-- The `-` in the statements below doesn't resolve without this line.
+
+This seems to a be a problem of synthesized vs inferred typeclasses disagreeing. If we replace
+the statement of `decompose_neg` with `@eq (⨁ i, ℳ i) (decompose ℳ (-x)) (-decompose ℳ x)`
+instead of `decompose ℳ (-x) = -decompose ℳ x`, which forces the typeclasses needed by `⨁ i, ℳ i` to
+be found by unification rather than synthesis, then everything works fine without this instance. -/
+instance add_comm_group_set_like [add_comm_group M] [set_like σ M] [add_subgroup_class σ M]
+  (ℳ : ι → σ) : add_comm_group (⨁ i, ℳ i) := by apply_instance
+
+section add_comm_group
+variables [decidable_eq ι] [add_comm_group M]
+variables [set_like σ M] [add_subgroup_class σ M] (ℳ : ι → σ)
+variables [decomposition ℳ]
+include M
+
+@[simp] lemma decompose_neg (x : M) : decompose ℳ (-x) = -decompose ℳ x :=
+map_neg (decompose_add_equiv ℳ) x
+@[simp] lemma decompose_symm_neg (x : ⨁ i, ℳ i) :
+  (decompose ℳ).symm (-x) = -(decompose ℳ).symm x :=
+map_neg (decompose_add_equiv ℳ).symm x
+
+@[simp] lemma decompose_sub (x y : M) : decompose ℳ (x - y) = decompose ℳ x - decompose ℳ y :=
+map_sub (decompose_add_equiv ℳ) x y
+@[simp] lemma decompose_symm_sub (x y : ⨁ i, ℳ i) :
+  (decompose ℳ).symm (x - y) = (decompose ℳ).symm x - (decompose ℳ).symm y :=
+map_sub (decompose_add_equiv ℳ).symm x y
+
+end add_comm_group
+
+section module
+variables [decidable_eq ι] [semiring R] [add_comm_monoid M] [module R M]
+variables (ℳ : ι → submodule R M)
+variables [decomposition ℳ]
+include M
+
+/-- If `M` is graded by `ι` with degree `i` component `ℳ i`, then it is isomorphic as
+a module to a direct sum of components. -/
+@[simps {fully_applied := ff}]
+def decompose_linear_equiv : M ≃ₗ[R] ⨁ i, ℳ i := linear_equiv.symm
+{ map_smul' := map_smul (direct_sum.coe_linear_map ℳ),
+  ..(decompose_add_equiv ℳ).symm }
+
+@[simp] lemma decompose_smul (r : R) (x : M) : decompose ℳ (r • x) = r • decompose ℳ x :=
+map_smul (decompose_linear_equiv ℳ) r x
+
+end module
+
+end direct_sum

src/algebra/monoid_algebra/grading.lean

@@ -113,7 +113,7 @@ by apply grade_by.graded_monoid (add_monoid_hom.id _)
 variables {R} [add_monoid M] [decidable_eq ι] [add_monoid ι] [comm_semiring R] (f : M →+ ι)
 
 /-- Auxiliary definition; the canonical grade decomposition, used to provide
-`graded_algebra.decompose`. -/
+`direct_sum.decompose`. -/
 def decompose_aux : add_monoid_algebra R M →ₐ[R] ⨁ i : ι, grade_by R f i :=
 add_monoid_algebra.lift R M _
 { to_fun := λ m, direct_sum.of (λ i : ι, grade_by R f i) (f m.to_add)
@@ -182,31 +182,39 @@ graded_algebra.of_alg_hom _
   end)
   (λ i x, by convert (decompose_aux_coe f x : _))
 
+-- Lean can't find this later without us repeating it
+instance grade_by.decomposition : direct_sum.decomposition (grade_by R f) :=
+by apply_instance
+
 @[simp] lemma decompose_aux_eq_decompose :
   ⇑(decompose_aux f : add_monoid_algebra R M →ₐ[R] ⨁ i : ι, grade_by R f i) =
-    (graded_algebra.decompose (grade_by R f)) := rfl
+    (direct_sum.decompose (grade_by R f)) := rfl
 
 @[simp] lemma grades_by.decompose_single (m : M) (r : R) :
-  graded_algebra.decompose (grade_by R f) (finsupp.single m r) =
+  direct_sum.decompose (grade_by R f) (finsupp.single m r) =
     direct_sum.of (λ i : ι, grade_by R f i) (f m)
       ⟨finsupp.single m r, single_mem_grade_by _ _ _⟩ :=
 decompose_aux_single _ _ _
 
 instance grade.graded_algebra : graded_algebra (grade R : ι → submodule _ _) :=
 add_monoid_algebra.grade_by.graded_algebra (add_monoid_hom.id _)
 
+-- Lean can't find this later without us repeating it
+instance grade.decomposition : direct_sum.decomposition (grade R : ι → submodule _ _) :=
+by apply_instance
+
 @[simp]
 lemma grade.decompose_single (i : ι) (r : R) :
-  graded_algebra.decompose (grade R : ι → submodule _ _) (finsupp.single i r) =
+  direct_sum.decompose (grade R : ι → submodule _ _) (finsupp.single i r) =
     direct_sum.of (λ i : ι, grade R i) i ⟨finsupp.single i r, single_mem_grade _ _⟩ :=
 decompose_aux_single _ _ _
 
 /-- `add_monoid_algebra.gradesby` describe an internally graded algebra -/
 lemma grade_by.is_internal : direct_sum.is_internal (grade_by R f) :=
-graded_algebra.is_internal _
+direct_sum.decomposition.is_internal _
 
 /-- `add_monoid_algebra.grades` describe an internally graded algebra -/
 lemma grade.is_internal : direct_sum.is_internal (grade R : ι → submodule R _) :=
-graded_algebra.is_internal _
+direct_sum.decomposition.is_internal _
 
 end add_monoid_algebra

src/algebraic_geometry/projective_spectrum/topology.lean

@@ -392,8 +392,8 @@ topological_space.opens.ext $ set.ext $ λ z, begin
   split; intros hz,
   { rcases show ∃ i, graded_algebra.proj 𝒜 i f ∉ z.as_homogeneous_ideal, begin
       contrapose! hz with H,
-      haveI : Π (i : ℕ) (x : 𝒜 i), decidable (x ≠ 0) := λ _, classical.dec_pred _,
-      rw ←graded_algebra.sum_support_decompose 𝒜 f,
+      classical,
+      rw ←direct_sum.sum_support_decompose 𝒜 f,
       apply ideal.sum_mem _ (λ i hi, H i)
     end with ⟨i, hi⟩,
     exact ⟨basic_open 𝒜 (graded_algebra.proj 𝒜 i f), ⟨i, rfl⟩, by rwa mem_basic_open⟩ },