diff --git a/src/algebra/algebra/operations.lean b/src/algebra/algebra/operations.lean index 492885cb7f309..1129f2fcb7137 100644 --- a/src/algebra/algebra/operations.lean +++ b/src/algebra/algebra/operations.lean @@ -325,7 +325,15 @@ instance : idem_semiring (submodule R A) := ..(by apply_instance : order_bot (submodule R A)), ..(by apply_instance : lattice (submodule R A)) } -variables (M) +variable R + +def span_singleton : A →*₀ submodule R A := +{ to_fun := λ x, span R {x}, + map_zero' := span_zero_singleton R, + map_one' := one_eq_span.symm, + map_mul' := λ x y, by rw [span_mul_span, set.singleton_mul_singleton] } + +variables {R} (M) lemma span_pow (s : set A) : ∀ n : ℕ, span R s ^ n = span R (s ^ n) | 0 := by rw [pow_zero, pow_zero, one_eq_span_one_set] @@ -418,14 +426,21 @@ is closed under addition, and holds for `x * m` where `m ∈ M` and it holds for submodule.pow_induction_on_right' M (by exact hr) (λ x y i hx hy, hadd x y) (λ i x hx, hmul _) hx -/-- `submonoid.map` as a `monoid_with_zero_hom`, when applied to `alg_hom`s. -/ +/-- `submodule.map` as a `ring_hom`, when applied to an `alg_hom`. -/ @[simps] def map_hom {A'} [semiring A'] [algebra R A'] (f : A →ₐ[R] A') : - submodule R A →*₀ submodule R A' := -{ to_fun := map f.to_linear_map, - map_zero' := submodule.map_bot _, + submodule R A →+* submodule R A' := +{ to_fun := map f, + map_zero' := map_bot _, map_one' := submodule.map_one _, - map_mul' := λ _ _, submodule.map_mul _ _ _} + map_add' := (add_hom f).map_add, + map_mul' := λ _ _, submodule.map_mul _ _ _ } + +/-- `submodule.map` as a `ring_equiv`, when applied to an `alg_equiv`. -/ +@[simps] +def map_equiv {A'} [semiring A'] [algebra R A'] (f : A ≃ₐ[R] A') : + submodule R A ≃+* submodule R A' := +{ map_mul' := λ _ _, submodule.map_mul _ _ f.to_alg_hom, .. add_equiv f.to_linear_equiv } /-- The ring of submodules of the opposite algebra is isomorphic to the opposite ring of submodules. -/ diff --git a/src/algebra/module/equiv.lean b/src/algebra/module/equiv.lean index 5cb99e06014d4..0986a0e897a4b 100644 --- a/src/algebra/module/equiv.lean +++ b/src/algebra/module/equiv.lean @@ -102,6 +102,16 @@ instance [ring_hom_inv_pair σ σ'] [ring_hom_inv_pair σ' σ] [s : semilinear_e coe_injective' := @fun_like.coe_injective F _ _ _, ..s } +variable {F} +def to_linear_equiv [ring_hom_inv_pair σ σ'] [ring_hom_inv_pair σ' σ] + [semilinear_equiv_class F σ M M₂] (f : F) : M ≃ₛₗ[σ] M₂ := +{ to_fun := f, + map_add' := map_add f, + map_smul' := map_smulₛₗ f, + inv_fun := inv f, + left_inv := left_inv f, + right_inv := right_inv f } + end semilinear_equiv_class namespace linear_equiv diff --git a/src/algebra/module/submodule/pointwise.lean b/src/algebra/module/submodule/pointwise.lean index bc4be0638ac43..598c73ca6a147 100644 --- a/src/algebra/module/submodule/pointwise.lean +++ b/src/algebra/module/submodule/pointwise.lean @@ -149,6 +149,29 @@ instance : canonically_ordered_add_monoid (submodule R M) := ..submodule.pointwise_add_comm_monoid, ..submodule.complete_lattice } +section hom + +variables {R₂ M₂ F : Type*} [semiring R₂] [add_comm_monoid M₂] [module R₂ M₂] + {σ₁₂ : R →+* R₂} [ring_hom_surjective σ₁₂] + +/-- `submodule.map` as an `add_hom`. -/ +@[simps] def add_hom [semilinear_map_class F σ₁₂ M M₂] (f : F) : submodule R M →+ submodule R₂ M₂ := +{ to_fun := map f, + map_zero' := map_bot f, + map_add' := by { intros, simp_rw add_eq_sup, apply map_sup } } + +/-- `submodule.map` as an `add_equiv`, when applied to a `linear_equiv`. + TODO: allow `semilinear_equiv_class`. -/ +@[simps] def add_equiv {σ₂₁ : R₂ →+* R} [ring_hom_inv_pair σ₁₂ σ₂₁] [ring_hom_inv_pair σ₂₁ σ₁₂] + (f : M ≃ₛₗ[σ₁₂] M₂) : submodule R M ≃+ submodule R₂ M₂ := +{ to_fun := map f, + inv_fun := map f.symm, + left_inv := λ N, by rw map_symm_eq_iff, + right_inv := λ N, by rw ← map_symm_eq_iff, + map_add' := (add_hom f).map_add } + +end hom + section variables [monoid α] [distrib_mul_action α M] [smul_comm_class α R M] diff --git a/src/linear_algebra/basic.lean b/src/linear_algebra/basic.lean index 4fe744590ba1e..09ea5fd6cba6b 100644 --- a/src/linear_algebra/basic.lean +++ b/src/linear_algebra/basic.lean @@ -1996,7 +1996,9 @@ end submodule namespace submodule -variables [comm_semiring R] [comm_semiring R₂] +section + +variables [semiring R] [semiring R₂] variables [add_comm_monoid M] [add_comm_monoid M₂] [module R M] [module R₂ M₂] variables [add_comm_monoid N] [add_comm_monoid N₂] [module R N] [module R N₂] variables {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} @@ -2043,16 +2045,6 @@ lemma order_iso_map_comap_symm_apply' (e : M ≃ₛₗ[τ₁₂] M₂) (p : subm p.comap_equiv_eq_map_symm _ omit τ₂₁ -lemma comap_le_comap_smul (fₗ : N →ₗ[R] N₂) (c : R) : - comap fₗ qₗ ≤ comap (c • fₗ) qₗ := -begin - rw set_like.le_def, - intros m h, - change c • (fₗ m) ∈ qₗ, - change fₗ m ∈ qₗ at h, - apply qₗ.smul_mem _ h, -end - lemma inf_comap_le_comap_add (f₁ f₂ : M →ₛₗ[τ₁₂] M₂) : comap f₁ q ⊓ comap f₂ q ≤ comap (f₁ + f₂) q := begin @@ -2063,6 +2055,21 @@ begin apply q.add_mem h.1 h.2, end +end + +variables [comm_semiring R] [add_comm_monoid N] [add_comm_monoid N₂] [module R N] [module R N₂] +variables (pₗ : submodule R N) (qₗ : submodule R N₂) + +lemma comap_le_comap_smul (fₗ : N →ₗ[R] N₂) (c : R) : + comap fₗ qₗ ≤ comap (c • fₗ) qₗ := +begin + rw set_like.le_def, + intros m h, + change c • (fₗ m) ∈ qₗ, + change fₗ m ∈ qₗ at h, + apply qₗ.smul_mem _ h, +end + /-- Given modules `M`, `M₂` over a commutative ring, together with submodules `p ⊆ M`, `q ⊆ M₂`, the set of maps $\{f ∈ Hom(M, M₂) | f(p) ⊆ q \}$ is a submodule of `Hom(M, M₂)`. -/ def compatible_maps : submodule R (N →ₗ[R] N₂) := diff --git a/src/ring_theory/class_group.lean b/src/ring_theory/class_group.lean index 446a8b7cdbbb8..76153187e5628 100644 --- a/src/ring_theory/class_group.lean +++ b/src/ring_theory/class_group.lean @@ -36,43 +36,40 @@ variables [algebra R L] [is_scalar_tower R K L] open_locale non_zero_divisors -open is_localization is_fraction_ring fractional_ideal units +open is_localization is_fraction_ring submodule units section variables (R K) +/-- The group of invertible fractional `R`-ideals in `K` is isomorphic to the group of + invertible `R`-submodules of `K`. We will use the latter henceforth for simplicity. -/ +example : (fractional_ideal R⁰ K)ˣ ≃* (submodule R K)ˣ := fractional_ideal.unit_equiv + /-- `to_principal_ideal R K x` sends `x ≠ 0 : K` to the fractional `R`-ideal generated by `x` -/ @[irreducible] -def to_principal_ideal : Kˣ →* (fractional_ideal R⁰ K)ˣ := -{ to_fun := λ x, - ⟨span_singleton _ x, - span_singleton _ x⁻¹, - by simp only [span_singleton_one, units.mul_inv', span_singleton_mul_span_singleton], - by simp only [span_singleton_one, units.inv_mul', span_singleton_mul_span_singleton]⟩, - map_mul' := λ x y, ext - (by simp only [units.coe_mk, units.coe_mul, span_singleton_mul_span_singleton]), - map_one' := ext (by simp only [span_singleton_one, units.coe_mk, units.coe_one]) } +def to_principal_ideal : Kˣ →* (submodule R K)ˣ := units.map (span_singleton R).to_monoid_hom variables {R K} @[simp] lemma coe_to_principal_ideal (x : Kˣ) : - (to_principal_ideal R K x : fractional_ideal R⁰ K) = span_singleton _ x := + (to_principal_ideal R K x : submodule R K) = span R {x} := by { simp only [to_principal_ideal], refl } -@[simp] lemma to_principal_ideal_eq_iff {I : (fractional_ideal R⁰ K)ˣ} {x : Kˣ} : - to_principal_ideal R K x = I ↔ span_singleton R⁰ (x : K) = I := +@[simp] lemma to_principal_ideal_eq_iff {I : (submodule R K)ˣ} {x : Kˣ} : + to_principal_ideal R K x = I ↔ span R ({x} : set K) = I := by { simp only [to_principal_ideal], exact units.ext_iff } -lemma mem_principal_ideals_iff {I : (fractional_ideal R⁰ K)ˣ} : - I ∈ (to_principal_ideal R K).range ↔ ∃ x : K, span_singleton R⁰ x = I := +lemma mem_principal_ideals_iff {I : (submodule R K)ˣ} : + I ∈ (to_principal_ideal R K).range ↔ ∃ x : K, span R ({x} : set K) = I := begin simp only [monoid_hom.mem_range, to_principal_ideal_eq_iff], split; rintros ⟨x, hx⟩, { exact ⟨x, hx⟩ }, { refine ⟨units.mk0 x _, hx⟩, rintro rfl, - simpa [I.ne_zero.symm] using hx } + apply I.ne_zero.symm, + simpa using hx } end instance principal_ideals.normal : (to_principal_ideal R K).range.normal := @@ -86,18 +83,26 @@ variables (R) [is_domain R] modulo the principal ideals. -/ @[derive comm_group] def class_group := -(fractional_ideal R⁰ (fraction_ring R))ˣ ⧸ (to_principal_ideal R (fraction_ring R)).range +(submodule R (fraction_ring R))ˣ ⧸ (to_principal_ideal R (fraction_ring R)).range noncomputable instance : inhabited (class_group R) := ⟨1⟩ variables {R K} /-- Send a nonzero fractional ideal to the corresponding class in the class group. -/ -noncomputable def class_group.mk : (fractional_ideal R⁰ K)ˣ →* class_group R := -(quotient_group.mk' (to_principal_ideal R (fraction_ring R)).range).comp - (units.map (fractional_ideal.canonical_equiv R⁰ K (fraction_ring R))) +noncomputable def class_group.mk : (submodule R K)ˣ →* class_group R := +(quotient_group.mk' _).comp $ mul_equiv.to_monoid_hom $ units.map_equiv $ + ring_equiv.to_mul_equiv $ submodule.map_equiv $ is_localization.alg_equiv R⁰ _ _ + +lemma class_group.mk_apply (I : (submodule R $ fraction_ring R)ˣ) : + class_group.mk I = quotient_group.mk' _ I := +begin + rw [class_group.mk, monoid_hom.comp_apply], + congr, ext1, squeeze_simp, + convert submodule.map_id I, +end -lemma class_group.mk_eq_mk {I J : (fractional_ideal R⁰ $ fraction_ring R)ˣ} : +lemma class_group.mk_eq_mk {I J : (submodule R $ fraction_ring R)ˣ} : class_group.mk I = class_group.mk J ↔ ∃ x : (fraction_ring R)ˣ, I * to_principal_ideal R (fraction_ring R) x = J := by { erw [quotient_group.mk'_eq_mk', canonical_equiv_self, units.map_id, set.exists_range_iff], diff --git a/src/ring_theory/fractional_ideal.lean b/src/ring_theory/fractional_ideal.lean index 676ec477949c0..d8b43e86cf6ce 100644 --- a/src/ring_theory/fractional_ideal.lean +++ b/src/ring_theory/fractional_ideal.lean @@ -78,17 +78,19 @@ variables [algebra R P] variables (S) -/-- A submodule `I` is a fractional ideal if `a I ⊆ R` for some `a ≠ 0`. -/ +/-- A submodule `I` is a fractional ideal with respect to a submonoid `S` + if `a I ⊆ R` for some `a ∈ S`. -/ def is_fractional (I : submodule R P) := ∃ a ∈ S, ∀ b ∈ I, is_integer R (a • b) variables (S P) -/-- The fractional ideals of a domain `R` are ideals of `R` divided by some `a ∈ R`. +/-- The fractional ideals of a domain `R` with respect to a submonoid `S` + are ideals of `R` divided by some `a ∈ S`. More precisely, let `P` be a localization of `R` at some submonoid `S`, then a fractional ideal `I ⊆ P` is an `R`-submodule of `P`, - such that there is a nonzero `a : R` with `a I ⊆ R`. + such that there is an `a ∈ S` with `a I ⊆ R`. -/ def fractional_ideal := {I : submodule R P // is_fractional S I} @@ -691,7 +693,7 @@ lemma is_fractional_span_iff {s : set P} : include loc -lemma is_fractional_of_fg {I : submodule R P} (hI : I.fg) : +lemma _root_.is_fractional_of_fg {I : submodule R P} (hI : I.fg) : is_fractional S I := begin rcases hI with ⟨I, rfl⟩, @@ -700,6 +702,29 @@ begin exact ⟨s, hs1, hs⟩, end +lemma _root_.is_fractional_unit (I : (submodule R P)ˣ) : is_fractional S (I : submodule R P) := +is_fractional_of_fg $ fg_unit I + +lemma _root_.is_fractional_of_is_unit {I : submodule R P} (hI : is_unit I) : is_fractional S I := +is_fractional_of_fg $ fg_of_is_unit hI + +/-- The group of invertible fractional `R`-ideals in `P` is isomorphic to + the group of invertible `R`-submodules of `P`. -/ +def unit_equiv : (fractional_ideal S P)ˣ ≃* (submodule R P)ˣ := +{ to_fun := λ I, by use [I, ↑I⁻¹]; + simp only [coe_coe, ← fractional_ideal.coe_mul, I.mul_inv, I.inv_mul, fractional_ideal.coe_one], + inv_fun := λ I, begin + use [⟨I, is_fractional_unit I⟩, ⟨_, is_fractional_unit I⁻¹⟩]; + apply subtype.ext; + simp only [fractional_ideal.coe_mul, fractional_ideal.coe_mk, + I.mul_inv, I.inv_mul, fractional_ideal.coe_one], + end, + left_inv := λ I, by { ext1, ext1, refl }, + right_inv := λ I, by { ext1, refl }, + map_mul' := λ I J, begin + ext1, simp only [coe_coe, fractional_ideal.coe_mul, units.coe_mul, units.coe_mk], + end } + omit loc lemma mem_span_mul_finite_of_mem_mul {I J : fractional_ideal S P} {x : P} (hx : x ∈ I * J) : @@ -731,6 +756,15 @@ variables (S P P') include loc loc' +@[irreducible] +noncomputable def canonical_equiv : + fractional_ideal S P ≃+* fractional_ideal S P' := +submodule.map_equiv + { commutes' := λ r, ring_equiv_of_ring_equiv_eq _ _, + ..ring_equiv_of_ring_equiv P P' (ring_equiv.refl R) + (show S.map _ = S, by rw [ring_equiv.to_monoid_hom_refl, submonoid.map_id]) } + + /-- `canonical_equiv f f'` is the canonical equivalence between the fractional ideals in `P` and in `P'` -/ @[irreducible]