feat(ring_theory/fractional_ideal): pushforward of fractional ideals (#…

…2984)

Extend `submodule.map` to fractional ideals by showing that the pushforward is also fractional.

For this, we need a slightly tweaked definition of fractional ideal: if we localize `R` at the submonoid `S`, the old definition required a nonzero `x : R` such that `xI ≤ R`, and the new definition requires `x ∈ S` instead. In the most common case, `S = non_zero_divisors R`, the results are exactly the same, and all operations are still the same.

A practical use of these pushforwards is included: `canonical_equiv` states fractional ideals don't depend on choice of localization map.

Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>

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

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`

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

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