feat(ring_theory/ideal/operations): add lemmas about comap (#10418)

This also adds `ring_hom.to_semilinear_map` and `ring_equiv.to_semilinear_equiv`.

src/algebra/module/linear_map.lean

@@ -258,6 +258,13 @@ theorem ext_ring_iff {σ : R →+* R} {f g : R →ₛₗ[σ] M} : f = g ↔ f 1
 
 end
 
+/-- Interpret a `ring_hom` `f` as an `f`-semilinear map. -/
+@[simps]
+def _root_.ring_hom.to_semilinear_map (f : R →+* S) : R →ₛₗ[f] S :=
+{ to_fun := f,
+  map_smul' := f.map_mul,
+  .. f}
+
 section
 
 variables [semiring R₁] [semiring R₂] [semiring R₃]

src/data/equiv/module.lean

@@ -311,6 +311,17 @@ omit σ'
 
 end
 
+/-- Interpret a `ring_equiv` `f` as an `f`-semilinear equiv. -/
+@[simps]
+def _root_.ring_equiv.to_semilinear_equiv (f : R ≃+* S) :
+  by haveI := ring_hom_inv_pair.of_ring_equiv f;
+     haveI := ring_hom_inv_pair.symm (↑f : R →+* S) (f.symm : S →+* R);
+     exact (R ≃ₛₗ[(↑f : R →+* S)] S) :=
+by exact
+{ to_fun := f,
+  map_smul' := f.map_mul,
+  .. f}
+
 variables [semiring R₁] [semiring R₂] [semiring R₃]
 variables [add_comm_monoid M] [add_comm_monoid M₁] [add_comm_monoid M₂]
 

src/ring_theory/ideal/operations.lean

@@ -767,8 +767,7 @@ span (f '' I)
 /-- `I.comap f` is the preimage of `I` under `f`. -/
 def comap (I : ideal S) : ideal R :=
 { carrier := f ⁻¹' I,
-  smul_mem' := λ c x hx, show f (c * x) ∈ I, by { rw f.map_mul, exact I.mul_mem_left _ hx },
-  .. I.to_add_submonoid.comap (f : R →+ S) }
+  .. I.comap f.to_semilinear_map }
 
 variables {f}
 theorem map_mono (h : I ≤ J) : map f I ≤ map f J :=
@@ -794,6 +793,29 @@ theorem comap_ne_top (hK : K ≠ ⊤) : comap f K ≠ ⊤ :=
 (ne_top_iff_one _).2 $ by rw [mem_comap, f.map_one];
   exact (ne_top_iff_one _).1 hK
 
+lemma map_le_comap_of_inv_on (g : S →+* R) (I : ideal R) (hf : set.left_inv_on g f I) :
+  I.map f ≤ I.comap g :=
+begin
+  refine ideal.span_le.2 _,
+  rintros x ⟨x, hx, rfl⟩,
+  rw [set_like.mem_coe, mem_comap, hf hx],
+  exact hx,
+end
+
+lemma comap_le_map_of_inv_on (g : S →+* R) (I : ideal S) (hf : set.left_inv_on g f (f ⁻¹' I)) :
+  I.comap f ≤ I.map g :=
+λ x (hx : f x ∈ I), hf hx ▸ ideal.mem_map_of_mem g hx
+
+/-- The `ideal` version of `set.image_subset_preimage_of_inverse`. -/
+lemma map_le_comap_of_inverse (g : S →+* R) (I : ideal R) (h : function.left_inverse g f) :
+  I.map f ≤ I.comap g :=
+map_le_comap_of_inv_on _ _ _ $ h.left_inv_on _
+
+/-- The `ideal` version of `set.preimage_subset_image_of_inverse`. -/
+lemma comap_le_map_of_inverse (g : S →+* R) (I : ideal S) (h : function.left_inverse g f) :
+  I.comap f ≤ I.map g :=
+comap_le_map_of_inv_on _ _ _ $ h.left_inv_on _
+
 instance is_prime.comap [hK : K.is_prime] : (comap f K).is_prime :=
 ⟨comap_ne_top _ hK.1, λ x y,
   by simp only [mem_comap, f.map_mul]; apply hK.2⟩
@@ -1160,10 +1182,10 @@ end ideal
 
 namespace ring_hom
 
-variables {R : Type u} {S : Type v}
+variables {R : Type u} {S : Type v} {T : Type v}
 
 section semiring
-variables [semiring R] [semiring S] (f : R →+* S)
+variables [semiring R] [semiring S] [semiring T] (f : R →+* S) (g : T →+* S)
 
 /-- Kernel of a ring homomorphism as an ideal of the domain. -/
 def ker : ideal R := ideal.comap f ⊥
@@ -1176,6 +1198,9 @@ lemma ker_eq : ((ker f) : set R) = set.preimage f {0} := rfl
 
 lemma ker_eq_comap_bot (f : R →+* S) : f.ker = ideal.comap f ⊥ := rfl
 
+lemma comap_ker (f : S →+* R) : f.ker.comap g = (f.comp g).ker :=
+by rw [ring_hom.ker_eq_comap_bot, ideal.comap_comap, ring_hom.ker_eq_comap_bot]
+
 /-- If the target is not the zero ring, then one is not in the kernel.-/
 lemma not_one_mem_ker [nontrivial S] (f : R →+* S) : (1:R) ∉ ker f :=
 by { rw [mem_ker, f.map_one], exact one_ne_zero }