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, Mitchell Rowett, Scott Morrison, Johan Commelin, Mario Carneiro,
Michael Howes
! This file was ported from Lean 3 source module deprecated.subgroup
! leanprover-community/mathlib commit f93c11933efbc3c2f0299e47b8ff83e9b539cbf6
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.GroupTheory.Subgroup.Basic
import Mathlib.Deprecated.Submonoid
/-!
# Unbundled subgroups (deprecated)
This file is deprecated, and is no longer imported by anything in mathlib other than other
deprecated files, and test files. You should not need to import it.
This file defines unbundled multiplicative and additive subgroups. Instead of using this file,
please use `Subgroup G` and `AddSubgroup A`, defined in `GroupTheory.Subgroup.Basic`.
## Main definitions
`IsAddSubgroup (S : Set A)` : the predicate that `S` is the underlying subset of an additive
subgroup of `A`. The bundled variant `AddSubgroup A` should be used in preference to this.
`IsSubgroup (S : Set G)` : the predicate that `S` is the underlying subset of a subgroup
of `G`. The bundled variant `Subgroup G` should be used in preference to this.
## Tags
subgroup, subgroups, IsSubgroup
-/
open Set Function
variable { G : Type _ : Type (?u.39733+1)} { H : Type _ } { A : Type _ } { a aβ aβ b c : G }
section Group
variable [ Group G ] [ AddGroup A ]
/-- `s` is an additive subgroup: a set containing 0 and closed under addition and negation. -/
structure IsAddSubgroup ( s : Set A ) extends IsAddSubmonoid s : Prop where
/-- The proposition that `s` is closed under negation. -/
neg_mem { a } : a β s β - a β s
#align is_add_subgroup IsAddSubgroup
/-- `s` is a subgroup: a set containing 1 and closed under multiplication and inverse. -/
@[ to_additive ]
structure IsSubgroup ( s : Set G ) extends IsSubmonoid s : Prop where
/-- The proposition that `s` is closed under inverse. -/
inv_mem { a } : a β s β a β»ΒΉ β s
#align is_subgroup IsSubgroup
@[ to_additive ]
theorem IsSubgroup.div_mem { s : Set G } ( hs : IsSubgroup s ) { x y : G } ( hx : x β s ) ( hy : y β s ) :
x / y β s := by simpa only [ div_eq_mul_inv ] using hs . mul_mem hx ( hs . inv_mem hy )
#align is_subgroup.div_mem IsSubgroup.div_mem
#align is_add_subgroup.sub_mem IsAddSubgroup.sub_mem
theorem Additive.isAddSubgroup { s : Set G } ( hs : IsSubgroup s ) : @ IsAddSubgroup ( Additive G ) _ s :=
@ IsAddSubgroup.mk ( Additive G ) _ _ ( Additive.isAddSubmonoid hs . toIsSubmonoid ) hs . inv_mem
#align additive.is_add_subgroup Additive.isAddSubgroup
theorem Additive.isAddSubgroup_iff { s : Set G } : @ IsAddSubgroup ( Additive G ) _ s β IsSubgroup s :=
β¨ by rintro β¨ β¨ hβ , hβ β© , hβ β© ; exact @ IsSubgroup.mk G _ _ β¨ hβ , @ hβ β© @ hβ , fun h =>
Additive.isAddSubgroup h β©
#align additive.is_add_subgroup_iff Additive.isAddSubgroup_iff
theorem Multiplicative.isSubgroup { s : Set A } ( hs : IsAddSubgroup s ) :
@ IsSubgroup ( Multiplicative : Type ?u.3288 β Type ?u.3288 A ) _ s :=
@ IsSubgroup.mk ( Multiplicative : Type ?u.3306 β Type ?u.3306 A ) _ _ ( Multiplicative.isSubmonoid hs . toIsAddSubmonoid ) hs . neg_mem
#align multiplicative.is_subgroup Multiplicative.isSubgroup
theorem Multiplicative.isSubgroup_iff { s : Set A } :
@ IsSubgroup ( Multiplicative : Type ?u.3710 β Type ?u.3710 A ) _ s β IsAddSubgroup s :=
β¨ by rintro β¨ β¨ hβ , hβ β© , hβ β© ; exact @ IsAddSubgroup.mk A _ _ β¨ hβ , @ hβ β© @ hβ , fun h =>
Multiplicative.isSubgroup h β©
#align multiplicative.is_subgroup_iff Multiplicative.isSubgroup_iff
@[ to_additive of_add_neg ]
theorem IsSubgroup.of_div ( s : Set G ) ( one_mem : ( 1 : G ) β s )
( div_mem : β { a b : G }, a β s β b β s β a * b β»ΒΉ β s ) : IsSubgroup s :=
have inv_mem : β a , a β s β a β»ΒΉ β s := fun a ha => by
have : 1 * a β»ΒΉ β s := div_mem one_mem ha
convert this using 1
rw [ one_mul ]
{ inv_mem := inv_mem _
mul_mem := fun { a b } ha hb => by
have : a * b β»ΒΉβ»ΒΉ β s := div_mem ha ( inv_mem b hb )
convert this
rw [ inv_inv ]
one_mem }
#align is_subgroup.of_div IsSubgroup.of_div
#align is_add_subgroup.of_add_neg IsAddSubgroup.of_add_neg
theorem IsAddSubgroup.of_sub ( s : Set A ) ( zero_mem : ( 0 : A ) β s )
( sub_mem : β {a b : A }, a β s b β s a - b β s sub_mem : β { a b : A }, a β s β b β s β a - b β s ) : IsAddSubgroup s :=
IsAddSubgroup.of_add_neg s zero_mem fun { x y } hx hy => by
simpa only [ sub_eq_add_neg ] using sub_mem : β {a b : A }, a β s b β s a - b β s sub_mem hx hy
#align is_add_subgroup.of_sub IsAddSubgroup.of_sub
@[ to_additive ]
theorem IsSubgroup.inter { sβ sβ : Set G } ( hsβ : IsSubgroup sβ ) ( hsβ : IsSubgroup sβ ) :
IsSubgroup ( sβ β© sβ ) :=
{ IsSubmonoid.inter hsβ . toIsSubmonoid hsβ . toIsSubmonoid with
inv_mem := fun hx => β¨ hsβ . inv_mem hx . 1 , hsβ . inv_mem hx . 2 β© }
#align is_subgroup.inter IsSubgroup.inter
#align is_add_subgroup.inter IsAddSubgroup.inter
@[ to_additive ]
theorem IsSubgroup.iInter { ΞΉ : Sort _ } { s : ΞΉ β Set G } ( hs : β y : ΞΉ , IsSubgroup ( s y )) :
IsSubgroup ( Set.iInter : {Ξ² : Type ?u.11045} β {ΞΉ : Sort ?u.11044} β (ΞΉ β Set Ξ² Set Ξ² s ) :=
{ IsSubmonoid.iInter fun y => ( hs y ). toIsSubmonoid with
inv_mem := fun h =>
Set.mem_iInter : β {Ξ± : Type ?u.11463} {ΞΉ : Sort ?u.11464} {x : Ξ± } {s : ΞΉ β Set Ξ± (x β Set.iInter fun i => s i β β (i : ΞΉ ), x β s i . 2 : β {a b : Prop }, (a β b b β a fun y => IsSubgroup.inv_mem ( hs _ ) ( Set.mem_iInter : β {Ξ± : Type ?u.11497} {ΞΉ : Sort ?u.11498} {x : Ξ± } {s : ΞΉ β Set Ξ± (x β Set.iInter fun i => s i β β (i : ΞΉ ), x β s i . 1 : β {a b : Prop }, (a β b a β b h y ) }
#align is_subgroup.Inter IsSubgroup.iInter
#align is_add_subgroup.Inter IsAddSubgroup.iInter
@[ to_additive ]
theorem isSubgroup_iUnion_of_directed { ΞΉ : Type _ : Type (?u.11620+1)} [ Nonempty ΞΉ ] { s : ΞΉ β Set G }
( hs : β i , IsSubgroup ( s i )) ( directed : β (i j : ΞΉ ), β k , s i β s k β§ s j β s k directed : β i j , β k , s i β s k β§ s j β s k ) :
IsSubgroup (β i , s i ) :=
{ inv_mem := fun ha =>
let β¨ i , hi β© := Set.mem_iUnion : β {Ξ± : Type ?u.12166} {ΞΉ : Sort ?u.12167} {x : Ξ± } {s : ΞΉ β Set Ξ± (x β iUnion fun i => s i β β i , x β s i . 1 : β {a b : Prop }, (a β b a β b ha
Set.mem_iUnion : β {Ξ± : Type ?u.12219} {ΞΉ : Sort ?u.12220} {x : Ξ± } {s : ΞΉ β Set Ξ± (x β iUnion fun i => s i β β i , x β s i . 2 : β {a b : Prop }, (a β b b β a β¨ i , ( hs i ). inv_mem hi β©
toIsSubmonoid := isSubmonoid_iUnion_of_directed ( fun i => ( hs i ). toIsSubmonoid ) directed : β (i j : ΞΉ ), β k , s i β s k β§ s j β s k directed }
#align is_subgroup_Union_of_directed isSubgroup_iUnion_of_directed
#align is_add_subgroup_Union_of_directed isAddSubgroup_iUnion_of_directed
end Group
namespace IsSubgroup
open IsSubmonoid
variable [ Group G ] { s : Set G } ( hs : IsSubgroup s )
@[ to_additive ]
theorem inv_mem_iff : a β»ΒΉ β s β a β s :=
β¨ fun h => by simpa using hs . inv_mem h , inv_mem hs β©
#align is_subgroup.inv_mem_iff IsSubgroup.inv_mem_iff
#align is_add_subgroup.neg_mem_iff IsAddSubgroup.neg_mem_iff
@[ to_additive ]
theorem mul_mem_cancel_right ( h : a β s ) : b * a β s β b β s :=
β¨ fun hba => by simpa using hs . mul_mem hba ( hs . inv_mem h ) , fun hb => hs . mul_mem hb h β©
#align is_subgroup.mul_mem_cancel_right IsSubgroup.mul_mem_cancel_right
#align is_add_subgroup.add_mem_cancel_right IsAddSubgroup.add_mem_cancel_right
@[ to_additive ]
theorem mul_mem_cancel_left ( h : a β s ) : a * b β s β b β s :=
β¨ fun hab => by simpa using hs . mul_mem ( hs . inv_mem h ) hab , hs . mul_mem h β©
#align is_subgroup.mul_mem_cancel_left IsSubgroup.mul_mem_cancel_left
#align is_add_subgroup.add_mem_cancel_left IsAddSubgroup.add_mem_cancel_left
end IsSubgroup
/-- `IsNormalAddSubgroup (s : Set A)` expresses the fact that `s` is a normal additive subgroup
of the additive group `A`. Important: the preferred way to say this in Lean is via bundled
subgroups `S : AddSubgroup A` and `hs : S.normal`, and not via this structure. -/
structure IsNormalAddSubgroup [ AddGroup : Type ?u.16114 β Type ?u.16114 A ] ( s : Set A ) extends IsAddSubgroup s : Prop where
/-- The proposition that `s` is closed under (additive) conjugation. -/
normal : β n β s , β g : A , g + n + - g β s
#align is_normal_add_subgroup IsNormalAddSubgroup
/-- `IsNormalSubgroup (s : Set G)` expresses the fact that `s` is a normal subgroup
of the group `G`. Important: the preferred way to say this in Lean is via bundled
subgroups `S : Subgroup G` and not via this structure. -/
@[ to_additive ]
structure IsNormalSubgroup [ Group G ] ( s : Set G ) extends IsSubgroup s : Prop where
/-- The proposition that `s` is closed under conjugation. -/
normal : β n β s , β g : G , g * n * g β»ΒΉ β s
#align is_normal_subgroup IsNormalSubgroup
@[ to_additive ]
theorem isNormalSubgroup_of_commGroup [ CommGroup : Type ?u.18689 β Type ?u.18689 G ] { s : Set G } ( hs : IsSubgroup s ) :
IsNormalSubgroup s :=
{ hs with normal := fun n hn g => by rwa [ mul_right_comm , mul_right_inv , one_mul ] }
#align is_normal_subgroup_of_comm_group isNormalSubgroup_of_commGroup
#align is_normal_add_subgroup_of_add_comm_group isNormalAddSubgroup_of_addCommGroup
theorem Additive.isNormalAddSubgroup [ Group G ] { s : Set G } ( hs : IsNormalSubgroup s ) :
@ IsNormalAddSubgroup ( Additive : Type ?u.19620 β Type ?u.19620 G ) _ s :=
@ IsNormalAddSubgroup.mk ( Additive : Type ?u.19639 β Type ?u.19639 G ) _ _ ( Additive.isAddSubgroup hs . toIsSubgroup )
(@ IsNormalSubgroup.normal _ βΉGroup (Additive G)βΊ _ hs )
-- porting note: Lean needs help synthesising
#align additive.is_normal_add_subgroup Additive.isNormalAddSubgroup
theorem Additive.isNormalAddSubgroup_iff [ Group G ] { s : Set G } :
@ IsNormalAddSubgroup ( Additive : Type ?u.20805 β Type ?u.20805 G ) _ s β IsNormalSubgroup s :=
β¨ by rintro β¨ hβ , hβ β© ; exact @ IsNormalSubgroup.mk G _ _ ( Additive.isAddSubgroup_iff . 1 : β {a b : Prop }, (a β b a β b hβ ) @ hβ ,
fun h => Additive.isNormalAddSubgroup h β©
#align additive.is_normal_add_subgroup_iff Additive.isNormalAddSubgroup_iff
theorem Multiplicative.isNormalSubgroup [ AddGroup : Type ?u.21006 β Type ?u.21006 A ] { s : Set A } ( hs : IsNormalAddSubgroup s ) :
@ IsNormalSubgroup ( Multiplicative : Type ?u.21043 β Type ?u.21043 A ) _ s :=
@ IsNormalSubgroup.mk ( Multiplicative : Type ?u.21062 β Type ?u.21062 A ) _ _ ( Multiplicative.isSubgroup hs . toIsAddSubgroup )
(@ IsNormalAddSubgroup.normal _ βΉAddGroup (Multiplicative A)βΊ _ hs )
#align multiplicative.is_normal_subgroup Multiplicative.isNormalSubgroup
theorem Multiplicative.isNormalSubgroup_iff [ AddGroup : Type ?u.22220 β Type ?u.22220 A ] { s : Set A } :
@ IsNormalSubgroup ( Multiplicative : Type ?u.22227 β Type ?u.22227 A ) _ s β IsNormalAddSubgroup s :=
β¨ by
rintro β¨ hβ , hβ β© ;
exact @ IsNormalAddSubgroup.mk A _ _ ( Multiplicative.isSubgroup_iff . 1 : β {a b : Prop }, (a β b a β b hβ ) @ hβ ,
fun h => Multiplicative.isNormalSubgroup h β©
#align multiplicative.is_normal_subgroup_iff Multiplicative.isNormalSubgroup_iff
namespace IsSubgroup
variable [ Group G ]
-- Normal subgroup properties
@[ to_additive ]
theorem mem_norm_comm { s : Set G } ( hs : IsNormalSubgroup s ) { a b : G } ( hab : a * b β s ) :
b * a β s := by
have h : a β»ΒΉ * ( a * b ) * a β»ΒΉβ»ΒΉ β s := hs . normal ( a * b ) hab a β»ΒΉ
simp at h ; exact h
#align is_subgroup.mem_norm_comm IsSubgroup.mem_norm_comm
#align is_add_subgroup.mem_norm_comm IsAddSubgroup.mem_norm_comm
@[ to_additive ]
theorem mem_norm_comm_iff { s : Set G } ( hs : IsNormalSubgroup s ) { a b : G } : a * b β s β b * a β s :=
β¨ mem_norm_comm hs , mem_norm_comm hs β©
#align is_subgroup.mem_norm_comm_iff IsSubgroup.mem_norm_comm_iff
#align is_add_subgroup.mem_norm_comm_iff IsAddSubgroup.mem_norm_comm_iff
/-- The trivial subgroup -/
@[ to_additive "the trivial additive subgroup"]
def trivial ( G : Type _ : Type (?u.27395+1)) [ Group G ] : Set G :=
{ 1 }
#align is_subgroup.trivial IsSubgroup.trivial : (G : Type u_1) β [inst : Group G Set G
#align is_add_subgroup.trivial IsAddSubgroup.trivial
@[ to_additive ( attr := simp )]
theorem mem_trivial { g : G } : g β trivial G β g = 1 :=
mem_singleton_iff : β {Ξ± : Type ?u.28194} {a b : Ξ± }, a β {b } β a = b
#align is_subgroup.mem_trivial IsSubgroup.mem_trivial
#align is_add_subgroup.mem_trivial IsAddSubgroup.mem_trivial
@[ to_additive ]
theorem trivial_normal : IsNormalSubgroup ( trivial G ) := by
refine' { .. } refine'_1 refine'_2 refine'_3 refine'_4 <;> refine'_1 refine'_2 refine'_3 refine'_4 simp ( config := { contextual := true }) [ trivial ]
#align is_subgroup.trivial_normal IsSubgroup.trivial_normal
#align is_add_subgroup.trivial_normal IsAddSubgroup.trivial_normal
@[ to_additive ]
theorem eq_trivial_iff { s : Set G } ( hs : IsSubgroup s ) : s = trivial G β β x β s , x = ( 1 : G ) := by
simp only [ Set.ext_iff , IsSubgroup.mem_trivial ] ;
exact β¨ fun h x => ( h x ). 1 : β {a b : Prop }, (a β b a β b , fun h x => β¨ h x , fun hx => hx . symm : β {Ξ± : Sort ?u.35199} {a b : Ξ± }, a = b b = a βΈ hs . toIsSubmonoid . one_mem β©β©
#align is_subgroup.eq_trivial_iff IsSubgroup.eq_trivial_iff
#align is_add_subgroup.eq_trivial_iff IsAddSubgroup.eq_trivial_iff
@[ to_additive ]
theorem univ_subgroup : IsNormalSubgroup (@ univ : {Ξ± : Type ?u.35637} β Set Ξ± G ) := by refine' { .. } refine'_1 refine'_2 β {a b : G }, a β univ b β univ a * b β univ refine'_3 refine'_4 <;> refine'_1 refine'_2 β {a b : G }, a β univ b β univ a * b β univ refine'_3 refine'_4 simp
#align is_subgroup.univ_subgroup IsSubgroup.univ_subgroup
#align is_add_subgroup.univ_add_subgroup IsAddSubgroup.univ_addSubgroup
/-- The underlying set of the center of a group. -/
@[ to_additive addCenter "The underlying set of the center of an additive group."]
def center ( G : Type _ : Type (?u.38576+1)) [ Group G ] : Set G :=
{ z | β g , g * z = z * g }
#align is_subgroup.center IsSubgroup.center : (G : Type u_1) β [inst : Group G Set G
#align is_add_subgroup.add_center IsAddSubgroup.addCenter
@[ to_additive mem_add_center ]
theorem mem_center { a : G } : a β center G β β g , g * a = a * g :=
Iff.rfl
#align is_subgroup.mem_center IsSubgroup.mem_center
#align is_add_subgroup.mem_add_center IsAddSubgroup.mem_add_center
@[ to_additive add_center_normal ]
theorem center_normal : IsNormalSubgroup ( center G ) :=
{ one_mem := by simp [ center ]
mul_mem := fun ha hb g => by
g * (aβ * bβ = aβ * bβ * g rw [ g * (aβ * bβ = aβ * bβ * g β mul_assoc : β {G : Type ?u.49232} [inst : Semigroup G a b c : G ), a * b * c = a * (b * c , g * aβ * bβ = aβ * bβ * g g * (aβ * bβ = aβ * bβ * g mem_center . 2 : β {a b : Prop }, (a β b b β a ha g , aβ * g * bβ = aβ * bβ * g g * (aβ * bβ = aβ * bβ * g mul_assoc : β {G : Type ?u.49592} [inst : Semigroup G a b c : G ), a * b * c = a * (b * c , aβ * (g * bβ = aβ * bβ * g g * (aβ * bβ = aβ * bβ * g mem_center . 2 : β {a b : Prop }, (a β b b β a hb g , aβ * (bβ * g = aβ * bβ * g g * (aβ * bβ = aβ * bβ * g β mul_assoc : β {G : Type ?u.49680} [inst : Semigroup G a b c : G ), a * b * c = a * (b * c aβ * bβ * g = aβ * bβ * g ]
inv_mem := fun { a } ha g =>
calc
g * a β»ΒΉ = a β»ΒΉ * ( g * a ) * a β»ΒΉ := by simp [ ha g ]
_ = a β»ΒΉ * g := by rw [ β mul_assoc : β {G : Type ?u.50189} [inst : Semigroup G a b c : G ), a * b * c = a * (b * c , mul_assoc : β {G : Type ?u.50252} [inst : Semigroup G a b c : G ), a * b * c = a * (b * c ] ; simp
normal := fun n ha g h =>
calc
h * ( g * n * g β»ΒΉ) = h * n := by simp [ ha g , mul_assoc : β {G : Type ?u.50817} [inst : Semigroup G a b c : G ), a * b * c = a * (b * c ]
_ = g * g β»ΒΉ * n * h := by rw [ ha h ] ; simp
_ = g * n * g β»ΒΉ * h := by rw [ mul_assoc : β {G : Type ?u.50979} [inst : Semigroup G a b c : G ), a * b * c = a * (b * c g , ha g β»ΒΉ, β mul_assoc : β {G : Type ?u.51031} [inst : Semigroup G a b c : G ), a * b * c = a * (b * c ]
}
#align is_subgroup.center_normal IsSubgroup.center_normal
#align is_add_subgroup.add_center_normal IsAddSubgroup.add_center_normal
/-- The underlying set of the normalizer of a subset `S : Set G` of a group `G`. That is,
the elements `g : G` such that `g * S * gβ»ΒΉ = S`. -/
@[ to_additive addNormalizer
"The underlying set of the normalizer of a subset `S : Set A` of an
additive group `A`. That is, the elements `a : A` such that `a + S - a = S`."]
def normalizer ( s : Set G ) : Set G :=
{ g : G | β n , n β s β g * n * g β»ΒΉ β s }
#align is_subgroup.normalizer IsSubgroup.normalizer : {G : Type u_1} β [inst : Group G Set G Set G
#align is_add_subgroup.add_normalizer IsAddSubgroup.addNormalizer
@[ to_additive ]
theorem normalizer_isSubgroup ( s : Set G ) : IsSubgroup ( normalizer s ) :=
{ one_mem := by simp [ normalizer ]
mul_mem := fun { a b }
( ha : β n , n β s β a * n * a β»ΒΉ β s ) ( hb : β n , n β s β b * n * b β»ΒΉ β s ) n =>
by rw [ mul_inv_rev , β mul_assoc : β {G : Type ?u.57704} [inst : Semigroup G a b c : G ), a * b * c = a * (b * c , mul_assoc : β {G : Type ?u.58023} [inst : Semigroup G a b c : G ), a * b * c = a * (b * c a , mul_assoc : β {G : Type ?u.58034} [inst : Semigroup G a b c : G ), a * b * c = a * (b * c a , β ha , β hb ]
inv_mem := fun { a } ( ha : β n , n β s β a * n * a β»ΒΉ β s ) n => by
rw [ ha ( a β»ΒΉ * n * a β»ΒΉβ»ΒΉ) ] ; simp [ mul_assoc : β {G : Type ?u.58792} [inst : Semigroup G a b c : G ), a * b * c = a * (b * c ] }
#align is_subgroup.normalizer_is_subgroup IsSubgroup.normalizer_isSubgroup : β {G :