Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+β Ctrl+β to navigate,
Ctrl+π±οΈ to focus.
On Mac, use
Cmd instead of
Ctrl .
/-
Copyright (c) 2018 Johannes HΓΆlzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes HΓΆlzl, Kenny Lau, Johan Commelin, Mario Carneiro, Kevin Buzzard,
Amelia Livingston, Yury Kudryashov, Yakov Pechersky
! This file was ported from Lean 3 source module group_theory.subsemigroup.basic
! leanprover-community/mathlib commit feb99064803fd3108e37c18b0f77d0a8344677a3
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Hom.Group
import Mathlib.Data.Set.Lattice
import Mathlib.Data.SetLike.Basic
/-!
# Subsemigroups: definition and `CompleteLattice` structure
This file defines bundled multiplicative and additive subsemigroups. We also define
a `CompleteLattice` structure on `Subsemigroup`s,
and define the closure of a set as the minimal subsemigroup that includes this set.
## Main definitions
* `Subsemigroup M`: the type of bundled subsemigroup of a magma `M`; the underlying set is given in
the `carrier` field of the structure, and should be accessed through coercion as in `(S : Set M)`.
* `AddSubsemigroup M` : the type of bundled subsemigroups of an additive magma `M`.
For each of the following definitions in the `Subsemigroup` namespace, there is a corresponding
definition in the `AddSubsemigroup` namespace.
* `Subsemigroup.copy` : copy of a subsemigroup with `carrier` replaced by a set that is equal but
possibly not definitionally equal to the carrier of the original `Subsemigroup`.
* `Subsemigroup.closure` : semigroup closure of a set, i.e.,
the least subsemigroup that includes the set.
* `Subsemigroup.gi` : `closure : Set M β Subsemigroup M` and coercion `coe : Subsemigroup M β Set M`
form a `GaloisInsertion`;
## Implementation notes
Subsemigroup inclusion is denoted `β€` rather than `β`, although `β` is defined as
membership of a subsemigroup's underlying set.
Note that `Subsemigroup M` does not actually require `Semigroup M`,
instead requiring only the weaker `Mul M`.
This file is designed to have very few dependencies. In particular, it should not use natural
numbers.
## Tags
subsemigroup, subsemigroups
-/
-- Only needed for notation
variable { M : Type _ } { N : Type _ } { A : Type _ }
section NonAssoc
variable [ Mul M ] { s : Set M }
variable [ Add A ] { t : Set A }
/-- `MulMemClass S M` says `S` is a type of sets `s : Set M` that are closed under `(*)` -/
class MulMemClass ( S : Type _ ) ( M : Type _ ) [ Mul M ] [ SetLike S M ] : Prop where
/-- A substructure satisfying `MulMemClass` is closed under multiplication. -/
mul_mem : β { s : S } { a b : M }, a β s β b β s β a * b β s
#align mul_mem_class MulMemClass
export MulMemClass (mul_mem)
/-- `AddMemClass S M` says `S` is a type of sets `s : Set M` that are closed under `(+)` -/
class AddMemClass ( S : Type _ ) ( M : Type _ ) [ Add M ] [ SetLike S M ] : Prop where
/-- A substructure satisfying `AddMemClass` is closed under addition. -/
add_mem : β { s : S } { a b : M }, a β s β b β s β a + b β s
#align add_mem_class AddMemClass
export AddMemClass (add_mem)
attribute [ to_additive ] MulMemClass
/-- A subsemigroup of a magma `M` is a subset closed under multiplication. -/
structure Subsemigroup : (M : Type u_1) β [inst : Mul M Type u_1 ( M : Type _ ) [ Mul M ] where
/-- The carrier of a subsemigroup. -/
carrier : Set M
/-- The product of two elements of a subsemigroup belongs to the subsemigroup. -/
mul_mem' : β {M : Type u_1} [inst : Mul M self : Subsemigroup M a b : M },
a β self .carrierb β self .carriera * b β self .carrier { a b } : a β carrier β b β carrier β a * b β carrier
#align subsemigroup Subsemigroup : (M : Type u_1) β [inst : Mul M Type u_1
/-- An additive subsemigroup of an additive magma `M` is a subset closed under addition. -/
structure AddSubsemigroup ( M : Type _ ) [ Add M ] where
/-- The carrier of an additive subsemigroup. -/
carrier : Set M
/-- The sum of two elements of an additive subsemigroup belongs to the subsemigroup. -/
add_mem' { a b } : a β carrier β b β carrier β a + b β carrier
#align add_subsemigroup AddSubsemigroup : (M : Type u_1) β [inst : Add M Type u_1
attribute [ to_additive AddSubsemigroup : (M : Type u_1) β [inst : Add M Type u_1 ] Subsemigroup : (M : Type u_1) β [inst : Mul M Type u_1
namespace Subsemigroup
@[ to_additive ]
instance : SetLike ( Subsemigroup : (M : Type ?u.1578) β [inst : Mul M Type ?u.1578 M ) M :=
β¨ Subsemigroup.carrier , fun p q h => by cases p M : Type ?u.1555N : Type ?u.1558A : Type ?u.1561instβΒΉ : Mul M s : Set M instβ : Add A t : Set A q : Subsemigroup M carrierβ : Set M mul_mem'β : β {a b : M }, a β carrierβ b β carrierβ a * b β carrierβ h : { carrier := carrierβ , mul_mem' := mul_mem'β } .carrier= q .carriermk { carrier := carrierβ , mul_mem' := mul_mem'β } = q ; M : Type ?u.1555N : Type ?u.1558A : Type ?u.1561instβΒΉ : Mul M s : Set M instβ : Add A t : Set A q : Subsemigroup M carrierβ : Set M mul_mem'β : β {a b : M }, a β carrierβ b β carrierβ a * b β carrierβ h : { carrier := carrierβ , mul_mem' := mul_mem'β } .carrier= q .carriermk { carrier := carrierβ , mul_mem' := mul_mem'β } = q cases q M : Type ?u.1555N : Type ?u.1558A : Type ?u.1561instβΒΉ : Mul M s : Set M instβ : Add A t : Set A carrierβΒΉ : Set M mul_mem'βΒΉ : β {a b : M }, a β carrierβΒΉ b β carrierβΒΉ a * b β carrierβΒΉ carrierβ : Set M mul_mem'β : β {a b : M }, a β carrierβ b β carrierβ a * b β carrierβ h : { carrier := carrierβΒΉ , mul_mem' := mul_mem'βΒΉ } .carrier= { carrier := carrierβ , mul_mem' := mul_mem'β } .carriermk.mk { carrier := carrierβΒΉ , mul_mem' := mul_mem'βΒΉ } = { carrier := carrierβ , mul_mem' := mul_mem'β } ; M : Type ?u.1555N : Type ?u.1558A : Type ?u.1561instβΒΉ : Mul M s : Set M instβ : Add A t : Set A carrierβΒΉ : Set M mul_mem'βΒΉ : β {a b : M }, a β carrierβΒΉ b β carrierβΒΉ a * b β carrierβΒΉ carrierβ : Set M mul_mem'β : β {a b : M }, a β carrierβ b β carrierβ a * b β carrierβ h : { carrier := carrierβΒΉ , mul_mem' := mul_mem'βΒΉ } .carrier= { carrier := carrierβ , mul_mem' := mul_mem'β } .carriermk.mk { carrier := carrierβΒΉ , mul_mem' := mul_mem'βΒΉ } = { carrier := carrierβ , mul_mem' := mul_mem'β } congr β©
@[ to_additive ]
instance : MulMemClass ( Subsemigroup : (M : Type ?u.2145) β [inst : Mul M Type ?u.2145 M ) M where mul_mem := fun { _ _ _ } => Subsemigroup.mul_mem' : β {M : Type ?u.2187} [inst : Mul M self : Subsemigroup M a b : M },
a β self .carrierb β self .carriera * b β self .carrier _
initialize_simps_projections Subsemigroup : (M : Type u_1) β [inst : Mul M Type u_1 ( carrier β coe )
initialize_simps_projections AddSubsemigroup : (M : Type u_1) β [inst : Add M Type u_1 ( carrier β coe )
@[ to_additive ( attr := simp )]
theorem mem_carrier { s : Subsemigroup : (M : Type ?u.2374) β [inst : Mul M Type ?u.2374 M } { x : M } : x β s . carrier β x β s :=
Iff.rfl
#align subsemigroup.mem_carrier Subsemigroup.mem_carrier
#align add_subsemigroup.mem_carrier AddSubsemigroup.mem_carrier
@[ to_additive : β {M : Type u_1} [inst : Add M s : Set M x : M } (h_mul : β {a b : M }, a β s b β s a + b β s ),
x β { carrier := s , add_mem' := h_mul } β x β s to_additive ( attr := simp )]
theorem mem_mk : β {s : Set M x : M } (h_mul : β {a b : M }, a β s b β s a * b β s ), x β { carrier := s , mul_mem' := h_mul } β x β s mem_mk { s : Set M } { x : M } ( h_mul ) : x β mk s h_mul β x β s :=
Iff.rfl
#align subsemigroup.mem_mk Subsemigroup.mem_mk : β {M : Type u_1} [inst : Mul M s : Set M x : M } (h_mul : β {a b : M }, a β s b β s a * b β s ),
x β { carrier := s , mul_mem' := h_mul } β x β s
#align add_subsemigroup.mem_mk AddSubsemigroup.mem_mk : β {M : Type u_1} [inst : Add M s : Set M x : M } (h_mul : β {a b : M }, a β s b β s a + b β s ),
x β { carrier := s , add_mem' := h_mul } β x β s
@[ to_additive : β {M : Type u_1} [inst : Add M s : Set M h_mul : β {a b : M }, a β s b β s a + b β s ),
β{ carrier := s , add_mem' := h_mul } = s to_additive ( attr := simp )]
theorem coe_set_mk : β {M : Type u_1} [inst : Mul M s : Set M h_mul : β {a b : M }, a β s b β s a * b β s ),
β{ carrier := s , mul_mem' := h_mul } = s coe_set_mk { s : Set M } ( h_mul : β {a b : M }, a β s b β s a * b β s h_mul ) : ( mk s h_mul : Set M ) = s :=
rfl : β {Ξ± : Sort ?u.2923} {a : Ξ± }, a = a
#align subsemigroup.coe_set_mk Subsemigroup.coe_set_mk : β {M : Type u_1} [inst : Mul M s : Set M h_mul : β {a b : M }, a β s b β s a * b β s ),
β{ carrier := s , mul_mem' := h_mul } = s
#align add_subsemigroup.coe_set_mk AddSubsemigroup.coe_set_mk : β {M : Type u_1} [inst : Add M s : Set M h_mul : β {a b : M }, a β s b β s a + b β s ),
β{ carrier := s , add_mem' := h_mul } = s
@[ to_additive : β {M : Type u_1} [inst : Add M s t : Set M h_mul : β {a b : M }, a β s b β s a + b β s )
(h_mul' : β {a b : M }, a β t b β t a + b β t ),
{ carrier := s , add_mem' := h_mul } β€ { carrier := t , add_mem' := h_mul' } β s β t to_additive ( attr := simp )]
theorem mk_le_mk : β {M : Type u_1} [inst : Mul M s t : Set M h_mul : β {a b : M }, a β s b β s a * b β s )
(h_mul' : β {a b : M }, a β t b β t a * b β t ),
{ carrier := s , mul_mem' := h_mul } β€ { carrier := t , mul_mem' := h_mul' } β s β t mk_le_mk { s t : Set M } ( h_mul : β {a b : M }, a β s b β s a * b β s h_mul ) ( h_mul' : β {a b : M }, a β t b β t a * b β t h_mul' ) : mk s h_mul β€ mk t h_mul' β s β t :=
Iff.rfl
#align subsemigroup.mk_le_mk Subsemigroup.mk_le_mk : β {M : Type u_1} [inst : Mul M s t : Set M h_mul : β {a b : M }, a β s b β s a * b β s )
(h_mul' : β {a b : M }, a β t b β t a * b β t ),
{ carrier := s , mul_mem' := h_mul } β€ { carrier := t , mul_mem' := h_mul' } β s β t
#align add_subsemigroup.mk_le_mk AddSubsemigroup.mk_le_mk : β {M : Type u_1} [inst : Add M s t : Set M h_mul : β {a b : M }, a β s b β s a + b β s )
(h_mul' : β {a b : M }, a β t b β t a + b β t ),
{ carrier := s , add_mem' := h_mul } β€ { carrier := t , add_mem' := h_mul' } β s β t
/-- Two subsemigroups are equal if they have the same elements. -/
@[ to_additive ( attr := ext ) "Two `AddSubsemigroup`s are equal if they have the same elements."]
theorem ext { S T : Subsemigroup : (M : Type ?u.3536) β [inst : Mul M Type ?u.3536 M } ( h : β x , x β S β x β T ) : S = T :=
SetLike.ext : β {A : Type ?u.3604} {B : Type ?u.3603} [i : SetLike A B p q : A }, (β (x : B ), x β p β x β q ) β p = q h
#align subsemigroup.ext Subsemigroup.ext
#align add_subsemigroup.ext AddSubsemigroup.ext
/-- Copy a subsemigroup replacing `carrier` with a set that is equal to it. -/
@[ to_additive "Copy an additive subsemigroup replacing `carrier` with a set that is equal to it."]
protected def copy ( S : Subsemigroup : (M : Type ?u.3712) β [inst : Mul M Type ?u.3712 M ) ( s : Set M ) ( hs : s = S ) :
Subsemigroup : (M : Type ?u.3885) β [inst : Mul M Type ?u.3885 M where
carrier := s
mul_mem' := hs . symm : β {Ξ± : Sort ?u.3898} {a b : Ξ± }, a = b b = a βΈ S . mul_mem' : β {M : Type ?u.3909} [inst : Mul M self : Subsemigroup M a b : M },
a β self .carrierb β self .carriera * b β self .carrier
#align subsemigroup.copy Subsemigroup.copy
#align add_subsemigroup.copy AddSubsemigroup.copy
variable { S : Subsemigroup : (M : Type ?u.12567) β [inst : Mul M Type ?u.12567 M }
@[ to_additive ( attr := simp )]
theorem coe_copy { s : Set M } ( hs : s = S ) : ( S . copy s hs : Set M ) = s :=
rfl : β {Ξ± : Sort ?u.4437} {a : Ξ± }, a = a
#align subsemigroup.coe_copy Subsemigroup.coe_copy
#align add_subsemigroup.coe_copy AddSubsemigroup.coe_copy
@[ to_additive ]
theorem copy_eq { s : Set M } ( hs : s = S ) : S . copy s hs = S :=
SetLike.coe_injective hs
#align subsemigroup.copy_eq Subsemigroup.copy_eq
#align add_subsemigroup.copy_eq AddSubsemigroup.copy_eq
variable ( S )
/-- A subsemigroup is closed under multiplication. -/
@[ to_additive "An `AddSubsemigroup` is closed under addition."]
protected theorem mul_mem : β {x y : M }, x β S y β S x * y β S mul_mem { x y : M } : x β S β y β S β x * y β S :=
Subsemigroup.mul_mem' : β {M : Type ?u.4999} [inst : Mul M self : Subsemigroup M a b : M },
a β self .carrierb β self .carriera * b β self .carrier S
#align subsemigroup.mul_mem Subsemigroup.mul_mem
#align add_subsemigroup.add_mem AddSubsemigroup.add_mem
/-- The subsemigroup `M` of the magma `M`. -/
@[ to_additive "The additive subsemigroup `M` of the magma `M`."]
instance : Top ( Subsemigroup : (M : Type ?u.5091) β [inst : Mul M Type ?u.5091 M ) :=
β¨{ carrier := Set.univ : {Ξ± : Type ?u.5110} β Set Ξ±
mul_mem' := fun _ _ => Set.mem_univ : β {Ξ± : Type ?u.5122} (x : Ξ± ), x β Set.univ _ }β©
/-- The trivial subsemigroup `β
` of a magma `M`. -/
@[ to_additive "The trivial `AddSubsemigroup` `β
` of an additive magma `M`."]
instance : Bot ( Subsemigroup : (M : Type ?u.5279) β [inst : Mul M Type ?u.5279 M ) :=
β¨{ carrier := β
mul_mem' := False.elim : β {C : Sort ?u.5344}, False β C }β©
@[ to_additive ]
instance : Inhabited : Sort ?u.5485 β Sort (max1?u.5485) ( Subsemigroup : (M : Type ?u.5486) β [inst : Mul M Type ?u.5486 M ) :=
β¨ β₯ β©
@[ to_additive ]
theorem not_mem_bot { x : M } : x β ( β₯ : Subsemigroup : (M : Type ?u.5654) β [inst : Mul M Type ?u.5654 M ) :=
Set.not_mem_empty : β {Ξ± : Type ?u.5723} (x : Ξ± ), Β¬ x β β
x
#align subsemigroup.not_mem_bot Subsemigroup.not_mem_bot : β {M : Type u_1} [inst : Mul M x : M }, Β¬ x β β₯
#align add_subsemigroup.not_mem_bot AddSubsemigroup.not_mem_bot : β {M : Type u_1} [inst : Add M x : M }, Β¬ x β β₯
@[ to_additive : β {M : Type u_1} [inst : Add M x : M ), x β β€ to_additive ( attr := simp )]
theorem mem_top : β (x : M ), x β β€ mem_top ( x : M ) : x β ( β€ : Subsemigroup : (M : Type ?u.5801) β [inst : Mul M Type ?u.5801 M ) :=
Set.mem_univ : β {Ξ± : Type ?u.5865} (x : Ξ± ), x β Set.univ x
#align subsemigroup.mem_top Subsemigroup.mem_top : β {M : Type u_1} [inst : Mul M x : M ), x β β€
#align add_subsemigroup.mem_top AddSubsemigroup.mem_top : β {M : Type u_1} [inst : Add M x : M ), x β β€
@[ to_additive : β {M : Type u_1} [inst : Add M ββ€ = Set.univ to_additive ( attr := simp )]
theorem coe_top : ββ€ = Set.univ coe_top : (( β€ : Subsemigroup : (M : Type ?u.5962) β [inst : Mul M Type ?u.5962 M ) : Set M ) = Set.univ : {Ξ± : Type ?u.6091} β Set Ξ± :=
rfl : β {Ξ± : Sort ?u.6123} {a : Ξ± }, a = a
#align subsemigroup.coe_top Subsemigroup.coe_top : β {M : Type u_1} [inst : Mul M ββ€ = Set.univ
#align add_subsemigroup.coe_top AddSubsemigroup.coe_top : β {M : Type u_1} [inst : Add M ββ€ = Set.univ
@[ to_additive ( attr := simp )]
theorem coe_bot : (( β₯ : Subsemigroup : (M : Type ?u.6201) β [inst : Mul M Type ?u.6201 M ) : Set M ) = β
:=
rfl : β {Ξ± : Sort ?u.6412} {a : Ξ± }, a = a
#align subsemigroup.coe_bot Subsemigroup.coe_bot : β {M : Type u_1} [inst : Mul M ββ₯ = β
#align add_subsemigroup.coe_bot AddSubsemigroup.coe_bot : β {M : Type u_1} [inst : Add M ββ₯ = β
/-- The inf of two subsemigroups is their intersection. -/
@[ to_additive "The inf of two `AddSubsemigroup`s is their intersection."]
instance : Inf ( Subsemigroup : (M : Type ?u.6487) β [inst : Mul M Type ?u.6487 M ) :=
β¨ fun Sβ Sβ =>
{ carrier := Sβ β© Sβ
mul_mem' := fun β¨ hx , hx' β© β¨ hy , hy' β© => β¨ Sβ . mul_mem hx hy , Sβ . mul_mem hx' hy' β© }β©
@[ to_additive ( attr := simp )]
theorem coe_inf ( p p' : Subsemigroup : (M : Type ?u.7142) β [inst : Mul M Type ?u.7142 M ) : (( p β p' : Subsemigroup : (M : Type ?u.7150) β [inst : Mul M Type ?u.7150 M ) : Set M ) = ( p : Set M ) β© p' :=
rfl : β {Ξ± : Sort ?u.7410} {a : Ξ± }, a = a
#align subsemigroup.coe_inf Subsemigroup.coe_inf
#align add_subsemigroup.coe_inf AddSubsemigroup.coe_inf
@[ to_additive ( attr := simp )]
theorem mem_inf { p p' : Subsemigroup : (M : Type ?u.7516) β [inst : Mul M Type ?u.7516 M } { x : M } : x β p β p' β x β p β§ x β p' :=
Iff.rfl
#align subsemigroup.mem_inf Subsemigroup.mem_inf
#align add_subsemigroup.mem_inf AddSubsemigroup.mem_inf
@[ to_additive ]
instance : InfSet ( Subsemigroup : (M : Type ?u.7713) β [inst : Mul M Type ?u.7713 M ) :=
β¨ fun s =>
{ carrier := β t β s , β t
mul_mem' := fun hx hy =>
Set.mem_biInter fun i h =>
i . mul_mem ( by apply Set.mem_iInterβ : β {Ξ³ : Type ?u.7972} {ΞΉ : Sort ?u.7973} {ΞΊ : ΞΉ β Sort ?u.7974x : Ξ³ } {s : (i : ΞΉ ) β ΞΊ i Set Ξ³ },
(x β Set.iInter fun i => Set.iInter fun j => s i j β β (i : ΞΉ ) (j : ΞΊ i x β s i j . 1 : β {a b : Prop }, (a β b a β b hx i h ) ( by apply Set.mem_iInterβ : β {Ξ³ : Type ?u.8013} {ΞΉ : Sort ?u.8014} {ΞΊ : ΞΉ β Sort ?u.8015x : Ξ³ } {s : (i : ΞΉ ) β ΞΊ i Set Ξ³ },
(x β Set.iInter fun i => Set.iInter fun j => s i j β β (i : ΞΉ ) (j : ΞΊ i x β s i j . 1 : β {a b : Prop }, (a β b a β b hy i h ) }β©
@[ to_additive ( attr := simp , norm_cast )]
theorem coe_sInf ( S : Set ( Subsemigroup : (M : Type ?u.8246) β [inst : Mul M Type ?u.8246 M )) : (( sInf : {Ξ± : Type ?u.8262} β [self : InfSet Ξ± Set Ξ± Ξ± S : Subsemigroup : (M : Type ?u.8260) β [inst : Mul M Type ?u.8260 M ) : Set M ) = β s β S , β s :=
rfl : β {Ξ± : Sort ?u.8668} {a : Ξ± }, a = a
#align subsemigroup.coe_Inf Subsemigroup.coe_sInf
#align add_subsemigroup.coe_Inf AddSubsemigroup.coe_sInf
@[ to_additive ]
theorem mem_sInf { S : Set ( Subsemigroup : (M : Type ?u.9015) β [inst : Mul M Type ?u.9015 M )} { x : M } : x β sInf : {Ξ± : Type ?u.9032} β [self : InfSet Ξ± Set Ξ± Ξ± S β β p β S , x β p :=
Set.mem_iInterβ : β {Ξ³ : Type ?u.9139} {ΞΉ : Sort ?u.9140} {ΞΊ : ΞΉ β Sort ?u.9141x : Ξ³ } {s : (i : ΞΉ ) β ΞΊ i Set Ξ³ },
(x β Set.iInter fun i => Set.iInter fun j => s i j β β (i : ΞΉ ) (j : ΞΊ i x β s i j
#align subsemigroup.mem_Inf Subsemigroup.mem_sInf
#align add_subsemigroup.mem_Inf AddSubsemigroup.mem_sInf
@[ to_additive ]
theorem mem_iInf { ΞΉ : Sort _ } { S : ΞΉ β Subsemigroup : (M : Type ?u.9261) β [inst : Mul M Type ?u.9261 M } { x : M } : ( x β β¨
i , S i ) β β i , x β S i := by
(x β β¨
i , S i β β (i : ΞΉ ), x β S i simp only [ iInf : {Ξ± : Type ?u.9374} β [inst : InfSet Ξ± {ΞΉ : Sort ?u.9373} β (ΞΉ β Ξ± Ξ± , mem_sInf , Set.forall_range_iff : β {Ξ± : Type ?u.9410} {ΞΉ : Sort ?u.9411} {f : ΞΉ β Ξ± p : Ξ± β Prop (β (a : Ξ± ), a β Set.range f p a ) β β (i : ΞΉ ), p (f i ]
#align subsemigroup.mem_infi Subsemigroup.mem_iInf
#align add_subsemigroup.mem_infi AddSubsemigroup.mem_iInf
@[ to_additive ( attr := simp , norm_cast )]
theorem coe_iInf { ΞΉ : Sort _ } { S : ΞΉ β Subsemigroup : (M : Type ?u.9695) β [inst : Mul M Type ?u.9695 M } : (β(β¨
i , S i ) : Set M ) = β i , S i := by
simp only [ iInf : {Ξ± : Type ?u.10085} β [inst : InfSet Ξ± {ΞΉ : Sort ?u.10084} β (ΞΉ β Ξ± Ξ± , coe_sInf , Set.biInter_range ]
#align subsemigroup.coe_infi Subsemigroup.coe_iInf
#align add_subsemigroup.coe_infi AddSubsemigroup.coe_iInf
/-- subsemigroups of a monoid form a complete lattice. -/
@[ to_additive "The `AddSubsemigroup`s of an `AddMonoid` form a complete lattice."]
instance : CompleteLattice : Type ?u.10745 β Type ?u.10745 ( Subsemigroup : (M : Type ?u.10746) β [inst : Mul M Type ?u.10746 M ) :=
{ completeLatticeOfInf ( Subsemigroup : (M : Type ?u.10758) β [inst : Mul M Type ?u.10758 M ) fun _ =>
IsGLB.of_image SetLike.coe_subset_coe : β {A : Type ?u.10951} {B : Type ?u.10950} [i : SetLike A B S T : A }, βS β βT β S β€ T isGLB_biInf with
le := (Β· β€ Β·)
lt := (Β· < Β·)
bot := β₯
bot_le := fun _ _ hx => ( not_mem_bot hx ). elim
top := β€
le_top := fun _ x _ => mem_top : β {M : Type ?u.11901} [inst : Mul M x : M ), x β β€ x
inf := (Β· β Β·)
sInf := InfSet.sInf : {Ξ± : Type ?u.11750} β [self : InfSet Ξ± Set Ξ± Ξ±
le_inf := fun _ _ _ ha hb _ hx => β¨ ha hx , hb hx β©
inf_le_left := fun _ _ _ => And.left : β {a b : Prop }, a β§ b a
inf_le_right := fun _ _ _ => And.right : β {a b : Prop }, a β§ b b }
@[ to_additive ( attr := simp )]
theorem subsingleton_of_subsingleton [ Subsingleton ( Subsemigroup : (M : Type ?u.12578) β [inst : Mul M Type ?u.12578 M )] : Subsingleton M := by
constructor ; intro x y
have : β a : M , a β ( β₯ : Subsemigroup : (M : Type ?u.12626) β [inst : Mul M Type ?u.12626 M ) := by simp [ Subsingleton.elim ( β₯ : Subsemigroup : (M : Type ?u.12700) β [inst : Mul M Type ?u.12700 M ) β€ ]
exact absurd : β {a : Prop } {b : Sort ?u.13602}, a β Β¬ a b ( this x ) not_mem_bot
#align subsemigroup.subsingleton_of_subsingleton Subsemigroup.subsingleton_of_subsingleton
#align add_subsemigroup.subsingleton_of_subsingleton AddSubsemigroup.subsingleton_of_subsingleton
@[ to_additive ]
instance [ hn : Nonempty M ] : Nontrivial ( Subsemigroup : (M : Type ?u.13723) β [inst : Mul M Type ?u.13723 M ) :=
β¨β¨ β₯ , β€ , fun h => by
obtain β¨ x β© := id : β {Ξ± : Sort ?u.13834}, Ξ± β Ξ± hn
refine' absurd : β {a : Prop } {b : Sort ?u.13858}, a β Β¬ a b ( _ : x β β₯ ) not_mem_bot
simp [ h ] β©β©
/-- The `Subsemigroup` generated by a set. -/
@[ to_additive "The `AddSubsemigroup` generated by a set"]
def closure ( s : Set M ) : Subsemigroup : (M : Type ?u.14180) β [inst : Mul M Type ?u.14180 M :=
sInf : {Ξ± : Type ?u.14190} β [self : InfSet Ξ± Set Ξ± Ξ± { S | s β S }
#align subsemigroup.closure Subsemigroup.closure
#align add_subsemigroup.closure AddSubsemigroup.closure
@[ to_additive ]
theorem mem_closure { x : M } : x β closure s β β S : Subsemigroup : (M : Type ?u.14505) β [inst : Mul M Type ?u.14505 M , s β S β x β S :=
mem_sInf
#align subsemigroup.mem_closure Subsemigroup.mem_closure
#align add_subsemigroup.mem_closure AddSubsemigroup.mem_closure
/-- The subsemigroup generated by a set includes the set. -/
@[ to_additive ( attr := simp ) "The `AddSubsemigroup` generated by a set includes the set."]
theorem subset_closure : s β closure s := fun _ hx => mem_closure . 2 : β {a b : Prop }, (a β b b β a fun _ hS => hS hx
#align subsemigroup.subset_closure Subsemigroup.subset_closure
#align add_subsemigroup.subset_closure AddSubsemigroup.subset_closure
@[ to_additive ]
theorem not_mem_of_not_mem_closure { P : M } ( hP : P β closure s ) : P β s := fun h =>
hP ( subset_closure h )
#align subsemigroup.not_mem_of_not_mem_closure Subsemigroup.not_mem_of_not_mem_closure
#align add_subsemigroup.not_mem_of_not_mem_closure AddSubsemigroup.not_mem_of_not_mem_closure
variable { S }
open Set
/-- A subsemigroup `S` includes `closure s` if and only if it includes `s`. -/
@[ to_additive ( attr := simp )
"An additive subsemigroup `S` includes `closure s` if and only if it includes `s`"]
theorem closure_le : closure s β€ S β s β S :=
β¨ Subset.trans : β {Ξ± : Type ?u.15448} {a b c : Set Ξ± a β b b β c a β c subset_closure , fun h => sInf_le h β©
#align subsemigroup.closure_le Subsemigroup.closure_le
#align add_subsemigroup.closure_le AddSubsemigroup.closure_le
/-- subsemigroup closure of a set is monotone in its argument: if `s β t`,
then `closure s β€ closure t`. -/
@[ to_additive "Additive subsemigroup closure of a set is monotone in its argument: if `s β t`,
then `closure s β€ closure t`"]
theorem closure_mono β¦ s t : Set M β¦ ( h : s β t ) : closure s β€ closure t :=
closure_le . 2 : β {a b : Prop }, (a β b b β a <| Subset.trans : β {Ξ± : Type ?u.15830} {a b c : Set Ξ± a β b b β c a β c h subset_closure
#align subsemigroup.closure_mono Subsemigroup.closure_mono
#align add_subsemigroup.closure_mono AddSubsemigroup.closure_mono
@[ to_additive ]
theorem closure_eq_of_le ( hβ : s β S ) ( hβ : S β€ closure s ) : closure s = S :=
le_antisymm ( closure_le . 2 : β {a b : Prop }, (a β b b β a hβ ) hβ
#align subsemigroup.closure_eq_of_le Subsemigroup.closure_eq_of_le
#align add_subsemigroup.closure_eq_of_le AddSubsemigroup.closure_eq_of_le
variable ( S )
/-- An induction principle for closure membership. If `p` holds for all elements of `s`, and
is preserved under multiplication, then `p` holds for all elements of the closure of `s`. -/
@[ to_additive ( attr := elab_as_elim) "An induction principle for additive closure membership. If `p`
holds for all elements of `s`, and is preserved under addition, then `p` holds for all
elements of the additive closure of `s`."]
theorem closure_induction : β {p : M β Prop x : M }, x β closure s (β (x : M ), x β s p x ) β (β (x y : M ), p x p y p (x * y ) β p x closure_induction { p : M β Prop } { x } ( h : x β closure s ) ( Hs : β (x : M ), x β s p x Hs : β x β s , p x )
( Hmul : β (x y : M ), p x p y p (x * y Hmul : β x y , p x β p y β p ( x * y )) : p x :=
(@ closure_le _ _ _ β¨ p , Hmul : β (x y : M ), p x p y p (x * y Hmul _ _ β©). 2 : β {a b : Prop }, (a β b b β a Hs : β (x : M ), x β s p x Hs h
#align subsemigroup.closure_induction Subsemigroup.closure_induction : β {M : Type u_1} [inst : Mul M s : Set M p : M β Prop x : M },
x β closure s (β (x : M ), x β s p x ) β (β (x y : M ), p x p y p (x * y ) β p x
#align add_subsemigroup.closure_induction AddSubsemigroup.closure_induction : β {M : Type u_1} [inst : Add M s : Set M p : M β Prop x : M },
x β AddSubsemigroup.closure s (β (x : M ), x β s p x ) β (β (x y : M ), p x p y p (x + y ) β p x
/-- A dependent version of `Subsemigroup.closure_induction`. -/
@[ to_additive ( attr := elab_as_elim) "A dependent version of `AddSubsemigroup.closure_induction`. "]
theorem closure_induction' ( s : Set M ) { p : β x , x β closure s β Prop }
( Hs : β ( x ) ( h : x β s ), p x ( subset_closure h ))
( Hmul : β x hx y hy , p x hx β p y hy β p ( x * y ) ( mul_mem hx hy )) { x } ( hx : x β closure s ) :
p x hx := by
refine' Exists.elim : β {Ξ± : Sort ?u.17078} {p : Ξ± β Prop b : Prop }, (β x , p x ) β (β (a : Ξ± ), p a b ) β b _ fun ( hx : x β closure s ) ( hc : p x hx ) => hc
exact
closure_induction : β {M : Type ?u.17160} [inst : Mul M s : Set M p : M β Prop x : M },
x β closure s (β (x : M ), x β s p x ) β (β (x y : M ), p x p y p (x * y ) β p x hx ( fun x hx => β¨ _ , Hs x hx β©) fun x y β¨ hx' , hx β© β¨ hy' , hy β© =>
β¨ _ , Hmul _ _ _ _ hx hy β©
#align subsemigroup.closure_induction' Subsemigroup.closure_induction'
#align add_subsemigroup.closure_induction' AddSubsemigroup.closure_induction'
/-- An induction principle for closure membership for predicates with two arguments. -/
@[ to_additive ( attr := elab_as_elim) "An induction principle for additive closure membership for
predicates with two arguments."]
theorem closure_inductionβ : β {p : M β M β Prop x y : M },
x β closure s y β closure s (β (x : M ), x β s β (y : M ), y β s p x y ) β
(β (x y z : M ), p x z p y z p (x * y z ) β (β (x y z : M ), p z x p z y p z (x * y ) β p x y closure_inductionβ { p : M β M β Prop } { x } { y : M } ( hx : x β closure s ) ( hy : y β closure s )
( Hs : β (x : M ), x β s β (y : M ), y β s p x y Hs : β x β s , β y β s , p x y ) ( Hmul_left : β (x y z : M ), p x z p y z p (x * y z Hmul_left : β x y z , p x z β p y z β p ( x * y ) z )
( Hmul_right : β (x y z : M ), p z x p z y p z (x * y Hmul_right : β x y z , p z x β p z y β p z ( x * y )) : p x y :=
closure_induction : β {M : Type ?u.18024} [inst : Mul M s : Set M p : M β Prop x : M },
x β closure s (β (x : M ), x β s p x ) β (β (x y : M ), p x p y p (x * y ) β p x hx
( fun x xs => closure_induction : β {M : Type ?u.18098} [inst : Mul M s : Set M p : M β Prop x : M },
x β closure s (β (x : M ), x β s p x ) β (β (x y : M ), p x p y p (x * y ) β p x hy ( Hs : β (x : M ), x β s β (y : M ), y β s p x y Hs x xs ) fun z _ hβ hβ => Hmul_right : β (x y z : M ), p z x p z y p z (x * y Hmul_right z _ _ hβ hβ )
fun _ _ hβ hβ => Hmul_left : β (x y z : M ), p x z p y z p (x * y z Hmul_left _ _ _ hβ hβ
#align subsemigroup.closure_inductionβ Subsemigroup.closure_inductionβ : β {M : Type u_1} [inst : Mul M s : Set M p : M β M β Prop x y : M },
x β closure s y β closure s (β (x : M ), x β s β (y : M ), y β s p x y ) β
(β (x y z : M ), p x z p y z p (x * y z ) β (β (x y z : M ), p z x p z y p z (x * y ) β p x y
#align add_subsemigroup.closure_inductionβ AddSubsemigroup.closure_inductionβ
/-- If `s` is a dense set in a magma `M`, `Subsemigroup.closure s = β€`, then in order to prove that
some predicate `p` holds for all `x : M` it suffices to verify `p x` for `x β s`,
and verify that `p x` and `p y` imply `p (x * y)`. -/
@[ to_additive ( attr := elab_as_elim) "If `s` is a dense set in an additive monoid `M`,
`AddSubsemigroup.closure s = β€`, then in order to prove that some predicate `p` holds
for all `x : M` it suffices to verify `p x` for `x β s`, and verify that `p x` and `p y` imply
`p (x + y)`."]
theorem dense_induction : β {p : M β Prop x : M ) {s : Set M closure s = β€ (β (x : M ), x β s p x ) β (β (x y : M ), p x p y p (x * y ) β p x dense_induction { p : M β Prop } ( x : M ) { s : Set M } ( hs : closure s = β€ ) ( Hs : β (x : M ), x β s p x Hs : β x β s , p x )
( Hmul : β (x y : M ), p x p y p (x * y Hmul : β x y , p x β p y β p ( x * y )) : p x := by
have : β x β closure s , p x := fun x hx => closure_induction : β {M : Type ?u.18715} [inst : Mul M s : Set M p : M β Prop x : M },
x β closure s (β (x : M ), x β s p x ) β (β (x y : M ), p x p y p (x * y ) β p x hx Hs : β (x : M ), x β s p x Hs Hmul : β (x y : M ), p x p y p (x * y Hmul
simpa [ hs ] using this x
#align subsemigroup.dense_induction Subsemigroup.dense_induction : β {M : Type u_1} [inst : Mul M p : M β Prop x : M ) {s : Set M closure s = β€ (β (x : M ), x β s p x ) β (β (x y : M ), p x p y p (x * y ) β p x
#align add_subsemigroup.dense_induction AddSubsemigroup.dense_induction : β {M : Type u_1} [inst : Add M p : M β Prop x : M ) {s : Set M AddSubsemigroup.closure s = β€ (β (x : M ), x β s p x ) β (β (x y : M ), p x p y p (x + y ) β p x
variable ( M )
/-- `closure` forms a Galois insertion with the coercion to set. -/
@[ to_additive "`closure` forms a Galois insertion with the coercion to set."]
protected def gi : GaloisInsertion : {Ξ± : Type ?u.19155} β
{Ξ² : Type ?u.19154} β [inst : Preorder Ξ± [inst : Preorder Ξ² (Ξ± β Ξ² (Ξ² β Ξ± Type (max?u.19155?u.19154) (@ closure M _) SetLike.coe :=
GaloisConnection.toGaloisInsertion ( fun _ _ => closure_le ) fun _ => subset_closure
#align subsemigroup.gi Subsemigroup.gi
#align add_subsemigroup.gi AddSubsemigroup.gi
variable { M }
/-- Closure of a subsemigroup `S` equals `S`. -/
@[ to_additive ( attr := simp ) "Additive closure of an additive subsemigroup `S` equals `S`"]
theorem closure_eq : closure ( S : Set M ) = S :=
( Subsemigroup.gi M ). l_u_eq S
#align subsemigroup.closure_eq Subsemigroup.closure_eq
#align add_subsemigroup.closure_eq AddSubsemigroup.closure_eq
@[ to_additive ( attr := simp )]
theorem closure_empty : closure ( β
: Set M ) = β₯ :=
( Subsemigroup.gi M ). gc . l_bot
#align subsemigroup.closure_empty Subsemigroup.closure_empty
#align add_subsemigroup.closure_empty AddSubsemigroup.closure_empty
@[ to_additive ( attr := simp )]
theorem closure_univ : closure ( univ : {Ξ± : Type ?u.20325} β Set Ξ± : Set M ) = β€ :=
@ coe_top : β {M : Type ?u.20385} [inst : Mul M ββ€ = univ M _ βΈ closure_eq β€
#align subsemigroup.closure_univ Subsemigroup.closure_univ
#align add_subsemigroup.closure_univ AddSubsemigroup.closure_univ
@[ to_additive ]
theorem closure_union ( s t : Set M ) : closure ( s βͺ t ) = closure s β closure t :=
( Subsemigroup.gi M ). gc . l_sup
#align subsemigroup.closure_union Subsemigroup.closure_union
#align add_subsemigroup.closure_union AddSubsemigroup.closure_union
@[ to_additive ]
theorem closure_iUnion { ΞΉ } ( s : ΞΉ β Set M ) : closure (β i , s i ) = β¨ i , closure ( s i ) :=
( Subsemigroup.gi M ). gc . l_iSup
#align subsemigroup.closure_Union Subsemigroup.closure_iUnion
#align add_subsemigroup.closure_Union AddSubsemigroup.closure_iUnion
@[ to_additive ]
theorem closure_singleton_le_iff_mem ( m : M ) ( p : Subsemigroup : (M : Type ?u.21199) β [inst : Mul M Type ?u.21199 M ) : closure { m } β€ p β m β p := by
rw [ closure_le , singleton_subset_iff : β {Ξ± : Type ?u.21361} {a : Ξ± } {s : Set Ξ± {a } β s β a β s , SetLike.mem_coe ]
#align subsemigroup.closure_singleton_le_iff_mem Subsemigroup.closure_singleton_le_iff_mem
#align add_subsemigroup.closure_singleton_le_iff_mem AddSubsemigroup.closure_singleton_le_iff_mem
@[ to_additive ]
theorem mem_iSup { ΞΉ : Sort _ } ( p : ΞΉ β Subsemigroup : (M : Type ?u.21492) β [inst : Mul M Type ?u.21492 M ) { m : M } :
( m β β¨ i , p i ) β β N , (β i , p i β€ N ) β m β N := by
rw [ β closure_singleton_le_iff_mem , le_iSup_iff ]
simp only [ closure_singleton_le_iff_mem ]
#align subsemigroup.mem_supr Subsemigroup.mem_iSup
#align add_subsemigroup.mem_supr AddSubsemigroup.mem_iSup
@[ to_additive ]
theorem iSup_eq_closure { ΞΉ : Sort _ } ( p : ΞΉ β Subsemigroup : (M : Type ?u.22203) β [inst : Mul M Type ?u.22203 M ) :
(β¨ i , p i ) = Subsemigroup.closure (β i , ( p i : Set M )) := by
simp_rw [ Subsemigroup.closure_iUnion ,