chore(Submonoid/Membership): don't import MonoidWithZero

See #10327 for the new copyright header

Mathlib.lean

@@ -296,6 +296,7 @@ import Mathlib.Algebra.Group.Hom.CompTypeclasses
 import Mathlib.Algebra.Group.Hom.Defs
 import Mathlib.Algebra.Group.Hom.End
 import Mathlib.Algebra.Group.Hom.Instances
+import Mathlib.Algebra.Group.Idempotent
 import Mathlib.Algebra.Group.Indicator
 import Mathlib.Algebra.Group.InjSurj
 import Mathlib.Algebra.Group.Int.Defs
@@ -389,6 +390,7 @@ import Mathlib.Algebra.GroupWithZero.Conj
 import Mathlib.Algebra.GroupWithZero.Defs
 import Mathlib.Algebra.GroupWithZero.Divisibility
 import Mathlib.Algebra.GroupWithZero.Hom
+import Mathlib.Algebra.GroupWithZero.Idempotent
 import Mathlib.Algebra.GroupWithZero.Indicator
 import Mathlib.Algebra.GroupWithZero.InjSurj
 import Mathlib.Algebra.GroupWithZero.Invertible
@@ -402,6 +404,7 @@ import Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic
 import Mathlib.Algebra.GroupWithZero.Pointwise.Set.Card
 import Mathlib.Algebra.GroupWithZero.Prod
 import Mathlib.Algebra.GroupWithZero.Semiconj
+import Mathlib.Algebra.GroupWithZero.Submonoid
 import Mathlib.Algebra.GroupWithZero.ULift
 import Mathlib.Algebra.GroupWithZero.Units.Basic
 import Mathlib.Algebra.GroupWithZero.Units.Equiv
@@ -905,7 +908,7 @@ import Mathlib.Algebra.Ring.Ext
 import Mathlib.Algebra.Ring.Fin
 import Mathlib.Algebra.Ring.Hom.Basic
 import Mathlib.Algebra.Ring.Hom.Defs
-import Mathlib.Algebra.Ring.Idempotents
+import Mathlib.Algebra.Ring.Idempotent
 import Mathlib.Algebra.Ring.Identities
 import Mathlib.Algebra.Ring.InjSurj
 import Mathlib.Algebra.Ring.Int.Defs
@@ -925,6 +928,7 @@ import Mathlib.Algebra.Ring.Rat
 import Mathlib.Algebra.Ring.Regular
 import Mathlib.Algebra.Ring.Semiconj
 import Mathlib.Algebra.Ring.Semireal.Defs
+import Mathlib.Algebra.Ring.Submonoid
 import Mathlib.Algebra.Ring.Subring.Basic
 import Mathlib.Algebra.Ring.Subring.Defs
 import Mathlib.Algebra.Ring.Subring.IntPolynomial

Mathlib/Algebra/Group/Idempotent.lean

