diff --git a/src/data/equiv/ring.lean b/src/data/equiv/ring.lean
index 43d7bb3a14f0f..f0cd6c2f3b305 100644
--- a/src/data/equiv/ring.lean
+++ b/src/data/equiv/ring.lean
@@ -52,8 +52,7 @@ variables [has_mul R] [has_add R] [has_mul S] [has_add S] [has_mul S'] [has_add
 
 instance : has_coe_to_fun (R ≃+* S) := ⟨_, ring_equiv.to_fun⟩
 
-@[simp]
-lemma to_fun_eq_coe (f : R ≃+* S) : f.to_fun = f := rfl
+@[simp] lemma to_fun_eq_coe_fun (f : R ≃+* S) : f.to_fun = f := rfl
 
 instance has_coe_to_mul_equiv : has_coe (R ≃+* S) (R ≃* S) := ⟨ring_equiv.to_mul_equiv⟩
 
@@ -70,6 +69,12 @@ variable (R)
 /-- The identity map is a ring isomorphism. -/
 @[refl] protected def refl : R ≃+* R := { .. mul_equiv.refl R, .. add_equiv.refl R }
 
+@[simp] lemma refl_apply (x : R) : ring_equiv.refl R x = x := rfl
+
+@[simp] lemma coe_add_equiv_refl : (ring_equiv.refl R : R ≃+ R) = add_equiv.refl R := rfl
+
+@[simp] lemma coe_mul_equiv_refl : (ring_equiv.refl R : R ≃* R) = mul_equiv.refl R := rfl
+
 variables {R}
 
 /-- The inverse of a ring isomorphism is a ring isomorphism. -/
@@ -169,6 +174,15 @@ def of (e : R ≃ S) [is_semiring_hom e] : R ≃+* S :=
 
 instance (e : R ≃+* S) : is_semiring_hom e := e.to_ring_hom.is_semiring_hom
 
+@[simp]
+lemma to_ring_hom_refl : (ring_equiv.refl R).to_ring_hom = ring_hom.id R := rfl
+
+@[simp]
+lemma to_monoid_hom_refl : (ring_equiv.refl R).to_monoid_hom = monoid_hom.id R := rfl
+
+@[simp]
+lemma to_add_monoid_hom_refl : (ring_equiv.refl R).to_add_monoid_hom = add_monoid_hom.id R := rfl
+
 @[simp]
 lemma to_ring_hom_apply_symm_to_ring_hom_apply {R S} [semiring R] [semiring S] (e : R ≃+* S) :
   ∀ (y : S), e.to_ring_hom (e.symm.to_ring_hom y) = y :=
diff --git a/src/group_theory/submonoid.lean b/src/group_theory/submonoid.lean
index 9e74647ead01c..50ef34c7b1660 100644
--- a/src/group_theory/submonoid.lean
+++ b/src/group_theory/submonoid.lean
@@ -510,6 +510,9 @@ lemma comap_infi {ι : Sort*} (f : M →* N) (s : ι → submonoid N) :
 @[simp, to_additive] lemma comap_top (f : M →* N) : (⊤ : submonoid N).comap f = ⊤ :=
 (gc_map_comap f).u_top
 
+@[simp, to_additive] lemma map_id (S : submonoid M) : S.map (monoid_hom.id M) = S :=
+ext (λ x, ⟨λ ⟨_, h, rfl⟩, h, λ h, ⟨_, h, rfl⟩⟩)
+
 /-- Given `submonoid`s `s`, `t` of monoids `M`, `N` respectively, `s × t` as a submonoid
 of `M × N`. -/
 @[to_additive prod "Given `add_submonoid`s `s`, `t` of `add_monoid`s `A`, `B` respectively, `s × t`
diff --git a/src/ring_theory/algebra.lean b/src/ring_theory/algebra.lean
index 9b230ebe2cea9..37761f0de3164 100644
--- a/src/ring_theory/algebra.lean
+++ b/src/ring_theory/algebra.lean
@@ -399,6 +399,9 @@ instance : inhabited (A₁ ≃ₐ[R] A₁) := ⟨1⟩
 @[refl]
 def refl : A₁ ≃ₐ[R] A₁ := 1
 
+@[simp] lemma coe_refl : (@refl R A₁ _ _ _ : A₁ →ₐ[R] A₁) = alg_hom.id R A₁ :=
+alg_hom.ext (λ x, rfl)
+
 /-- Algebra equivalences are symmetric. -/
 @[symm]
 def symm (e : A₁ ≃ₐ[R] A₂) : A₂ ≃ₐ[R] A₁ :=
@@ -418,6 +421,14 @@ def trans (e₁ : A₁ ≃ₐ[R] A₂) (e₂ : A₂ ≃ₐ[R] A₃) : A₁ ≃
 @[simp] lemma symm_apply_apply (e : A₁ ≃ₐ[R] A₂) : ∀ x, e.symm (e x) = x :=
   e.to_equiv.symm_apply_apply
 
+@[simp] lemma comp_symm (e : A₁ ≃ₐ[R] A₂) :
+  alg_hom.comp (e : A₁ →ₐ[R] A₂) ↑e.symm = alg_hom.id R A₂ :=
+by { ext, simp }
+
+@[simp] lemma symm_comp (e : A₁ ≃ₐ[R] A₂) :
+  alg_hom.comp ↑e.symm (e : A₁ →ₐ[R] A₂) = alg_hom.id R A₁ :=
+by { ext, simp }
+
 end alg_equiv
 
 namespace algebra
diff --git a/src/ring_theory/algebra_operations.lean b/src/ring_theory/algebra_operations.lean
index 6960afd00de96..2b3f0a0cb725d 100644
--- a/src/ring_theory/algebra_operations.lean
+++ b/src/ring_theory/algebra_operations.lean
@@ -126,6 +126,27 @@ begin
   exact mul_mem_mul hi hj
 end
 
+lemma map_mul {A'} [ring A'] [algebra R A'] (f : A →ₐ[R] A') :
+  map f.to_linear_map (M * N) = map f.to_linear_map M * map f.to_linear_map N :=
+calc map f.to_linear_map (M * N)
+    = ⨆ (i : M), (N.map (lmul R A i)).map f.to_linear_map : map_supr _ _
+... = map f.to_linear_map M * map f.to_linear_map N  :
+  begin
+    apply congr_arg Sup,
+    ext S,
+    split; rintros ⟨y, hy⟩,
+    { use [f y, mem_map.mpr ⟨y.1, y.2, rfl⟩],
+      refine trans _ hy,
+      ext,
+      simp },
+    { obtain ⟨y', hy', fy_eq⟩ := mem_map.mp y.2,
+      use [y', hy'],
+      refine trans _ hy,
+      rw f.to_linear_map_apply at fy_eq,
+      ext,
+      simp [fy_eq] }
+  end
+
 variables {M N P}
 
 instance : semiring (submodule R A) :=
diff --git a/src/ring_theory/fractional_ideal.lean b/src/ring_theory/fractional_ideal.lean
index b9bada9c83860..71245a305caf9 100644
--- a/src/ring_theory/fractional_ideal.lean
+++ b/src/ring_theory/fractional_ideal.lean
@@ -20,6 +20,7 @@ natural ring hom from `R` to `P`.
  * `comm_semiring (fractional_ideal f)` instance:
    the typical ideal operations generalized to fractional ideals
  * `lattice (fractional_ideal f)` instance
+ * `map` is the pushforward of a fractional ideal along an algebra morphism
 
 Let `K` be the localization of `R` at `R \ {0}` and `g` the natural ring hom from `R` to `K`.
  * `has_div (fractional_ideal g)` instance:
@@ -71,7 +72,7 @@ variables {R : Type*} [integral_domain R] {S : submonoid R} {P : Type*} [comm_ri
 
 /-- A submodule `I` is a fractional ideal if `a I ⊆ R` for some `a ≠ 0`. -/
 def is_fractional (I : submodule R f.codomain) :=
-∃ a ≠ (0 : R), ∀ b ∈ I, f.is_integer (f.to_map a * b)
+∃ a ∈ S, ∀ b ∈ I, f.is_integer (f.to_map a * b)
 
 /-- The fractional ideals of a domain `R` are ideals of `R` divided by some `a ∈ R`.
 
@@ -92,7 +93,11 @@ open submodule
 variables {R : Type*} [integral_domain R] {S : submonoid R} {P : Type*} [comm_ring P]
   {f : localization_map S P}
 
-instance : has_mem P (fractional_ideal f) := ⟨λ x I, x ∈ I.1⟩
+instance : has_coe (fractional_ideal f) (submodule R f.codomain) := ⟨λ I, I.val⟩
+
+@[simp] lemma val_eq_coe (I : fractional_ideal f) : I.val = I := rfl
+
+instance : has_mem P (fractional_ideal f) := ⟨λ x I, x ∈ (I : submodule R f.codomain)⟩
 
 /-- Fractional ideals are equal if their submodules are equal.
 
@@ -100,14 +105,14 @@ instance : has_mem P (fractional_ideal f) := ⟨λ x I, x ∈ I.1⟩
   they have the same elements.
 -/
 @[ext]
-lemma ext {I J : fractional_ideal f} : I.1 = J.1 → I = J :=
+lemma ext {I J : fractional_ideal f} : (I : submodule R f.codomain) = J → I = J :=
 subtype.ext.mpr
 
 lemma fractional_of_subset_one (I : submodule R f.codomain)
   (h : I ≤ (submodule.span R {1})) :
   is_fractional f I :=
 begin
-  use [1, one_ne_zero],
+  use [1, S.one_mem],
   intros b hb,
   rw [f.to_map.map_one, one_mul],
   rw ←submodule.one_eq_span at h,
@@ -121,7 +126,7 @@ instance coe_to_fractional_ideal : has_coe (ideal R) (fractional_ideal f) :=
   submodule.mem_span_singleton.2 ⟨y, by rw ←h; exact mul_one _⟩⟩ ⟩
 
 @[simp]
-lemma val_coe_ideal (I : ideal R) : (I : fractional_ideal f).1 = I := rfl
+lemma coe_coe_ideal (I : ideal R) : ((I : fractional_ideal f) : submodule R f.codomain) = I := rfl
 
 @[simp]
 lemma mem_coe {x : f.codomain} {I : ideal R} :
@@ -138,10 +143,11 @@ lemma mem_zero_iff {x : P} : x ∈ (0 : fractional_ideal f) ↔ x = 0 :=
     by simp [x'_eq_x.symm, x'_eq_zero]),
   (λ hx, ⟨0, rfl, by simp [hx]⟩) ⟩
 
-@[simp] lemma val_zero : (0 : fractional_ideal f).1 = 0 :=
+@[simp] lemma coe_zero : ↑(0 : fractional_ideal f) = (⊥ : submodule R f.codomain) :=
 submodule.ext $ λ _, mem_zero_iff
 
-lemma nonzero_iff_val_nonzero {I : fractional_ideal f} : I.1 ≠ 0 ↔ I ≠ 0 :=
+lemma coe_ne_bot_iff_nonzero {I : fractional_ideal f} :
+  ↑I ≠ (⊥ : submodule R f.codomain) ↔ I ≠ 0 :=
 ⟨ λ h h', h (by simp [h']),
   λ h h', h (ext (by simp [h'])) ⟩
 
