/-
Copyright (c) 2021 Eric Wieser. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Eric Wieser

! This file was ported from Lean 3 source module group_theory.submonoid.center
! leanprover-community/mathlib commit 6cb77a8eaff0ddd100e87b1591c6d3ad319514ff
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.GroupTheory.Submonoid.Operations
import Mathlib.GroupTheory.Subsemigroup.Center

/-!
# Centers of monoids

## Main definitions

* `Submonoid.center`: the center of a monoid
* `AddSubmonoid.center`: the center of an additive monoid

We provide `Subgroup.center`, `AddSubgroup.center`, `Subsemiring.center`, and `Subring.center` in
other files.
-/


namespace Submonoid

section

variable (
M: Type ?u.8
M : 
Type _: Type (?u.1801+1)
Type _) [
Monoid: Type ?u.5 → Type ?u.5
Monoid 
M: Type ?u.575
M]

/-- The center of a monoid `M` is the set of elements that commute with everything in `M` -/
@[
to_additive: (M : Type u_1) → [inst : AddMonoid M] → AddSubmonoid M
to_additive
      "The center of a monoid `M` is the set of elements that commute with everything in `M`"]
def 
center: (M : Type u_1) → [inst : Monoid M] → Submonoid M
center : 
Submonoid: (M : Type ?u.14) → [inst : MulOneClass M] → Type ?u.14
Submonoid 
M: Type ?u.8
M where
  carrier := 
Set.center: (M : Type ?u.297) → [inst : Mul M] → Set M
Set.center 
M: Type ?u.8
M
  one_mem' := 
Set.one_mem_center: ∀ (M : Type ?u.451) [inst : MulOneClass M], 1 ∈ Set.center M
Set.one_mem_center 
M: Type ?u.8
M
  mul_mem' := 
Set.mul_mem_center: ∀ {M : Type ?u.303} [inst : Semigroup M] {a b : M}, a ∈ Set.center M → b ∈ Set.center M → a * b ∈ Set.center M
Set.mul_mem_center
#align submonoid.center 
Submonoid.center: (M : Type u_1) → [inst : Monoid M] → Submonoid M
Submonoid.center
#align add_submonoid.center 
AddSubmonoid.center: (M : Type u_1) → [inst : AddMonoid M] → AddSubmonoid M
AddSubmonoid.center

@[
to_additive: ∀ (M : Type u_1) [inst : AddMonoid M], ↑(AddSubmonoid.center M) = Set.addCenter M
to_additive]
theorem 
coe_center: ↑(center M) = Set.center M
coe_center : ↑(
center: (M : Type ?u.785) → [inst : Monoid M] → Submonoid M
center 
M: Type ?u.575
M) = 
Set.center: (M : Type ?u.585) → [inst : Mul M] → Set M
Set.center 
M: Type ?u.575
M :=
  
rfl: ∀ {α : Sort ?u.881} {a : α}, a = a
rfl
#align submonoid.coe_center 
Submonoid.coe_center: ∀ (M : Type u_1) [inst : Monoid M], ↑(center M) = Set.center M
Submonoid.coe_center
#align add_submonoid.coe_center 
AddSubmonoid.coe_center: ∀ (M : Type u_1) [inst : AddMonoid M], ↑(AddSubmonoid.center M) = Set.addCenter M
AddSubmonoid.coe_center

@[to_additive (attr := simp) 
AddSubmonoid.center_toAddSubsemigroup: ∀ (M : Type u_1) [inst : AddMonoid M], (AddSubmonoid.center M).toAddSubsemigroup = AddSubsemigroup.center M
AddSubmonoid.center_toAddSubsemigroup]
theorem 
center_toSubsemigroup: (center M).toSubsemigroup = Subsemigroup.center M
center_toSubsemigroup : (
center: (M : Type ?u.907) → [inst : Monoid M] → Submonoid M
center 
M: Type ?u.900
M).
toSubsemigroup: {M : Type ?u.917} → [inst : MulOneClass M] → Submonoid M → Subsemigroup M
toSubsemigroup = 
Subsemigroup.center: (M : Type ?u.1022) → [inst : Semigroup M] → Subsemigroup M
Subsemigroup.center 
M: Type ?u.900
M :=
  
rfl: ∀ {α : Sort ?u.1133} {a : α}, a = a
rfl
#align submonoid.center_to_subsemigroup 
Submonoid.center_toSubsemigroup: ∀ (M : Type u_1) [inst : Monoid M], (center M).toSubsemigroup = Subsemigroup.center M
Submonoid.center_toSubsemigroup

variable {
M: ?m.1183
M}

