feat(algebra/{lie/subalgebra,module/submodule/pointwise}): submodules…

… and lie subalgebras form canonically ordered additive monoids under addition (#14529)

We can't actually make these instances because they result in loops for `simp`.

The `le_iff_exists_sup` lemma is probably not very useful for much beyond these new instances, but it matches `le_iff_exists_add`.

src/algebra/lie/subalgebra.lean

@@ -378,6 +378,13 @@ instance : add_comm_monoid (lie_subalgebra R L) :=
   add_zero  := λ _, sup_bot_eq,
   add_comm  := λ _ _, sup_comm, }
 
+/-- This is not an instance, as it would stop `⊥` being the simp-normal form (via `bot_eq_zero`). -/
+def canonically_ordered_add_monoid : canonically_ordered_add_monoid (lie_subalgebra R L) :=
+{ add_le_add_left := λ a b, sup_le_sup_left,
+  le_iff_exists_add := λ a b, le_iff_exists_sup,
+  ..lie_subalgebra.add_comm_monoid,
+  ..lie_subalgebra.complete_lattice }
+
 @[simp] lemma add_eq_sup : K + K' = K ⊔ K' := rfl
 
 @[norm_cast, simp] lemma inf_coe_to_submodule :

src/algebra/module/submodule/pointwise.lean

@@ -136,6 +136,22 @@ instance pointwise_add_comm_monoid : add_comm_monoid (submodule R M) :=
 @[simp] lemma add_eq_sup (p q : submodule R M) : p + q = p ⊔ q := rfl
 @[simp] lemma zero_eq_bot : (0 : submodule R M) = ⊥ := rfl
 
+/-- This is not an instance, as it would form a simp loop between `bot_eq_zero` and
+`submodule.zero_eq_bot`. It can be safely enabled with
+```lean
+local attribute [-simp] submodule.zero_eq_bot
+local attribute [instance] canonically_ordered_add_monoid
+```
+-/
+def canonically_ordered_add_monoid : canonically_ordered_add_monoid (submodule R M) :=
+{ zero := 0,
+  bot := ⊥,
+  add := (+),
+  add_le_add_left := λ a b, sup_le_sup_left,
+  le_iff_exists_add := λ a b, le_iff_exists_sup,
+  ..submodule.pointwise_add_comm_monoid,
+  ..submodule.complete_lattice }
+
 section
 variables [monoid α] [distrib_mul_action α M] [smul_comm_class α R M]
 

src/order/lattice.lean

@@ -183,6 +183,14 @@ le_sup_right.lt_iff_ne.trans $ not_congr right_eq_sup
 lemma left_or_right_lt_sup (h : a ≠ b) : (a < a ⊔ b ∨ b < a ⊔ b) :=
 h.not_le_or_not_le.symm.imp left_lt_sup.2 right_lt_sup.2
 
+theorem le_iff_exists_sup : a ≤ b ↔ ∃ c, b = a ⊔ c :=
+begin
+  split,
+  { intro h, exact ⟨b, (sup_eq_right.mpr h).symm⟩ },
+  { rintro ⟨c, (rfl : _ = _ ⊔ _)⟩,
+    exact le_sup_left }
+end
+
 theorem sup_le_sup (h₁ : a ≤ b) (h₂ : c ≤ d) : a ⊔ c ≤ b ⊔ d :=
 sup_le (le_sup_of_le_left h₁) (le_sup_of_le_right h₂)
 

src/ring_theory/ideal/operations.lean

@@ -1522,7 +1522,7 @@ end
 
 theorem map_is_prime_of_equiv (f : R ≃+* S) {I : ideal R} [is_prime I] :
   is_prime (map (f : R →+* S) I) :=
-map_is_prime_of_surjective f.surjective $ by simp
+map_is_prime_of_surjective f.surjective $ by simp only [ring_hom.ker_coe_equiv, bot_le]
 
 end ring
 

src/ring_theory/nilpotent.lean

@@ -146,7 +146,7 @@ lemma mem_nilradical : x ∈ nilradical R ↔ is_nilpotent x := iff.rfl
 
 lemma nilradical_eq_Inf (R : Type*) [comm_semiring R] :
   nilradical R = Inf { J : ideal R | J.is_prime } :=
-by { convert ideal.radical_eq_Inf 0, simp }
+(ideal.radical_eq_Inf ⊥).trans $ by simp_rw and_iff_right bot_le
 
 lemma nilpotent_iff_mem_prime : is_nilpotent x ↔ ∀ (J : ideal R), J.is_prime → x ∈ J :=
 by { rw [← mem_nilradical, nilradical_eq_Inf, submodule.mem_Inf], refl }