@@ -159,7 +165,9 @@ mem_one_iff.mpr ⟨x, rfl⟩
 lemma one_mem_one : (1 : P) ∈ (1 : fractional_ideal f) :=
 mem_one_iff.mpr ⟨1, f.to_map.map_one⟩
 
-@[simp] lemma val_one : (1 : fractional_ideal f).1 = (1 : ideal R) := rfl
+@[simp] lemma coe_one :
+  ↑(1 : fractional_ideal f) = ((1 : ideal R) : submodule R f.codomain) :=
+rfl
 
 section lattice
 
@@ -202,7 +210,7 @@ begin
   rcases I.2 with ⟨aI, haI, hI⟩,
   rcases J.2 with ⟨aJ, haJ, hJ⟩,
   use aI * aJ,
-  use mul_ne_zero haI haJ,
+  use S.mul_mem haI haJ,
   intros b hb,
   rcases mem_sup.mp hb with
     ⟨bI, hbI, bJ, hbJ, hbIJ⟩,
@@ -248,14 +256,14 @@ instance : has_add (fractional_ideal f) := ⟨(⊔)⟩
 lemma sup_eq_add (I J : fractional_ideal f) : I ⊔ J = I + J := rfl
 
 @[simp]
-lemma val_add (I J : fractional_ideal f) : (I + J).1 = I.1 + J.1 := rfl
+lemma coe_add (I J : fractional_ideal f) : (↑(I + J) : submodule R f.codomain) = I + J := rfl
 
 lemma fractional_mul (I J : fractional_ideal f) : is_fractional f (I.1 * J.1) :=
 begin
   rcases I with ⟨I, aI, haI, hI⟩,
   rcases J with ⟨I, aJ, haJ, hJ⟩,
   use aI * aJ,