@[
to_additive: ∀ {M : Type u_1} [inst : AddMonoid M] {z : M}, z ∈ AddSubmonoid.center M ↔ ∀ (g : M), g + z = z + g
to_additive]
theorem 
mem_center_iff: ∀ {z : M}, z ∈ center M ↔ ∀ (g : M), g * z = z * g
mem_center_iff {
z: M
z : 
M: Type ?u.1186
M} : 
z: M
z ∈ 
center: (M : Type ?u.1199) → [inst : Monoid M] → Submonoid M
center 
M: Type ?u.1186
M ↔ ∀ 
g: ?m.1234
g, 
g: ?m.1234
g * 
z: M
z = 
z: M
z * 
g: ?m.1234
g :=
  
Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.rfl
#align submonoid.mem_center_iff 
Submonoid.mem_center_iff: ∀ {M : Type u_1} [inst : Monoid M] {z : M}, z ∈ center M ↔ ∀ (g : M), g * z = z * g
Submonoid.mem_center_iff
#align add_submonoid.mem_center_iff 
AddSubmonoid.mem_center_iff: ∀ {M : Type u_1} [inst : AddMonoid M] {z : M}, z ∈ AddSubmonoid.center M ↔ ∀ (g : M), g + z = z + g
AddSubmonoid.mem_center_iff

@[
to_additive: {M : Type u_1} →
  [inst : AddMonoid M] →
    (a : M) → [inst_1 : Decidable (∀ (b : M), b + a = a + b)] → Decidable (a ∈ AddSubmonoid.center M)
to_additive]
instance 
decidableMemCenter: (a : M) → [inst : Decidable (∀ (b : M), b * a = a * b)] → Decidable (a ∈ center M)
decidableMemCenter (
a: ?m.1807
a) [
Decidable: Prop → Type
Decidable <| ∀ 
b: M
b : 
M: Type ?u.1801
M, 
b: M
b * 
a: ?m.1807
a = 
a: ?m.1807
a * 
b: M
b] : 
Decidable: Prop → Type
Decidable (
a: ?m.1807
a ∈ 
center: (M : Type ?u.2364) → [inst : Monoid M] → Submonoid M
center 
M: Type ?u.1801
M) :=
  
decidable_of_iff': {a : Prop} → (b : Prop) → (a ↔ b) → [inst : Decidable b] → Decidable a
decidable_of_iff' 
_: Prop
_ 
mem_center_iff: ∀ {M : Type ?u.2400} [inst : Monoid M] {z : M}, z ∈ center M ↔ ∀ (g : M), g * z = z * g
mem_center_iff
#align submonoid.decidable_mem_center 
Submonoid.decidableMemCenter: {M : Type u_1} →
  [inst : Monoid M] → (a : M) → [inst_1 : Decidable (∀ (b : M), b * a = a * b)] → Decidable (a ∈ center M)
Submonoid.decidableMemCenter
#align add_submonoid.decidable_mem_center 
AddSubmonoid.decidableMemCenter: {M : Type u_1} →
  [inst : AddMonoid M] →
    (a : M) → [inst_1 : Decidable (∀ (b : M), b + a = a + b)] → Decidable (a ∈ AddSubmonoid.center M)
AddSubmonoid.decidableMemCenter

