|
| 1 | +/- |
| 2 | +Copyright (c) 2024 Joël Riou. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Joël Riou |
| 5 | +-/ |
| 6 | +import Mathlib.Algebra.Module.Presentation.Basic |
| 7 | +import Mathlib.Algebra.DirectSum.Module |
| 8 | +import Mathlib.Data.Finsupp.ToDFinsupp |
| 9 | + |
| 10 | +/-! |
| 11 | +# Presentation of a direct sum |
| 12 | +
|
| 13 | +If `M : ι → Type _` is a family of `A`-modules, then the data of a presentation |
| 14 | +of each `M i`, we obtain a presentation of the module `⨁ i, M i`. |
| 15 | +In particular, from a presentation of an `A`-module `M`, we get |
| 16 | +a presention of `ι →₀ M`. |
| 17 | +
|
| 18 | +-/ |
| 19 | + |
| 20 | +universe w' w₀ w₁ w v u |
| 21 | + |
| 22 | +namespace Module |
| 23 | + |
| 24 | +open DirectSum |
| 25 | + |
| 26 | +variable {A : Type u} [Ring A] {ι : Type w} [DecidableEq ι] |
| 27 | + (relations : ι → Relations.{w₀, w₁} A) |
| 28 | + {M : ι → Type v} [∀ i, AddCommGroup (M i)] [∀ i, Module A (M i)] |
| 29 | + |
| 30 | +namespace Relations |
| 31 | + |
| 32 | +/-- The direct sum operations on `Relations A`. Given a family |
| 33 | +`relations : ι → Relations A`, the type of generators and relations |
| 34 | +in `directSum relations` are the corresponding `Sigma` types. -/ |
| 35 | +@[simps G R relation] |
| 36 | +noncomputable def directSum : Relations A where |
| 37 | + G := Σ i, (relations i).G |
| 38 | + R := Σ i, (relations i).R |
| 39 | + relation := fun ⟨i, r⟩ ↦ Finsupp.embDomain (Function.Embedding.sigmaMk |
| 40 | + (β := fun i ↦ (relations i).G) i) ((relations i).relation r) |
| 41 | + |
| 42 | +namespace Solution |
| 43 | + |
| 44 | +variable {relations} |
| 45 | +variable {N : Type v} [AddCommGroup N] [Module A N] |
| 46 | + |
| 47 | +/-- Given an `A`-module `N` and a family `relations : ι → Relations A`, |
| 48 | +the data of a solution of `Relations.directSum relations` in `N` |
| 49 | +is equivalent to the data of a family of solutions of `relations i` in `N` |
| 50 | +for all `i`. -/ |
| 51 | +@[simps] |
| 52 | +def directSumEquiv : |
| 53 | + (Relations.directSum relations).Solution N ≃ |
| 54 | + ∀ i, (relations i).Solution N where |
| 55 | + toFun s i := |
| 56 | + { var := fun g ↦ s.var ⟨i, g⟩ |
| 57 | + linearCombination_var_relation := fun r ↦ by |
| 58 | + rw [← s.linearCombination_var_relation ⟨i, r⟩] |
| 59 | + symm |
| 60 | + apply Finsupp.linearCombination_embDomain } |
| 61 | + invFun t := |
| 62 | + { var := fun ⟨i, g⟩ ↦ (t i).var g |
| 63 | + linearCombination_var_relation := fun ⟨i, r⟩ ↦ by |
| 64 | + erw [← (t i).linearCombination_var_relation r] |
| 65 | + apply Finsupp.linearCombination_embDomain } |
| 66 | + left_inv _ := rfl |
| 67 | + right_inv _ := rfl |
| 68 | + |
| 69 | +/-- Given `solution : ∀ (i : ι), (relations i).Solution (M i)`, this is the |
| 70 | +canonical solution of `Relations.directSum relations` in `⨁ i, M i`. -/ |
| 71 | +def directSum (solution : ∀ (i : ι), (relations i).Solution (M i)) : |
| 72 | + (Relations.directSum relations).Solution (⨁ i, M i) := |
| 73 | + directSumEquiv.symm (fun i ↦ (solution i).postcomp (lof A ι M i)) |
| 74 | + |
| 75 | +@[simp] |
| 76 | +lemma directSum_var (solution : ∀ (i : ι), (relations i).Solution (M i)) |
| 77 | + (i : ι) (g : (relations i).G) : |
| 78 | + (directSum solution).var ⟨i, g⟩ = lof A ι M i ((solution i).var g) := rfl |
| 79 | + |
| 80 | +namespace IsPresentation |
| 81 | + |
| 82 | +variable {solution : ∀ (i : ι), (relations i).Solution (M i)} |
| 83 | + (h : ∀ i, (solution i).IsPresentation) |
| 84 | + |
| 85 | +/-- The direct sum admits a presentation by generators and relations. -/ |
| 86 | +noncomputable def directSum.isRepresentationCore : |
| 87 | + Solution.IsPresentationCore.{w'} (directSum solution) where |
| 88 | + desc s := DirectSum.toModule _ _ _ (fun i ↦ (h i).desc (directSumEquiv s i)) |
| 89 | + postcomp_desc s := by ext ⟨i, g⟩; simp |
| 90 | + postcomp_injective h' := by |
| 91 | + ext i : 1 |
| 92 | + apply (h i).postcomp_injective |
| 93 | + ext g |
| 94 | + exact Solution.congr_var h' ⟨i, g⟩ |
| 95 | + |
| 96 | +include h in |
| 97 | +lemma directSum : (directSum solution).IsPresentation := |
| 98 | + (directSum.isRepresentationCore h).isPresentation |
| 99 | + |
| 100 | +end IsPresentation |
| 101 | + |
| 102 | +end Solution |
| 103 | + |
| 104 | +end Relations |
| 105 | + |
| 106 | +namespace Presentation |
| 107 | + |
| 108 | +/-- The obvious presentation of the module `⨁ i, M i` that is obtained from |
| 109 | +the data of presentations of the module `M i` for each `i`. -/ |
| 110 | +@[simps! G R relation] |
| 111 | +noncomputable def directSum (pres : ∀ (i : ι), Presentation A (M i)) : |
| 112 | + Presentation A (⨁ i, M i) := |
| 113 | + ofIsPresentation |
| 114 | + (Relations.Solution.IsPresentation.directSum (fun i ↦ (pres i).toIsPresentation)) |
| 115 | + |
| 116 | +@[simp] |
| 117 | +lemma directSum_var (pres : ∀ (i : ι), Presentation A (M i)) (i : ι) (g : (pres i).G): |
| 118 | + (directSum pres).var ⟨i, g⟩ = lof A ι M i ((pres i).var g) := rfl |
| 119 | + |
| 120 | +section |
| 121 | + |
| 122 | +variable {N : Type v} [AddCommGroup N] [Module A N] |
| 123 | + (pres : Presentation A N) (ι : Type w) [DecidableEq ι] [DecidableEq N] |
| 124 | + |
| 125 | +/-- The obvious presentation of the module `ι →₀ N` that is deduced from a presentation |
| 126 | +of the module `N`. -/ |
| 127 | +@[simps! G R relation] |
| 128 | +noncomputable def finsupp : Presentation A (ι →₀ N) := |
| 129 | + (directSum (fun (_ : ι) ↦ pres)).ofLinearEquiv (finsuppLequivDFinsupp _).symm |
| 130 | + |
| 131 | +@[simp] |
| 132 | +lemma finsupp_var (i : ι) (g : pres.G) : |
| 133 | + (finsupp pres ι).var ⟨i, g⟩ = Finsupp.single i (pres.var g) := by |
| 134 | + apply (finsuppLequivDFinsupp A).injective |
| 135 | + erw [(finsuppLequivDFinsupp A).apply_symm_apply] |
| 136 | + rw [directSum_var, finsuppLequivDFinsupp_apply_apply, Finsupp.toDFinsupp_single] |
| 137 | + rfl |
| 138 | + |
| 139 | +end |
| 140 | + |
| 141 | +end Presentation |
| 142 | + |
| 143 | +end Module |
0 commit comments