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

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

/-!
# Centralizers of magmas and monoids

## Main definitions

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

We provide `Subgroup.centralizer`, `AddSubgroup.centralizer` in other files.
-/


variable {M: Type ?u.1584
M : Type _: Type (?u.1584+1)
Type _} {S: Set M
S T: Set M
T : Set: Type ?u.8 → Type ?u.8
Set M: Type ?u.2
M}

namespace Submonoid

section

variable [Monoid: Type ?u.1484 → Type ?u.1484
Monoid M: Type ?u.26
M] (S: ?m.23
S)

/-- The centralizer of a subset of a monoid `M`. -/
@[to_additive: {M : Type u_1} → Set M → [inst : AddMonoid M] → AddSubmonoid M
to_additive "The centralizer of a subset of an additive monoid."]
def centralizer: {M : Type u_1} → Set M → [inst : Monoid M] → Submonoid M
centralizer : Submonoid: (M : Type ?u.38) → [inst : MulOneClass M] → Type ?u.38
Submonoid M: Type ?u.26
M where
  carrier := S: Set M
S.centralizer: {M : Type ?u.321} → Set M → [inst : Mul M] → Set M
centralizer
  one_mem' := S: Set M
S.one_mem_centralizer: ∀ {M : Type ?u.484} (S : Set M) [inst : MulOneClass M], 1 ∈ Set.centralizer S
one_mem_centralizer
  mul_mem' := Set.mul_mem_centralizer: ∀ {M : Type ?u.332} {S : Set M} {a b : M} [inst : Semigroup M],
  a ∈ Set.centralizer S → b ∈ Set.centralizer S → a * b ∈ Set.centralizer S
Set.mul_mem_centralizer
#align submonoid.centralizer Submonoid.centralizer: {M : Type u_1} → Set M → [inst : Monoid M] → Submonoid M
Submonoid.centralizer
#align add_submonoid.centralizer AddSubmonoid.centralizer: {M : Type u_1} → Set M → [inst : AddMonoid M] → AddSubmonoid M
AddSubmonoid.centralizer

@[to_additive: ∀ {M : Type u_1} (S : Set M) [inst : AddMonoid M], ↑(AddSubmonoid.centralizer S) = Set.addCentralizer S
to_additive (attr := simp, norm_cast)]
theorem coe_centralizer: ∀ {M : Type u_1} (S : Set M) [inst : Monoid M], ↑(centralizer S) = Set.centralizer S
coe_centralizer : ↑(centralizer: {M : Type ?u.867} → Set M → [inst : Monoid M] → Submonoid M
centralizer S: Set M
S) = S: Set M
S.centralizer: {M : Type ?u.662} → Set M → [inst : Mul M] → Set M
centralizer :=
  rfl: ∀ {α : Sort ?u.967} {a : α}, a = a
rfl
#align submonoid.coe_centralizer Submonoid.coe_centralizer: ∀ {M : Type u_1} (S : Set M) [inst : Monoid M], ↑(centralizer S) = Set.centralizer S
Submonoid.coe_centralizer
#align add_submonoid.coe_centralizer AddSubmonoid.coe_centralizer: ∀ {M : Type u_1} (S : Set M) [inst : AddMonoid M], ↑(AddSubmonoid.centralizer S) = Set.addCentralizer S
AddSubmonoid.coe_centralizer

theorem centralizer_toSubsemigroup: ∀ {M : Type u_1} (S : Set M) [inst : Monoid M], (centralizer S).toSubsemigroup = Subsemigroup.centralizer S
centralizer_toSubsemigroup : (centralizer: {M : Type ?u.1215} → Set M → [inst : Monoid M] → Submonoid M
centralizer S: Set M
S).toSubsemigroup: {M : Type ?u.1229} → [inst : MulOneClass M] → Submonoid M → Subsemigroup M
toSubsemigroup = Subsemigroup.centralizer: {M : Type ?u.1334} → Set M → [inst : Semigroup M] → Subsemigroup M
Subsemigroup.centralizer S: Set M
S :=
  rfl: ∀ {α : Sort ?u.1448} {a : α}, a = a
rfl
#align submonoid.centralizer_to_subsemigroup Submonoid.centralizer_toSubsemigroup: ∀ {M : Type u_1} (S : Set M) [inst : Monoid M], (centralizer S).toSubsemigroup = Subsemigroup.centralizer S
Submonoid.centralizer_toSubsemigroup