/-- The center of a monoid is commutative. -/
instance 
center.commMonoid: CommMonoid { x // x ∈ center M }
center.commMonoid : 
CommMonoid: Type ?u.2610 → Type ?u.2610
CommMonoid (
center: (M : Type ?u.2611) → [inst : Monoid M] → Submonoid M
center 
M: Type ?u.2604
M) :=
  { (
center: (M : Type ?u.2766) → [inst : Monoid M] → Submonoid M
center 
M: Type ?u.2604
M).
toMonoid: {M : Type ?u.2768} → [inst : Monoid M] → (S : Submonoid M) → Monoid { x // x ∈ S }
toMonoid with
    mul_comm := fun 
_: ?m.2825
_ 
b: ?m.2828
b => 
Subtype.ext: ∀ {α : Sort ?u.2830} {p : α → Prop} {a1 a2 : { x // p x }}, ↑a1 = ↑a2 → a1 = a2
Subtype.ext <| 
b: ?m.2828
b.
prop: ∀ {α : Sort ?u.2841} {p : α → Prop} (x : Subtype p), p ↑x
prop 
_: M
_ }

/-- The center of a monoid acts commutatively on that monoid. -/
instance 
center.smulCommClass_left: ∀ {M : Type u_1} [inst : Monoid M], SMulCommClass { x // x ∈ center M } M M
center.smulCommClass_left : 
SMulCommClass: (M : Type ?u.2979) → (N : Type ?u.2978) → (α : Type ?u.2977) → [inst : SMul M α] → [inst : SMul N α] → Prop
SMulCommClass (
center: (M : Type ?u.2980) → [inst : Monoid M] → Submonoid M
center 
M: Type ?u.2971
M) 
M: Type ?u.2971
M 
M: Type ?u.2971
M
    where smul_comm 
m: ?m.3981
m 
x: ?m.3984
x 
y: ?m.3987
y := (
Commute.left_comm: ∀ {S : Type ?u.3989} [inst : Semigroup S] {a b : S}, Commute a b → ∀ (c : S), a * (b * c) = b * (a * c)
Commute.left_comm (
m: ?m.3981
m.
prop: ∀ {α : Sort ?u.3994} {p : α → Prop} (x : Subtype p), p ↑x
prop 
x: ?m.3984
x) 
y: ?m.3987
y).
symm: ∀ {α : Sort ?u.4117} {a b : α}, a = b → b = a
symm
#align submonoid.center.smul_comm_class_left 
Submonoid.center.smulCommClass_left: ∀ {M : Type u_1} [inst : Monoid M], SMulCommClass { x // x ∈ center M } M M
Submonoid.center.smulCommClass_left

/-- The center of a monoid acts commutatively on that monoid. -/
instance 
center.smulCommClass_right: ∀ {M : Type u_1} [inst : Monoid M], SMulCommClass M { x // x ∈ center M } M
center.smulCommClass_right : 
SMulCommClass: (M : Type ?u.4168) → (N : Type ?u.4167) → (α : Type ?u.4166) → [inst : SMul M α] → [inst : SMul N α] → Prop
SMulCommClass 
M: Type ?u.4160
M (
center: (M : Type ?u.4169) → [inst : Monoid M] → Submonoid M
center 
M: Type ?u.4160
M) 
M: Type ?u.4160
M :=
  
SMulCommClass.symm: ∀ (M : Type ?u.5156) (N : Type ?u.5157) (α : Type ?u.5158) [inst : SMul M α] [inst_1 : SMul N α]
  [inst_2 : SMulCommClass M N α], SMulCommClass N M α
SMulCommClass.symm 
_: Type ?u.5156
_ 
_: Type ?u.5157
_ 
_: Type ?u.5158
_
#align submonoid.center.smul_comm_class_right 
Submonoid.center.smulCommClass_right: ∀ {M : Type u_1} [inst : Monoid M], SMulCommClass M { x // x ∈ center M } M
Submonoid.center.smulCommClass_right

/-! Note that `smulCommClass (center M) (center M) M` is already implied by
`Submonoid.smulCommClass_right` -/

example: ∀ {M : Type u_1} [inst : Monoid M], SMulCommClass { x // x ∈ center M } { x // x ∈ center M } M
example : 
SMulCommClass: (M : Type ?u.5331) → (N : Type ?u.5330) → (α : Type ?u.5329) → [inst : SMul M α] → [inst : SMul N α] → Prop
SMulCommClass (
center: (M : Type ?u.5332) → [inst : Monoid M] → Submonoid M
center 
M: Type ?u.5323
M) (
center: (M : Type ?u.5483) → [inst : Monoid M] → Submonoid M
center 
M: Type ?u.5323
M) 
M: Type ?u.5323
M := by
Goals accomplished! 🐙 
M: Type ?u.5323

inst✝: Monoid M

SMulCommClass { x // x ∈ center M } { x // x ∈ center M } Minfer_instance
Goals accomplished! 🐙

end

section

variable (
M: Type ?u.6168
M : 
Type _: Type (?u.6162+1)
Type _) [
CommMonoid: Type ?u.6165 → Type ?u.6165
CommMonoid 
M: Type ?u.6162
M]

@[simp]
theorem 
center_eq_top: ∀ (M : Type u_1) [inst : CommMonoid M], center M = ⊤
center_eq_top : 
center: (M : Type ?u.6175) → [inst : Monoid M] → Submonoid M
center 
M: Type ?u.6168
M = 
⊤: ?m.6349
⊤ :=
  
SetLike.coe_injective: ∀ {A : Type ?u.6405} {B : Type ?u.6406} [i : SetLike A B], Function.Injective SetLike.coe
SetLike.coe_injective (
Set.center_eq_univ: ∀ (M : Type ?u.6425) [inst : CommSemigroup M], Set.center M = Set.univ
Set.center_eq_univ 
M: Type ?u.6168
M)
#align submonoid.center_eq_top 
Submonoid.center_eq_top: ∀ (M : Type u_1) [inst : CommMonoid M], center M = ⊤
Submonoid.center_eq_top

end

end Submonoid

-- Guard against import creep
assert_not_exists Finset