-  use mul_ne_zero haI haJ,
+  use S.mul_mem haI haJ,
   intros b hb,
   apply submodule.mul_induction_on hb,
   { intros m hm n hn,
@@ -278,7 +286,7 @@ end
 instance : has_mul (fractional_ideal f) := ⟨λ I J, ⟨I.1 * J.1, fractional_mul I J⟩⟩
 
 @[simp]
-lemma val_mul (I J : fractional_ideal f) : (I * J).1 = I.1 * J.1 := rfl
+lemma coe_mul (I J : fractional_ideal f) : (↑(I * J) : submodule R f.codomain) = I * J := rfl
 
 lemma mul_left_mono (I : fractional_ideal f) : monotone ((*) I) :=
 λ J J' h, mul_le.mpr (λ x hx y hy, mul_mem_mul hx (h hy))
@@ -336,6 +344,72 @@ instance comm_semiring : comm_semiring (fractional_ideal f) :=
   ..fractional_ideal.add_comm_monoid,
   ..fractional_ideal.comm_monoid }
 
+variables {P' : Type*} [comm_ring P'] {f' : localization_map S P'}
+variables {P'' : Type*} [comm_ring P''] {f'' : localization_map S P''}
+
+lemma fractional_map (g : f.codomain →ₐ[R] f'.codomain) (I : fractional_ideal f) :
+  is_fractional f' (submodule.map g.to_linear_map I.1) :=
+begin
+  rcases I with ⟨I, a, a_nonzero, hI⟩,
+  use [a, a_nonzero],
+  intros b hb,
+  obtain ⟨b', b'_mem, hb'⟩ := submodule.mem_map.mp hb,
+  obtain ⟨x, hx⟩ := hI b' b'_mem,
+  use x,
+  erw [←g.commutes, hx, g.map_smul, hb'],
+  refl
+end
+
+/-- `I.map g` is the pushforward of the fractional ideal `I` along the algebra morphism `g` -/
+def map (g : f.codomain →ₐ[R] f'.codomain) :
+  fractional_ideal f → fractional_ideal f' :=
+λ I, ⟨submodule.map g.to_linear_map I.1, fractional_map g I⟩
+
+@[simp] lemma coe_map (g : f.codomain →ₐ[R] f'.codomain) (I : fractional_ideal f) :
+  ↑(map g I) = submodule.map g.to_linear_map I := rfl
+
+@[simp] lemma map_id (I : fractional_ideal f) : I.map (alg_hom.id _ _) = I :=
+ext (submodule.map_id I.1)
+
+@[simp] lemma map_comp
+  (g : f.codomain →ₐ[R] f'.codomain) (g' : f'.codomain →ₐ[R] f''.codomain)
+  (I : fractional_ideal f) : I.map (g'.comp g) = (I.map g).map g' :=
+ext (submodule.map_comp g.to_linear_map g'.to_linear_map I.1)
+
+@[simp] lemma map_add (I J : fractional_ideal f) (g : f.codomain →ₐ[R] f'.codomain) :
+  (I + J).map g = I.map g + J.map g :=
+ext (submodule.map_sup _ _ _)
+
+@[simp] lemma map_mul (I J : fractional_ideal f) (g : f.codomain →ₐ[R] f'.codomain) :
+  (I * J).map g = I.map g * J.map g :=
+ext (submodule.map_mul _ _ _)
+
+/-- If `g` is an equivalence, `map g` is an isomorphism -/
+def map_equiv (g : f.codomain ≃ₐ[R] f'.codomain) :
+  fractional_ideal f ≃+* fractional_ideal f' :=
+{ to_fun := map g,
+  inv_fun := map g.symm,
+  map_add' := λ I J, map_add I J _,
+  map_mul' := λ I J, map_mul I J _,
+  left_inv := λ I, by { rw [←map_comp, alg_equiv.symm_comp, map_id] },
+  right_inv := λ I, by { rw [←map_comp, alg_equiv.comp_symm, map_id] } }
+
+@[simp] lemma map_equiv_apply (g : f.codomain ≃ₐ[R] f'.codomain) (I : fractional_ideal f) :
+  map_equiv g I = map ↑g I := rfl
+
+@[simp] lemma map_equiv_refl :
+  map_equiv alg_equiv.refl = ring_equiv.refl (fractional_ideal f) :=
+ring_equiv.ext (λ x, by simp)
+
+/-- `canonical_equiv f f'` is the canonical equivalence between the fractional
+ideals in `f.codomain` and in `f'.codomain` -/
+noncomputable def canonical_equiv (f f' : localization_map S P) :
+  fractional_ideal f ≃+* fractional_ideal f' :=
+map_equiv
+  { commutes' := λ r, ring_equiv_of_ring_equiv_eq _ _ _,
+    ..ring_equiv_of_ring_equiv f f' (ring_equiv.refl R)
+      (by rw [ring_equiv.to_monoid_hom_refl, submonoid.map_id]) }
+
 end semiring
 
 section quotient
@@ -370,11 +444,12 @@ begin
   obtain ⟨y', hy'⟩ := hJ y mem_J,
   use (aI * y'),
   split,
-  { apply mul_ne_zero haI,
+  { apply (non_zero_divisors R).mul_mem haI (mem_non_zero_divisors_iff_ne_zero.mpr _),
     intro y'_eq_zero,
     have : g.to_map aJ * y = 0 := by rw [←hy', y'_eq_zero, g.to_map.map_zero],
     obtain aJ_zero | y_zero := mul_eq_zero.mp this,
     { have : aJ = 0 := g.to_map.injective_iff.1 g.injective _ aJ_zero,
+      have : aJ ≠ 0 := mem_non_zero_divisors_iff_ne_zero.mp haJ,
       contradiction },
     { exact not_mem_zero (mem_zero_iff.mpr y_zero) } },
   intros b hb,
@@ -393,11 +468,11 @@ lemma div_nonzero {I J : fractional_ideal g} (h : J ≠ 0) :
 dif_neg h
 
 lemma inv_nonzero {I : fractional_ideal g} (h : I ≠ 0) :
-  I⁻¹ = ⟨(1 : fractional_ideal g).val / I.1, fractional_div_of_nonzero h⟩ :=
+  I⁻¹ = ⟨(1 : fractional_ideal g) / I, fractional_div_of_nonzero h⟩ :=
 div_nonzero h
 
-lemma val_inv_of_nonzero {I : fractional_ideal g} (h : I ≠ 0) :
-  I⁻¹.val = (1 : ideal R) / I.val :=
+lemma coe_inv_of_nonzero {I : fractional_ideal g} (h : I ≠ 0) :
+  (↑(I⁻¹) : submodule R g.codomain) = (1 : ideal R) / I :=
 by { rw inv_nonzero h, refl }
 
 @[simp] lemma div_one {I : fractional_ideal g} : I / 1 = I :=
@@ -455,34 +530,42 @@ open_locale classical
 open submodule submodule.is_principal
 
 lemma span_fractional_iff {s : set f.codomain} :
-  is_fractional f (span R s) ↔ ∃ (a ≠ (0 : R)), ∀ (b : P), b ∈ s → f.is_integer (f.to_map a * b) :=
-⟨ λ ⟨a, a_nonzero, h⟩, ⟨a, a_nonzero, λ b hb, h b (subset_span hb)⟩,
-  λ ⟨a, a_nonzero, h⟩, ⟨a, a_nonzero, λ b hb, span_induction hb
+  is_fractional f (span R s) ↔ ∃ a ∈ S, ∀ (b : P), b ∈ s → f.is_integer (f.to_map a * b) :=
+⟨ λ ⟨a, a_mem, h⟩, ⟨a, a_mem, λ b hb, h b (subset_span hb)⟩,
+  λ ⟨a, a_mem, h⟩, ⟨a, a_mem, λ b hb, span_induction hb
     h
     (is_integer_smul ⟨0, f.to_map.map_zero⟩)
     (λ x y hx hy, by { rw mul_add, exact is_integer_add hx hy })
     (λ s x hx, by { rw algebra.mul_smul_comm, exact is_integer_smul hx }) ⟩ ⟩
 
-lemma span_singleton_fractional {x : g.codomain} : is_fractional g (span R {x}) :=
-let ⟨a, ha⟩ := g.exists_integer_multiple x in
-span_fractional_iff.mpr
-  ⟨ a,
-    mem_non_zero_divisors_iff_ne_zero.mp a.2,
-    λ x hx, (mem_singleton_iff.mp hx).symm ▸ ha⟩
+lemma span_singleton_fractional (x : f.codomain) : is_fractional f (span R {x}) :=
+let ⟨a, ha⟩ := f.exists_integer_multiple x in
+span_fractional_iff.mpr ⟨ a.1, a.2, λ x hx, (mem_singleton_iff.mp hx).symm ▸ ha⟩
 
-/-- `span_singleton x` is the fractional ideal generated by `x` -/
-def span_singleton (x : g.codomain) : fractional_ideal g := ⟨span R {x}, span_singleton_fractional⟩
+/-- `span_singleton x` is the fractional ideal generated by `x` if `0 ∉ S` -/
+def span_singleton (x : f.codomain) : fractional_ideal f :=
+⟨span R {x}, span_singleton_fractional x⟩
 
-@[simp] lemma val_span_singleton (x : g.codomain) : (span_singleton x).val = span R {x} := rfl
+@[simp] lemma coe_span_singleton (x : f.codomain) :
+  (span_singleton x : submodule R f.codomain) = span R {x} := rfl
 
-lemma eq_span_singleton_of_principal (I : fractional_ideal g) [is_principal I.1] :
+lemma eq_span_singleton_of_principal (I : fractional_ideal f) [is_principal I.1] :
   I = span_singleton (generator I.1) :=
 ext (span_singleton_generator I.1).symm
 
-@[simp] lemma span_singleton_zero : span_singleton (0 : g.codomain) = 0 :=
+lemma is_principal_iff (I : fractional_ideal f) :
+  is_principal I.1 ↔ ∃ x, I = span_singleton x :=
+⟨ λ h, ⟨@generator _ _ _ _ _ I.1 h, @eq_span_singleton_of_principal _ _ _ _ _ _ I h⟩,
+  λ ⟨x, hx⟩, { principal := ⟨x, trans (congr_arg _ hx) (coe_span_singleton x)⟩ } ⟩
+
+@[simp] lemma span_singleton_zero : span_singleton (0 : f.codomain) = 0 :=
 by { ext, simp [submodule.mem_span_singleton, eq_comm] }
 
-@[simp] lemma span_singleton_one : span_singleton (1 : g.codomain) = 1 :=
+lemma span_singleton_eq_zero_iff {y : f.codomain} : span_singleton y = 0 ↔ y = 0 :=
+⟨ λ h, span_eq_bot.mp (by simpa using congr_arg subtype.val h) y (mem_singleton y),
+  λ h, by simp [h] ⟩
+
+@[simp] lemma span_singleton_one : span_singleton (1 : f.codomain) = 1 :=
 begin
   ext,
   refine mem_span_singleton.trans ((exists_congr _).trans mem_one_iff.symm),
@@ -491,16 +574,16 @@ begin
 end
 
 @[simp]
-lemma span_singleton_mul_span_singleton (x y : g.codomain) :
+lemma span_singleton_mul_span_singleton (x y : f.codomain) :
   span_singleton x * span_singleton y = span_singleton (x * y) :=
 begin
   ext,
-  simp_rw [val_mul, val_span_singleton, span_mul_span, singleton.is_mul_hom.map_mul]
+  simp_rw [coe_mul, coe_span_singleton, span_mul_span, singleton.is_mul_hom.map_mul]
 end
 
 @[simp]
-lemma coe_span_singleton (x : R) :
-  (↑(span R {x} : ideal R) : fractional_ideal g) = span_singleton (g.to_map x) :=
+lemma coe_ideal_span_singleton (x : R) :
+  (↑(span R {x} : ideal R) : fractional_ideal f) = span_singleton (f.to_map x) :=
 begin
   ext y,
   refine mem_coe.trans (iff.trans _ mem_span_singleton.symm),
@@ -508,13 +591,13 @@ begin
   { rintros ⟨y', hy', rfl⟩,
     obtain ⟨x', rfl⟩ := mem_span_singleton.mp hy',
     use x',
-    rw [smul_eq_mul, g.to_map.map_mul],
+    rw [smul_eq_mul, f.to_map.map_mul],
     refl },
   { rintros ⟨y', rfl⟩,
-    exact ⟨y' * x, mem_span_singleton.mpr ⟨y', rfl⟩, g.to_map.map_mul _ _⟩ }
+    exact ⟨y' * x, mem_span_singleton.mpr ⟨y', rfl⟩, f.to_map.map_mul _ _⟩ }
 end
 
-lemma mem_singleton_mul {x y : g.codomain} {I : fractional_ideal g} :
+lemma mem_singleton_mul {x y : f.codomain} {I : fractional_ideal f} :
   y ∈ span_singleton x * I ↔ ∃ y' ∈ I, y = x * y' :=
 begin
   split,
@@ -533,11 +616,10 @@ begin
     exact mul_mem_mul (mem_span_singleton.mpr ⟨1, one_smul _ _⟩) hy' }
 end
 
-lemma invertible_of_principal (I : fractional_ideal g)
+lemma mul_generator_self_inv (I : fractional_ideal g)
   [submodule.is_principal I.1] (h : I ≠ 0) :
-  I * I⁻¹ = 1 :=
+  I * span_singleton (generator I.1)⁻¹ = 1 :=
 begin
-  refine mul_inv_cancel_iff.mpr ⟨span_singleton (generator I.1)⁻¹, _⟩,
   -- Rewrite only the `I` that appears alone.
   conv_lhs { congr, rw eq_span_singleton_of_principal I },
   rw [span_singleton_mul_span_singleton, mul_inv_cancel, span_singleton_one],
@@ -550,6 +632,7 @@ lemma exists_eq_span_singleton_mul (I : fractional_ideal g) :
   ∃ (a : K) (aI : ideal R), I = span_singleton a * aI :=
 begin
   obtain ⟨a_inv, nonzero, ha⟩ := I.2,
+  have nonzero := mem_non_zero_divisors_iff_ne_zero.mp nonzero,
   have map_a_nonzero := mt g.to_map_eq_zero_iff.mpr nonzero,
   use (g.to_map a_inv)⁻¹,
   use (span_singleton (g.to_map a_inv) * I).1.comap g.lin_coe,
@@ -568,16 +651,16 @@ begin
     exact hy' }
 end
 
-instance is_principal {R} [principal_ideal_domain R] {g : fraction_map R K}
-  (I : fractional_ideal g) : I.val.is_principal :=
+instance is_principal {R} [principal_ideal_domain R] {f : fraction_map R K}
+  (I : fractional_ideal f) : (I : submodule R f.codomain).is_principal :=
 ⟨ begin
   obtain ⟨a, aI, ha⟩ := exists_eq_span_singleton_mul I,
-  have := a * g.to_map (generator aI),
-  use a * g.to_map (generator aI),
-  suffices : I = span_singleton (a * g.to_map (generator aI)),
+  have := a * f.to_map (generator aI),
+  use a * f.to_map (generator aI),
+  suffices : I = span_singleton (a * f.to_map (generator aI)),
   { exact congr_arg subtype.val this },
   conv_lhs { rw [ha, ←span_singleton_generator aI] },
-  rw [coe_span_singleton (generator aI), span_singleton_mul_span_singleton]
+  rw [coe_ideal_span_singleton (generator aI), span_singleton_mul_span_singleton]
 end ⟩
 
 end principal_ideal_domain