feat(ring_theory/power_series): order (#1292)

* First start on power_series * Innocent changes * Almost a comm_semiring * Defined hom from mv_polynomial to mv_power_series; sorrys remain * Attempt that seem to go nowhere * Working on coeff_mul for polynomials * Small progress * Finish mv_polynomial.coeff_mul * Cleaner proof of mv_polynomial.coeff_mul * Fix build * WIP * Finish proof of mul_assoc * WIP * Golfing coeff_mul * WIP * Crazy wf is crazy * mv_power_series over local ring is local * WIP * Add empty line * wip * wip * WIP * WIP * WIP * Add header comments * WIP * WIP * Fix finsupp build * Fix build, hopefully * Fix build: ideals * More docs * Update src/data/power_series.lean Fix typo. * Fix build -- bump instance search depth * Make changes according to some of the review comments * Use 'formal' in the names * Use 'protected' in more places, remove '@simp's * Make 'inv_eq_zero' an iff * Generalize to non-commutative scalars * Order of a power series * Start on formal Laurent series * WIP * Remove file. It's for another PR. * Add stuff about order * Remove old file * Basics on order of power series * Lots of stuff * Move stuff on kernels * Move stuff on ker to the right place * Fix build * Add elim_cast attributes, update documentation * Bundle homs * Fix build * Remove duplicate trunc_C * Fix build
leanprover-community · Sep 30, 2019 · c6fab42 · c6fab42
1 parent 30aa8d2
commit c6fab42
Show file tree

Hide file tree

Showing 2 changed files with 920 additions and 514 deletions.
diff --git a/src/ring_theory/ideal_operations.lean b/src/ring_theory/ideal_operations.lean
@@ -555,11 +555,17 @@ end ideal
 
 namespace is_ring_hom
 
-variables {R : Type u} {S : Type v} [comm_ring R] [comm_ring S]
-variables (f : R → S) [is_ring_hom f]
+variables {R : Type u} {S : Type v} (f : R → S) [comm_ring R]
+
+section comm_ring
+variables [comm_ring S] [is_ring_hom f]
 
 def ker : ideal R := ideal.comap f ⊥
 
+/-- An element is in the kernel if and only if it maps to zero.-/
+lemma mem_ker {r} : r ∈ ker f ↔ f r = 0 :=
+by rw [ker, ideal.mem_comap, submodule.mem_bot]
+
 lemma ker_eq : ((ker f) : set R) = is_add_group_hom.ker f := rfl
 
 lemma inj_iff_ker_eq_bot : function.injective f ↔ ker f = ⊥ :=
@@ -571,6 +577,18 @@ by rw [←submodule.ext'_iff, ker_eq]; exact is_add_group_hom.trivial_ker_iff_eq
 lemma injective_iff : function.injective f ↔ ∀ x, f x = 0 → x = 0 :=
 is_add_group_hom.injective_iff f
 
+end comm_ring
+
+/-- If the target is not the zero ring, then one is not in the kernel.-/
+lemma not_one_mem_ker [nonzero_comm_ring S] [is_ring_hom f] : (1:R) ∉ ker f :=
+by { rw [mem_ker, is_ring_hom.map_one f], exact one_ne_zero }
+
+/-- The kernel of a homomorphism to an integral domain is a prime ideal.-/
+lemma ker_is_prime [integral_domain S] [is_ring_hom f] :
+  (ker f).is_prime :=
+⟨by { rw [ne.def, ideal.eq_top_iff_one], exact not_one_mem_ker f },
+λ x y, by simpa only [mem_ker, is_ring_hom.map_mul f] using eq_zero_or_eq_zero_of_mul_eq_zero⟩
+
 end is_ring_hom
 
 namespace submodule