|
| 1 | +/- |
| 2 | +Copyright (c) 2017 Johannes Hölzl. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Johannes Hölzl, Mario Carneiro, Kevin Buzzard, Yury Kudryashov |
| 5 | +-/ |
| 6 | +import linear_algebra.quotient |
| 7 | + |
| 8 | +/-! |
| 9 | +# Isomorphism theorems for modules. |
| 10 | +
|
| 11 | +* The Noether's first, second, and third isomorphism theorems for modules are proved as |
| 12 | + `linear_map.quot_ker_equiv_range`, `linear_map.quotient_inf_equiv_sup_quotient` and |
| 13 | + `submodule.quotient_quotient_equiv_quotient`. |
| 14 | +
|
| 15 | +-/ |
| 16 | + |
| 17 | +universes u v |
| 18 | + |
| 19 | +variables {R M M₂ M₃ : Type*} |
| 20 | +variables [ring R] [add_comm_group M] [add_comm_group M₂] [add_comm_group M₃] |
| 21 | +variables [module R M] [module R M₂] [module R M₃] |
| 22 | +variables (f : M →ₗ[R] M₂) |
| 23 | + |
| 24 | +/-! The first and second isomorphism theorems for modules. -/ |
| 25 | +namespace linear_map |
| 26 | + |
| 27 | +open submodule |
| 28 | + |
| 29 | +section isomorphism_laws |
| 30 | + |
| 31 | +/-- The first isomorphism law for modules. The quotient of `M` by the kernel of `f` is linearly |
| 32 | +equivalent to the range of `f`. -/ |
| 33 | +noncomputable def quot_ker_equiv_range : f.ker.quotient ≃ₗ[R] f.range := |
| 34 | +(linear_equiv.of_injective (f.ker.liftq f $ le_refl _) $ |
| 35 | + ker_eq_bot.mp $ submodule.ker_liftq_eq_bot _ _ _ (le_refl f.ker)).trans |
| 36 | + (linear_equiv.of_eq _ _ $ submodule.range_liftq _ _ _) |
| 37 | + |
| 38 | +/-- The first isomorphism theorem for surjective linear maps. -/ |
| 39 | +noncomputable def quot_ker_equiv_of_surjective |
| 40 | + (f : M →ₗ[R] M₂) (hf : function.surjective f) : f.ker.quotient ≃ₗ[R] M₂ := |
| 41 | +f.quot_ker_equiv_range.trans |
| 42 | + (linear_equiv.of_top f.range (linear_map.range_eq_top.2 hf)) |
| 43 | + |
| 44 | +@[simp] lemma quot_ker_equiv_range_apply_mk (x : M) : |
| 45 | + (f.quot_ker_equiv_range (submodule.quotient.mk x) : M₂) = f x := |
| 46 | +rfl |
| 47 | + |
| 48 | +@[simp] lemma quot_ker_equiv_range_symm_apply_image (x : M) (h : f x ∈ f.range) : |
| 49 | + f.quot_ker_equiv_range.symm ⟨f x, h⟩ = f.ker.mkq x := |
| 50 | +f.quot_ker_equiv_range.symm_apply_apply (f.ker.mkq x) |
| 51 | + |
| 52 | +/-- |
| 53 | +Canonical linear map from the quotient `p/(p ∩ p')` to `(p+p')/p'`, mapping `x + (p ∩ p')` |
| 54 | +to `x + p'`, where `p` and `p'` are submodules of an ambient module. |
| 55 | +-/ |
| 56 | +def quotient_inf_to_sup_quotient (p p' : submodule R M) : |
| 57 | + (comap p.subtype (p ⊓ p')).quotient →ₗ[R] (comap (p ⊔ p').subtype p').quotient := |
| 58 | +(comap p.subtype (p ⊓ p')).liftq |
| 59 | + ((comap (p ⊔ p').subtype p').mkq.comp (of_le le_sup_left)) begin |
| 60 | +rw [ker_comp, of_le, comap_cod_restrict, ker_mkq, map_comap_subtype], |
| 61 | +exact comap_mono (inf_le_inf_right _ le_sup_left) end |
| 62 | + |
| 63 | +/-- |
| 64 | +Second Isomorphism Law : the canonical map from `p/(p ∩ p')` to `(p+p')/p'` as a linear isomorphism. |
| 65 | +-/ |
| 66 | +noncomputable def quotient_inf_equiv_sup_quotient (p p' : submodule R M) : |
| 67 | + (comap p.subtype (p ⊓ p')).quotient ≃ₗ[R] (comap (p ⊔ p').subtype p').quotient := |
| 68 | +linear_equiv.of_bijective (quotient_inf_to_sup_quotient p p') |
| 69 | + begin |
| 70 | + rw [← ker_eq_bot, quotient_inf_to_sup_quotient, ker_liftq_eq_bot], |
| 71 | + rw [ker_comp, ker_mkq], |
| 72 | + exact λ ⟨x, hx1⟩ hx2, ⟨hx1, hx2⟩ |
| 73 | + end |
| 74 | + begin |
| 75 | + rw [← range_eq_top, quotient_inf_to_sup_quotient, range_liftq, eq_top_iff'], |
| 76 | + rintros ⟨x, hx⟩, rcases mem_sup.1 hx with ⟨y, hy, z, hz, rfl⟩, |
| 77 | + use [⟨y, hy⟩], apply (submodule.quotient.eq _).2, |
| 78 | + change y - (y + z) ∈ p', |
| 79 | + rwa [sub_add_eq_sub_sub, sub_self, zero_sub, neg_mem_iff] |
| 80 | + end |
| 81 | + |
| 82 | +@[simp] lemma coe_quotient_inf_to_sup_quotient (p p' : submodule R M) : |
| 83 | + ⇑(quotient_inf_to_sup_quotient p p') = quotient_inf_equiv_sup_quotient p p' := rfl |
| 84 | + |
| 85 | +@[simp] lemma quotient_inf_equiv_sup_quotient_apply_mk (p p' : submodule R M) (x : p) : |
| 86 | + quotient_inf_equiv_sup_quotient p p' (submodule.quotient.mk x) = |
| 87 | + submodule.quotient.mk (of_le (le_sup_left : p ≤ p ⊔ p') x) := |
| 88 | +rfl |
| 89 | + |
| 90 | +lemma quotient_inf_equiv_sup_quotient_symm_apply_left (p p' : submodule R M) |
| 91 | + (x : p ⊔ p') (hx : (x:M) ∈ p) : |
| 92 | + (quotient_inf_equiv_sup_quotient p p').symm (submodule.quotient.mk x) = |
| 93 | + submodule.quotient.mk ⟨x, hx⟩ := |
| 94 | +(linear_equiv.symm_apply_eq _).2 $ by simp [of_le_apply] |
| 95 | + |
| 96 | +@[simp] lemma quotient_inf_equiv_sup_quotient_symm_apply_eq_zero_iff {p p' : submodule R M} |
| 97 | + {x : p ⊔ p'} : |
| 98 | + (quotient_inf_equiv_sup_quotient p p').symm (submodule.quotient.mk x) = 0 ↔ (x:M) ∈ p' := |
| 99 | +(linear_equiv.symm_apply_eq _).trans $ by simp [of_le_apply] |
| 100 | + |
| 101 | +lemma quotient_inf_equiv_sup_quotient_symm_apply_right (p p' : submodule R M) {x : p ⊔ p'} |
| 102 | + (hx : (x:M) ∈ p') : |
| 103 | + (quotient_inf_equiv_sup_quotient p p').symm (submodule.quotient.mk x) = 0 := |
| 104 | +quotient_inf_equiv_sup_quotient_symm_apply_eq_zero_iff.2 hx |
| 105 | + |
| 106 | +end isomorphism_laws |
| 107 | + |
| 108 | +end linear_map |
| 109 | + |
| 110 | +/-! The third isomorphism theorem for modules. -/ |
| 111 | +namespace submodule |
| 112 | + |
| 113 | +variables (S T : submodule R M) (h : S ≤ T) |
| 114 | + |
| 115 | +/-- The map from the third isomorphism theorem for modules: `(M / S) / (T / S) → M / T`. -/ |
| 116 | +def quotient_quotient_equiv_quotient_aux : |
| 117 | + quotient (T.map S.mkq) →ₗ[R] quotient T := |
| 118 | +liftq _ (mapq S T linear_map.id h) |
| 119 | + (by { rintro _ ⟨x, hx, rfl⟩, rw [linear_map.mem_ker, mkq_apply, mapq_apply], |
| 120 | + exact (quotient.mk_eq_zero _).mpr hx }) |
| 121 | + |
| 122 | +@[simp] lemma quotient_quotient_equiv_quotient_aux_mk (x : S.quotient) : |
| 123 | + quotient_quotient_equiv_quotient_aux S T h (quotient.mk x) = mapq S T linear_map.id h x := |
| 124 | +liftq_apply _ _ _ |
| 125 | + |
| 126 | +@[simp] lemma quotient_quotient_equiv_quotient_aux_mk_mk (x : M) : |
| 127 | + quotient_quotient_equiv_quotient_aux S T h (quotient.mk (quotient.mk x)) = quotient.mk x := |
| 128 | +by rw [quotient_quotient_equiv_quotient_aux_mk, mapq_apply, linear_map.id_apply] |
| 129 | + |
| 130 | +/-- **Noether's third isomorphism theorem** for modules: `(M / S) / (T / S) ≃ M / T`. -/ |
| 131 | +def quotient_quotient_equiv_quotient : |
| 132 | + quotient (T.map S.mkq) ≃ₗ[R] quotient T := |
| 133 | +{ to_fun := quotient_quotient_equiv_quotient_aux S T h, |
| 134 | + inv_fun := mapq _ _ (mkq S) (le_comap_map _ _), |
| 135 | + left_inv := λ x, quotient.induction_on' x $ λ x, quotient.induction_on' x $ λ x, by simp, |
| 136 | + right_inv := λ x, quotient.induction_on' x $ λ x, by simp, |
| 137 | + .. quotient_quotient_equiv_quotient_aux S T h } |
| 138 | + |
| 139 | +end submodule |
0 commit comments