@@ -0,0 +1,98 @@
+/-
+Copyright (c) 2022 Christopher Hoskin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christopher Hoskin
+-/
+import Mathlib.Algebra.Group.Basic
+import Mathlib.Algebra.Group.Commute.Defs
+import Mathlib.Algebra.Group.Hom.Defs
+import Mathlib.Data.Subtype
+import Mathlib.Tactic.MinImports
+
+/-!
+# Idempotents
+
+This file defines idempotents for an arbitrary multiplication and proves some basic results,
+including:
+
+* `IsIdempotentElem.mul_of_commute`: In a semigroup, the product of two commuting idempotents is
+  an idempotent;
+* `IsIdempotentElem.pow_succ_eq`: In a monoid `a ^ (n+1) = a` for `a` an idempotent and `n` a
+  natural number.
+
+## Tags
+
+projection, idempotent
+-/
+
+assert_not_exists GroupWithZero
+
+variable {M N S : Type*}
+
+/-- An element `a` is said to be idempotent if `a * a = a`. -/
+def IsIdempotentElem [Mul M] (a : M) : Prop := a * a = a
+
+namespace IsIdempotentElem
+section Mul
+variable [Mul M] {a : M}
+
+lemma of_isIdempotent [Std.IdempotentOp (α := M) (· * ·)] (a : M) : IsIdempotentElem a :=
+  Std.IdempotentOp.idempotent a
+
+lemma eq (ha : IsIdempotentElem a) : a * a = a := ha
+
+end Mul
+
+section Semigroup
+variable [Semigroup S] {a b : S}
+
+lemma mul_of_commute (hab : Commute a b) (ha : IsIdempotentElem a) (hb : IsIdempotentElem b) :
+    IsIdempotentElem (a * b) := by rw [IsIdempotentElem, hab.symm.mul_mul_mul_comm, ha.eq, hb.eq]
+
+end Semigroup
+
+section CommSemigroup
+variable [CommSemigroup S] {a b : S}
+
+lemma mul (ha : IsIdempotentElem a) (hb : IsIdempotentElem b) : IsIdempotentElem (a * b) :=
+  ha.mul_of_commute (.all ..) hb
+
+end CommSemigroup
+
+section MulOneClass
+variable [MulOneClass M] {a : M}
+
+lemma one : IsIdempotentElem (1 : M) := mul_one _
+
+instance : One {a : M // IsIdempotentElem a} where one := ⟨1, one⟩
+
+@[simp, norm_cast] lemma coe_one : ↑(1 : {a : M // IsIdempotentElem a}) = (1 : M) := rfl
+
+end MulOneClass
+
+section Monoid
+variable [Monoid M] {a : M}
+
+lemma pow (n : ℕ) (h : IsIdempotentElem a) : IsIdempotentElem (a ^ n) :=
+  Nat.recOn n ((pow_zero a).symm ▸ one) fun n _ =>
+    show a ^ n.succ * a ^ n.succ = a ^ n.succ by
+      conv_rhs => rw [← h.eq] -- Porting note: was `nth_rw 3 [← h.eq]`
+      rw [← sq, ← sq, ← pow_mul, ← pow_mul']
+
+lemma pow_succ_eq (n : ℕ) (h : IsIdempotentElem a) : a ^ (n + 1) = a :=
+  Nat.recOn n ((Nat.zero_add 1).symm ▸ pow_one a) fun n ih => by rw [pow_succ, ih, h.eq]
+
+end Monoid
+
+section CancelMonoid
+variable [CancelMonoid M] {a : M}
+
+@[simp] lemma iff_eq_one : IsIdempotentElem a ↔ a = 1 := by simp [IsIdempotentElem]
+
+end CancelMonoid
+
+lemma map {M N F} [Mul M] [Mul N] [FunLike F M N] [MulHomClass F M N] {e : M}
+    (he : IsIdempotentElem e) (f : F) : IsIdempotentElem (f e) := by
+  rw [IsIdempotentElem, ← map_mul, he.eq]
+
+end IsIdempotentElem

Mathlib/Algebra/Group/Submonoid/Membership.lean

@@ -5,14 +5,11 @@ Authors: Johannes Hölzl, Kenny Lau, Johan Commelin, Mario Carneiro, Kevin Buzza
 Amelia Livingston, Yury Kudryashov
 -/
 import Mathlib.Algebra.FreeMonoid.Basic
+import Mathlib.Algebra.Group.Idempotent
 import Mathlib.Algebra.Group.Nat.Hom
 import Mathlib.Algebra.Group.Submonoid.MulOpposite
 import Mathlib.Algebra.Group.Submonoid.Operations
-import Mathlib.Algebra.GroupWithZero.Divisibility
-import Mathlib.Algebra.Ring.Idempotents
-import Mathlib.Algebra.Ring.Int.Defs
 import Mathlib.Data.Fintype.Card
-import Mathlib.Data.Nat.Cast.Basic
 
 /-!
 # Submonoids: membership criteria
@@ -33,6 +30,7 @@ In this file we prove various facts about membership in a submonoid:
 submonoid, submonoids
 -/
 
+assert_not_exists MonoidWithZero
 -- We don't need ordered structures to establish basic membership facts for submonoids
 assert_not_exists OrderedSemiring
 
@@ -334,7 +332,7 @@ abbrev groupPowers {x : M} {n : ℕ} (hpos : 0 < n) (hx : x ^ n = 1) : Group (po
     simp only [← pow_mul, Int.natMod, SubmonoidClass.coe_pow]
     rw [Int.negSucc_coe, ← Int.add_mul_emod_self (b := (m + 1 : ℕ))]
     nth_rw 1 [← mul_one ((m + 1 : ℕ) : ℤ)]
-    rw [← sub_eq_neg_add, ← mul_sub, ← Int.natCast_pred_of_pos hpos]; norm_cast
+    rw [← sub_eq_neg_add, ← Int.mul_sub, ← Int.natCast_pred_of_pos hpos]; norm_cast
     simp only [Int.toNat_natCast]
     rw [mul_comm, pow_mul, ← pow_eq_pow_mod _ hx, mul_comm k, mul_assoc, pow_mul _ (_ % _),
       ← pow_eq_pow_mod _ hx, pow_mul, pow_mul]
@@ -483,40 +481,6 @@ an additive group if that element has finite order."] Submonoid.groupPowers
 
 end AddSubmonoid
 
-/-! Lemmas about additive closures of `Subsemigroup`. -/
-
-
-namespace MulMemClass
-
-variable {R : Type*} [NonUnitalNonAssocSemiring R] [SetLike M R] [MulMemClass M R] {S : M}
-  {a b : R}
-
-/-- The product of an element of the additive closure of a multiplicative subsemigroup `M`
-and an element of `M` is contained in the additive closure of `M`. -/
-theorem mul_right_mem_add_closure (ha : a ∈ AddSubmonoid.closure (S : Set R)) (hb : b ∈ S) :
-    a * b ∈ AddSubmonoid.closure (S : Set R) := by
-  induction ha using AddSubmonoid.closure_induction with
-  | mem r hr => exact AddSubmonoid.mem_closure.mpr fun y hy => hy (mul_mem hr hb)
-  | one => simp only [zero_mul, zero_mem _]
-  | mul r s _ _ hr hs => simpa only [add_mul] using add_mem hr hs
-
-/-- The product of two elements of the additive closure of a submonoid `M` is an element of the
-additive closure of `M`. -/
-theorem mul_mem_add_closure (ha : a ∈ AddSubmonoid.closure (S : Set R))
-    (hb : b ∈ AddSubmonoid.closure (S : Set R)) : a * b ∈ AddSubmonoid.closure (S : Set R) := by
-  induction hb using AddSubmonoid.closure_induction with
-  | mem r hr => exact MulMemClass.mul_right_mem_add_closure ha hr
-  | one => simp only [mul_zero, zero_mem _]
-  | mul r s _ _ hr hs => simpa only [mul_add] using add_mem hr hs
-
-/-- The product of an element of `S` and an element of the additive closure of a multiplicative
-submonoid `S` is contained in the additive closure of `S`. -/
-theorem mul_left_mem_add_closure (ha : a ∈ S) (hb : b ∈ AddSubmonoid.closure (S : Set R)) :
-    a * b ∈ AddSubmonoid.closure (S : Set R) :=
-  mul_mem_add_closure (AddSubmonoid.mem_closure.mpr fun _sT hT => hT ha) hb
-
-end MulMemClass
-
 namespace Submonoid
 
 /-- An element is in the closure of a two-element set if it is a linear combination of those two
@@ -552,9 +516,3 @@ theorem ofAdd_image_multiples_eq_powers_ofAdd [AddMonoid A] {x : A} :
   exact ofMul_image_powers_eq_multiples_ofMul
 
 end mul_add
-
-/-- The submonoid of primal elements in a cancellative commutative monoid with zero. -/
-def Submonoid.isPrimal (α) [CancelCommMonoidWithZero α] : Submonoid α where
-  carrier := {a | IsPrimal a}
-  mul_mem' := IsPrimal.mul
-  one_mem' := isUnit_one.isPrimal

Mathlib/Algebra/GroupWithZero/Idempotent.lean

@@ -0,0 +1,53 @@
+/-
+Copyright (c) 2022 Christopher Hoskin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christopher Hoskin
+-/
+import Mathlib.Algebra.Group.Idempotent
+import Mathlib.Algebra.GroupWithZero.Defs
+
+/-!
+# Idempotents
+
+This file defines idempotents for an arbitrary multiplication and proves some basic results,
+including:
+
+* `IsIdempotentElem.mul_of_commute`: In a semigroup, the product of two commuting idempotents is
+  an idempotent;
+* `IsIdempotentElem.one_sub_iff`: In a (non-associative) ring, `p` is an idempotent if and only if
+  `1-p` is an idempotent.
+* `IsIdempotentElem.pow_succ_eq`: In a monoid `p ^ (n+1) = p` for `p` an idempotent and `n` a
+  natural number.
+
+## Tags
+
+projection, idempotent
+-/
+
+assert_not_exists Ring
+
+variable {M N S M₀ M₁ R G G₀ : Type*}
+variable [MulOneClass M₁] [CancelMonoidWithZero G₀]
+
+namespace IsIdempotentElem
+section MulZeroClass
+variable [MulZeroClass M₀]
+
+lemma zero : IsIdempotentElem (0 : M₀) := mul_zero _
+
+instance : Zero { p : M₀ // IsIdempotentElem p } where zero := ⟨0, zero⟩
+
+@[simp] lemma coe_zero : ↑(0 : { p : M₀ // IsIdempotentElem p }) = (0 : M₀) := rfl
+
+end MulZeroClass
+
+section CancelMonoidWithZero
+variable [CancelMonoidWithZero M₀]
+
+@[simp]
+lemma iff_eq_zero_or_one {p : G₀} : IsIdempotentElem p ↔ p = 0 ∨ p = 1 where
+  mp h := or_iff_not_imp_left.mpr fun hp ↦ mul_left_cancel₀ hp (h.trans (mul_one p).symm)
+  mpr h := h.elim (fun hp => hp.symm ▸ zero) fun hp => hp.symm ▸ one
+
+end CancelMonoidWithZero
+end IsIdempotentElem

Mathlib/Algebra/GroupWithZero/Submonoid.lean

@@ -0,0 +1,17 @@
+/-
+Copyright (c) 2024 Junyan Xu. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Junyan Xu
+-/
+import Mathlib.Algebra.Group.Submonoid.Membership
+import Mathlib.Algebra.GroupWithZero.Divisibility
+
+/-!
+# Submonoid of primal elements
+-/
+
+/-- The submonoid of primal elements in a cancellative commutative monoid with zero. -/
+def Submonoid.isPrimal (M₀ : Type*) [CancelCommMonoidWithZero M₀] : Submonoid M₀ where
+  carrier := {a | IsPrimal a}
+  mul_mem' := .mul
+  one_mem' := isUnit_one.isPrimal

Mathlib/Algebra/Ring/Idempotent.lean

@@ -0,0 +1,87 @@
+/-
+Copyright (c) 2022 Christopher Hoskin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Christopher Hoskin
+-/
+import Mathlib.Algebra.GroupWithZero.Idempotent
+import Mathlib.Algebra.Ring.Defs
+import Mathlib.Order.Notation
+
+/-!
+# Idempotents
+
+This file defines idempotents for an arbitrary multiplication and proves some basic results,
+including:
+
+* `IsIdempotentElem.mul_of_commute`: In a semigroup, the product of two commuting idempotents is
+  an idempotent;
+* `IsIdempotentElem.one_sub_iff`: In a (non-associative) ring, `a` is an idempotent if and only if
+  `1-a` is an idempotent.
+* `IsIdempotentElem.pow_succ_eq`: In a monoid `a ^ (n+1) = a` for `a` an idempotent and `n` a
+  natural number.
+
+## Tags
+
+projection, idempotent
+-/
+
+variable {R : Type*}
+
+namespace IsIdempotentElem
+section NonAssocRing
+variable [NonAssocRing R] {a : R}
+
+lemma one_sub (h : IsIdempotentElem a) : IsIdempotentElem (1 - a) := by
+  rw [IsIdempotentElem, mul_sub, mul_one, sub_mul, one_mul, h.eq, sub_self, sub_zero]
+
+@[simp]
+lemma one_sub_iff : IsIdempotentElem (1 - a) ↔ IsIdempotentElem a :=
+  ⟨fun h => sub_sub_cancel 1 a ▸ h.one_sub, IsIdempotentElem.one_sub⟩
+
+@[simp]
+lemma mul_one_sub_self (h : IsIdempotentElem a) : a * (1 - a) = 0 := by
+  rw [mul_sub, mul_one, h.eq, sub_self]
+
+@[simp]
+lemma one_sub_mul_self (h : IsIdempotentElem a) : (1 - a) * a = 0 := by
+  rw [sub_mul, one_mul, h.eq, sub_self]
+
+instance : HasCompl {a : R // IsIdempotentElem a} where compl a := ⟨1 - a, a.prop.one_sub⟩
+
+@[simp] lemma coe_compl (a : {a : R // IsIdempotentElem a}) : ↑aᶜ = (1 : R) - ↑a := rfl
+
+@[simp] lemma compl_compl (a : {a : R // IsIdempotentElem a}) : aᶜᶜ = a := by ext; simp
+@[simp] lemma zero_compl : (0 : {a : R // IsIdempotentElem a})ᶜ = 1 := by ext; simp
+@[simp] lemma one_compl : (1 : {a : R // IsIdempotentElem a})ᶜ = 0 := by ext; simp
+
+end NonAssocRing
+
+section Semiring
+variable [Semiring R] {a b : R}
+
+lemma of_mul_add (mul : a * b = 0) (add : a + b = 1) : IsIdempotentElem a ∧ IsIdempotentElem b := by
+  simp_rw [IsIdempotentElem]; constructor
+  · conv_rhs => rw [← mul_one a, ← add, mul_add, mul, add_zero]
+  · conv_rhs => rw [← one_mul b, ← add, add_mul, mul, zero_add]
+
+end Semiring
+
+section Ring
+variable [Ring R] {a b : R}
+
+lemma add_sub_mul_of_commute (h : Commute a b) (hp : IsIdempotentElem a) (hq : IsIdempotentElem b) :
+    IsIdempotentElem (a + b - a * b) := by
+  convert (hp.one_sub.mul_of_commute ?_ hq.one_sub).one_sub using 1
+  · simp_rw [sub_mul, mul_sub, one_mul, mul_one, sub_sub, sub_sub_cancel, add_sub, add_comm]
+  · simp_rw [commute_iff_eq, sub_mul, mul_sub, one_mul, mul_one, sub_sub, add_sub, add_comm, h.eq]
+
+end Ring
+
+section CommRing
+variable [CommRing R] {a b : R}
+
+lemma add_sub_mul (hp : IsIdempotentElem a) (hq : IsIdempotentElem b) :
+    IsIdempotentElem (a + b - a * b) := add_sub_mul_of_commute (.all ..) hp hq
+
+end CommRing
+end IsIdempotentElem