theorem _root_.AddSubmonoid.centralizer_toAddSubsemigroup: ∀ {M : Type u_1} [inst : AddMonoid M] (S : Set M),
  (AddSubmonoid.centralizer S).toAddSubsemigroup = AddSubsemigroup.centralizer S
_root_.AddSubmonoid.centralizer_toAddSubsemigroup {M: ?m.1487
M} [AddMonoid: Type ?u.1490 → Type ?u.1490
AddMonoid M: ?m.1487
M] (S: Set M
S : Set: Type ?u.1493 → Type ?u.1493
Set M: ?m.1487
M) :
    (AddSubmonoid.centralizer: {M : Type ?u.1497} → Set M → [inst : AddMonoid M] → AddSubmonoid M
AddSubmonoid.centralizer S: Set M
S).toAddSubsemigroup: {M : Type ?u.1510} → [inst : AddZeroClass M] → AddSubmonoid M → AddSubsemigroup M
toAddSubsemigroup = AddSubsemigroup.centralizer: {M : Type ?u.1527} → Set M → [inst : AddSemigroup M] → AddSubsemigroup M
AddSubsemigroup.centralizer S: Set M
S :=
  rfl: ∀ {α : Sort ?u.1553} {a : α}, a = a
rfl
#align add_submonoid.centralizer_to_add_subsemigroup AddSubmonoid.centralizer_toAddSubsemigroup: ∀ {M : Type u_1} [inst : AddMonoid M] (S : Set M),
  (AddSubmonoid.centralizer S).toAddSubsemigroup = AddSubsemigroup.centralizer S
AddSubmonoid.centralizer_toAddSubsemigroup

attribute [to_additive existing AddSubmonoid.centralizer_toAddSubsemigroup: ∀ {M : Type u_1} [inst : AddMonoid M] (S : Set M),
  (AddSubmonoid.centralizer S).toAddSubsemigroup = AddSubsemigroup.centralizer S
AddSubmonoid.centralizer_toAddSubsemigroup]
  Submonoid.centralizer_toSubsemigroup: ∀ {M : Type u_1} (S : Set M) [inst : Monoid M], (centralizer S).toSubsemigroup = Subsemigroup.centralizer S
Submonoid.centralizer_toSubsemigroup

variable {S: ?m.1596
S}

@[to_additive: ∀ {M : Type u_1} {S : Set M} [inst : AddMonoid M] {z : M},
  z ∈ AddSubmonoid.centralizer S ↔ ∀ (g : M), g ∈ S → g + z = z + g
to_additive]
theorem mem_centralizer_iff: ∀ {z : M}, z ∈ centralizer S ↔ ∀ (g : M), g ∈ S → g * z = z * g
mem_centralizer_iff {z: M
z : M: Type ?u.1599
M} : z: M
z ∈ centralizer: {M : Type ?u.1618} → Set M → [inst : Monoid M] → Submonoid M
centralizer S: Set M
S ↔ ∀ g: ?m.1657
g ∈ S: Set M
S, g: ?m.1657
g * z: M
z = z: M
z * g: ?m.1657
g :=
  Iff.rfl: ∀ {a : Prop}, a ↔ a
Iff.rfl
#align submonoid.mem_centralizer_iff Submonoid.mem_centralizer_iff: ∀ {M : Type u_1} {S : Set M} [inst : Monoid M] {z : M}, z ∈ centralizer S ↔ ∀ (g : M), g ∈ S → g * z = z * g
Submonoid.mem_centralizer_iff
#align add_submonoid.mem_centralizer_iff AddSubmonoid.mem_centralizer_iff: ∀ {M : Type u_1} {S : Set M} [inst : AddMonoid M] {z : M},
  z ∈ AddSubmonoid.centralizer S ↔ ∀ (g : M), g ∈ S → g + z = z + g
AddSubmonoid.mem_centralizer_iff

@[to_additive: {M : Type u_1} →
  {S : Set M} →
    [inst : AddMonoid M] →
      (a : M) → [inst_1 : Decidable (∀ (b : M), b ∈ S → b + a = a + b)] → Decidable (a ∈ AddSubmonoid.centralizer S)
to_additive]
instance decidableMemCentralizer: {M : Type u_1} →
  {S : Set M} →
    [inst : Monoid M] →
      (a : M) → [inst_1 : Decidable (∀ (b : M), b ∈ S → b * a = a * b)] → Decidable (a ∈ centralizer S)
decidableMemCentralizer (a: M
a) [Decidable: Prop → Type
Decidable <| ∀ b: ?m.2280
b ∈ S: Set M
S, b: ?m.2280
b * a: ?m.2276
a = a: ?m.2276
a * b: ?m.2280
b] :
    Decidable: Prop → Type
