WIP

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. -/

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

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]
 

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₂) :=

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],

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]