Decidable (a: ?m.2276
a ∈ centralizer: {M : Type ?u.2869} → Set M → [inst : Monoid M] → Submonoid M
centralizer S: Set M
S) :=
  decidable_of_iff': {a : Prop} → (b : Prop) → (a ↔ b) → [inst : Decidable b] → Decidable a
decidable_of_iff' _: Prop
_ mem_centralizer_iff: ∀ {M : Type ?u.2906} {S : Set M} [inst : Monoid M] {z : M}, z ∈ centralizer S ↔ ∀ (g : M), g ∈ S → g * z = z * g
mem_centralizer_iff
#align submonoid.decidable_mem_centralizer Submonoid.decidableMemCentralizer: {M : Type u_1} →
  {S : Set M} →
    [inst : Monoid M] →
      (a : M) → [inst_1 : Decidable (∀ (b : M), b ∈ S → b * a = a * b)] → Decidable (a ∈ centralizer S)
Submonoid.decidableMemCentralizer
#align add_submonoid.decidable_mem_centralizer AddSubmonoid.decidableMemCentralizer: {M : Type u_1} →
  {S : Set M} →
    [inst : AddMonoid M] →
      (a : M) → [inst_1 : Decidable (∀ (b : M), b ∈ S → b + a = a + b)] → Decidable (a ∈ AddSubmonoid.centralizer S)
AddSubmonoid.decidableMemCentralizer

@[to_additive: ∀ {M : Type u_1} {S T : Set M} [inst : AddMonoid M], S ⊆ T → AddSubmonoid.centralizer T ≤ AddSubmonoid.centralizer S
to_additive]
theorem centralizer_le: S ⊆ T → centralizer T ≤ centralizer S
centralizer_le (h: S ⊆ T
h : S: Set M
S ⊆ T: Set M
T) : centralizer: {M : Type ?u.3194} → Set M → [inst : Monoid M] → Submonoid M
centralizer T: Set M
T ≤ centralizer: {M : Type ?u.3207} → Set M → [inst : Monoid M] → Submonoid M
centralizer S: Set M
S :=
  Set.centralizer_subset: ∀ {M : Type ?u.3309} {S T : Set M} [inst : Mul M], S ⊆ T → Set.centralizer T ⊆ Set.centralizer S
Set.centralizer_subset h: S ⊆ T
h
#align submonoid.centralizer_le Submonoid.centralizer_le: ∀ {M : Type u_1} {S T : Set M} [inst : Monoid M], S ⊆ T → centralizer T ≤ centralizer S
Submonoid.centralizer_le
#align add_submonoid.centralizer_le AddSubmonoid.centralizer_le: ∀ {M : Type u_1} {S T : Set M} [inst : AddMonoid M], S ⊆ T → AddSubmonoid.centralizer T ≤ AddSubmonoid.centralizer S
AddSubmonoid.centralizer_le

variable (M: ?m.3640
M)

@[to_additive: ∀ (M : Type u_1) [inst : AddMonoid M], AddSubmonoid.centralizer Set.univ = AddSubmonoid.center M
to_additive (attr := simp)]
theorem centralizer_univ: centralizer Set.univ = center M
centralizer_univ : centralizer: {M : Type ?u.3656} → Set M → [inst : Monoid M] → Submonoid M
centralizer Set.univ: {α : Type ?u.3658} → Set α
Set.univ = center: (M : Type ?u.3703) → [inst : Monoid M] → Submonoid M
center M: Type ?u.3643
M :=
  SetLike.ext': ∀ {A : Type ?u.3769} {B : Type ?u.3768} [i : SetLike A B] {p q : A}, ↑p = ↑q → p = q
SetLike.ext' (Set.centralizer_univ: ∀ (M : Type ?u.3788) [inst : Mul M], Set.centralizer Set.univ = Set.center M
Set.centralizer_univ M: Type ?u.3643
M)
#align submonoid.centralizer_univ Submonoid.centralizer_univ: ∀ (M : Type u_1) [inst : Monoid M], centralizer Set.univ = center M
Submonoid.centralizer_univ
#align add_submonoid.centralizer_univ AddSubmonoid.centralizer_univ: ∀ (M : Type u_1) [inst : AddMonoid M], AddSubmonoid.centralizer Set.univ = AddSubmonoid.center M
AddSubmonoid.centralizer_univ

end

end Submonoid

-- Guard against import creep
assert_not_exists Finset