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 Chris Hughes. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Chris Hughes
! This file was ported from Lean 3 source module group_theory.group_action.basic
! 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.Data.Fintype.Card
import Mathlib.GroupTheory.GroupAction.Defs
import Mathlib.GroupTheory.GroupAction.Group
import Mathlib.Data.Setoid.Basic
import Mathlib.Data.Set.Pointwise.SMul
import Mathlib.GroupTheory.Subgroup.Basic
/-!
# Basic properties of group actions
This file primarily concerns itself with orbits, stabilizers, and other objects defined in terms of
actions. Despite this file being called `basic`, low-level helper lemmas for algebraic manipulation
of `•` belong elsewhere.
## Main definitions
* `MulAction.orbit`
* `MulAction.fixedPoints`
* `MulAction.fixedBy`
* `MulAction.stabilizer`
-/
universe u v w
variable { α : Type u } { β : Type v } { γ : Type w }
open Pointwise
open Function
namespace MulAction
variable ( α ) [ Monoid α ] [ MulAction : (α : Type ?u.2725) → Type ?u.2724 → [inst : Monoid α Type (max?u.2725?u.2724) α β ]
/-- The orbit of an element under an action. -/
@[ to_additive "The orbit of an element under an action."]
def orbit ( b : β ) :=
Set.range : {α : Type ?u.61} → {ι : Sort ?u.60} → (ι → α Set α fun x : α => x • b
#align mul_action.orbit MulAction.orbit
#align add_action.orbit AddAction.orbit
variable { α }
@[ to_additive ]
theorem mem_orbit_iff { b₁ b₂ : β } : b₂ ∈ orbit α b₁ ↔ ∃ x : α , x • b₁ = b₂ :=
Iff.rfl : ∀ {a : Prop }, a ↔ a
#align mul_action.mem_orbit_iff MulAction.mem_orbit_iff
#align add_action.mem_orbit_iff AddAction.mem_orbit_iff
@[ to_additive ( attr := simp )]
theorem mem_orbit : ∀ (b : β ) (x : α ), x • b ∈ orbit α b mem_orbit ( b : β ) ( x : α ) : x • b ∈ orbit α b :=
⟨ x , rfl : ∀ {α : Sort ?u.2601} {a : α }, a = a ⟩
#align mul_action.mem_orbit MulAction.mem_orbit
#align add_action.mem_orbit AddAction.mem_orbit
@[ to_additive ( attr := simp )]
theorem mem_orbit_self : ∀ (b : β ), b ∈ orbit α b mem_orbit_self ( b : β ) : b ∈ orbit α b :=
⟨ 1 , by simp [ MulAction.one_smul ] ⟩
#align mul_action.mem_orbit_self MulAction.mem_orbit_self
#align add_action.mem_orbit_self AddAction.mem_orbit_self
@[ to_additive ]
theorem orbit_nonempty ( b : β ) : Set.Nonempty ( orbit α b ) :=
Set.range_nonempty _
#align mul_action.orbit_nonempty MulAction.orbit_nonempty
#align add_action.orbit_nonempty AddAction.orbit_nonempty
@[ to_additive ]
theorem mapsTo_smul_orbit ( a : α ) ( b : β ) : Set.MapsTo ( (· • ·) a ) ( orbit α b ) ( orbit α b ) :=
Set.range_subset_iff : ∀ {α : Type ?u.5519} {ι : Sort ?u.5520} {f : ι → α s : Set α Set.range f ⊆ s ↔ ∀ (y : ι ), f y ∈ s . 2 : ∀ {a b : Prop }, (a ↔ b b → a fun a' => ⟨ a * a' , mul_smul _ _ _ ⟩
#align mul_action.maps_to_smul_orbit MulAction.mapsTo_smul_orbit
#align add_action.maps_to_vadd_orbit AddAction.mapsTo_vadd_orbit
@[ to_additive ]
theorem smul_orbit_subset : ∀ (a : α ) (b : β ), a • orbit α b ⊆ orbit α b smul_orbit_subset ( a : α ) ( b : β ) : a • orbit α b ⊆ orbit α b :=
( mapsTo_smul_orbit a b ). image_subset
#align mul_action.smul_orbit_subset MulAction.smul_orbit_subset
#align add_action.vadd_orbit_subset AddAction.vadd_orbit_subset
@[ to_additive ]
theorem orbit_smul_subset : ∀ (a : α ) (b : β ), orbit α (a • b ⊆ orbit α b orbit_smul_subset ( a : α ) ( b : β ) : orbit α ( a • b ) ⊆ orbit α b :=
Set.range_subset_iff : ∀ {α : Type ?u.8231} {ι : Sort ?u.8232} {f : ι → α s : Set α Set.range f ⊆ s ↔ ∀ (y : ι ), f y ∈ s . 2 : ∀ {a b : Prop }, (a ↔ b b → a fun a' => mul_smul a' a b ▸ mem_orbit _ _
#align mul_action.orbit_smul_subset MulAction.orbit_smul_subset
#align add_action.orbit_vadd_subset AddAction.orbit_vadd_subset
@[ to_additive ]
instance { b : β } : MulAction : (α : Type ?u.8446) → Type ?u.8445 → [inst : Monoid α Type (max?u.8446?u.8445) α ( orbit α b ) where
smul a := ( mapsTo_smul_orbit a b ). restrict : {α : Type ?u.8655} → {β : Type ?u.8654} → (f : α → β (s : Set α (t : Set β Set.MapsTo f s t ↑s → ↑t restrict _ _ _
one_smul a := Subtype.ext : ∀ {α : Sort ?u.8692} {p : α → Prop a1 a2 : { x // p x }, ↑a1 = ↑a2 a1 = a2 ( one_smul α ( a : β ))
mul_smul a a' b' := Subtype.ext : ∀ {α : Sort ?u.8801} {p : α → Prop a1 a2 : { x // p x }, ↑a1 = ↑a2 a1 = a2 ( mul_smul a a' ( b' : β ))
@[ to_additive ( attr := simp )]
theorem orbit.coe_smul { b : β } { a : α } { b' : orbit α b } : ↑( a • b' ) = a • ( b' : β ) :=
rfl : ∀ {α : Sort ?u.11531} {a : α }, a = a
#align mul_action.orbit.coe_smul MulAction.orbit.coe_smul
#align add_action.orbit.coe_vadd AddAction.orbit.coe_vadd
variable ( α ) ( β )
/-- The set of elements fixed under the whole action. -/
@[ to_additive "The set of elements fixed under the whole action."]
def fixedPoints : Set β :=
{ b : β | ∀ x : α , x • b = b }
#align mul_action.fixed_points MulAction.fixedPoints
#align add_action.fixed_points AddAction.fixedPoints
/-- `fixedBy g` is the subfield of elements fixed by `g`. -/
@[ to_additive "`fixedBy g` is the subfield of elements fixed by `g`."]
def fixedBy ( g : α ) : Set β :=
{ x | g • x = x }
#align mul_action.fixed_by MulAction.fixedBy
#align add_action.fixed_by AddAction.fixedBy
@[ to_additive ]
theorem fixed_eq_iInter_fixedBy : fixedPoints α β = ⋂ g : α , fixedBy α β g :=
Set.ext : ∀ {α : Type ?u.13360} {a b : Set α (∀ (x : α ), x ∈ a ↔ x ∈ b ) → a = b fun _ =>
⟨ fun hx => Set.mem_iInter : ∀ {α : Type ?u.13382} {ι : Sort ?u.13383} {x : α } {s : ι → Set α (x ∈ Set.iInter fun i => s i ↔ ∀ (i : ι ), x ∈ s i . 2 : ∀ {a b : Prop }, (a ↔ b b → a fun g => hx g , fun hx g => ( Set.mem_iInter : ∀ {α : Type ?u.13425} {ι : Sort ?u.13426} {x : α } {s : ι → Set α (x ∈ Set.iInter fun i => s i ↔ ∀ (i : ι ), x ∈ s i . 1 : ∀ {a b : Prop }, (a ↔ b a → b hx g : _ )⟩
#align mul_action.fixed_eq_Inter_fixed_by MulAction.fixed_eq_iInter_fixedBy
#align add_action.fixed_eq_Inter_fixed_by AddAction.fixed_eq_iInter_fixedBy
variable { α }
@[ to_additive ( attr := simp )]
theorem mem_fixedPoints { b : β } : b ∈ fixedPoints α β ↔ ∀ x : α , x • b = b :=
Iff.rfl : ∀ {a : Prop }, a ↔ a
#align mul_action.mem_fixed_points MulAction.mem_fixedPoints
#align add_action.mem_fixed_points AddAction.mem_fixedPoints
@[ to_additive ( attr := simp )]
theorem mem_fixedBy { g : α } { b : β } : b ∈ fixedBy α β g ↔ g • b = b :=
Iff.rfl : ∀ {a : Prop }, a ↔ a
#align mul_action.mem_fixed_by MulAction.mem_fixedBy
#align add_action.mem_fixed_by AddAction.mem_fixedBy
@[ to_additive ]
theorem mem_fixedPoints' { b : β } : b ∈ fixedPoints α β ↔ ∀ b' , b' ∈ orbit α b → b' = b :=
⟨ fun h _ h₁ =>
let ⟨ x , hx ⟩ := mem_orbit_iff . 1 : ∀ {a b : Prop }, (a ↔ b a → b h₁
hx ▸ h x ,
fun h _ => h _ ( mem_orbit _ _ )⟩
#align mul_action.mem_fixed_points' MulAction.mem_fixedPoints'
#align add_action.mem_fixed_points' AddAction.mem_fixedPoints'
variable ( α ) { β }
/-- The stabilizer of a point `b` as a submonoid of `α`. -/
@[ to_additive "The stabilizer of a point `b` as an additive submonoid of `α`."]
def Stabilizer.submonoid ( b : β ) : Submonoid α where
carrier := { a | a • b = b }
one_mem' := one_smul _ b
mul_mem' { a a' } ( ha : a • b = b ) ( hb : a' • b = b ) :=
show ( a * a' ) • b = b by rw [ ← smul_smul : ∀ {M : Type ?u.19788} {α : Type ?u.19787} [inst : Monoid M inst_1 : MulAction M α a₁ a₂ : M ) (b : α ),
a₁ • a₂ • b = (a₁ * a₂ • b , hb , ha ]
#align mul_action.stabilizer.submonoid MulAction.Stabilizer.submonoid
#align add_action.stabilizer.add_submonoid AddAction.Stabilizer.addSubmonoid
@[ to_additive ( attr := simp )]
theorem mem_stabilizer_submonoid_iff { b : β } { a : α } : a ∈ Stabilizer.submonoid α b ↔ a • b = b :=
Iff.rfl : ∀ {a : Prop }, a ↔ a
#align mul_action.mem_stabilizer_submonoid_iff MulAction.mem_stabilizer_submonoid_iff
#align add_action.mem_stabilizer_add_submonoid_iff AddAction.mem_stabilizer_addSubmonoid_iff
@[ to_additive ]
theorem orbit_eq_univ [ IsPretransitive : (M : Type ?u.21119) → (α : Type ?u.21118) → [inst : SMul M α Prop α β ] ( x : β ) : orbit α x = Set.univ : {α : Type ?u.21850} → Set α :=
( surjective_smul α x ). range_eq
#align mul_action.orbit_eq_univ MulAction.orbit_eq_univ
#align add_action.orbit_eq_univ AddAction.orbit_eq_univ
variable { α }
@[ to_additive ]
theorem mem_fixedPoints_iff_card_orbit_eq_one { a : β } [ Fintype ( orbit α a )] :
a ∈ fixedPoints α β ↔ Fintype.card ( orbit α a ) = 1 := by
rw [ Fintype.card_eq_one_iff , mem_fixedPoints (∀ (x : α ), x • a = a ) ↔ ∃ x , ∀ (y : ↑(orbit α a ), y = x ] (∀ (x : α ), x • a = a ) ↔ ∃ x , ∀ (y : ↑(orbit α a ), y = x
constructor mp (∀ (x : α ), x • a = a ) → ∃ x , ∀ (y : ↑(orbit α a ), y = x mpr (∃ x , ∀ (y : ↑(orbit α a ), y = x ) → ∀ (x : α ), x • a = a
· mp (∀ (x : α ), x • a = a ) → ∃ x , ∀ (y : ↑(orbit α a ), y = x mp (∀ (x : α ), x • a = a ) → ∃ x , ∀ (y : ↑(orbit α a ), y = x mpr (∃ x , ∀ (y : ↑(orbit α a ), y = x ) → ∀ (x : α ), x • a = a exact fun h => ⟨⟨ a , mem_orbit_self _ ⟩, fun ⟨ b , ⟨ x , hx : (fun x => x • a ) x = b hx ⟩⟩ => Subtype.eq : ∀ {α : Type ?u.23266} {p : α → Prop a1 a2 : { x // p x }, ↑a1 = ↑a2 a1 = a2 <| mp (∀ (x : α ), x • a = a ) → ∃ x , ∀ (y : ↑(orbit α a ), y = x by ↑{ val := b , property := (_ : ∃ y , (fun x => x • a ) y = b ) } = ↑{ val := a , property := (_ : a ∈ orbit α a } simp [ h x , hx : (fun x => x • a ) x = b hx . symm : ∀ {α : Sort ?u.23402} {a b : α }, a = b b = a ] ⟩
· mpr (∃ x , ∀ (y : ↑(orbit α a ), y = x ) → ∀ (x : α ), x • a = a mpr (∃ x , ∀ (y : ↑(orbit α a ), y = x ) → ∀ (x : α ), x • a = a intro h x
mpr (∃ x , ∀ (y : ↑(orbit α a ), y = x ) → ∀ (x : α ), x • a = a rcases h with ⟨ ⟨ z , hz ⟩ , hz₁ : unknown free variable '_uniq.23510'
hz₁ ⟩
mpr (∃ x , ∀ (y : ↑(orbit α a ), y = x ) → ∀ (x : α ), x • a = a calc
x • a = z := Subtype.mk.inj : ∀ {α : Sort ?u.24267} {p : α → Prop val : α } {property : p val val_1 : α } {property_1 : p val_1 { val := val , property := property } = { val := val_1 , property := property_1 } val = val_1 ( hz₁ : ∀ (y : ↑(orbit α a ), y = { val := z , property := hz } hz₁ ⟨ x • a , mem_orbit _ _ ⟩)
_ = a := ( Subtype.mk.inj : ∀ {α : Sort ?u.24984} {p : α → Prop val : α } {property : p val val_1 : α } {property_1 : p val_1 { val := val , property := property } = { val := val_1 , property := property_1 } val = val_1 ( hz₁ : ∀ (y : ↑(orbit α a ), y = { val := z , property := hz } hz₁ ⟨ a , mem_orbit_self _ ⟩)). symm : ∀ {α : Sort ?u.25080} {a b : α }, a = b b = a symm
#align mul_action.mem_fixed_points_iff_card_orbit_eq_one MulAction.mem_fixedPoints_iff_card_orbit_eq_one
#align add_action.mem_fixed_points_iff_card_orbit_eq_zero AddAction.mem_fixedPoints_iff_card_orbit_eq_zero
end MulAction
namespace MulAction
variable ( α )
variable [ Group α ] [ MulAction : (α : Type ?u.52365) → Type ?u.52364 → [inst : Monoid α Type (max?u.52365?u.52364) α β ]
/-- The stabilizer of an element under an action, i.e. what sends the element to itself.
A subgroup. -/
@[ to_additive
"The stabilizer of an element under an action, i.e. what sends the element to itself.
An additive subgroup."]
def stabilizer ( b : β ) : Subgroup α :=
{ Stabilizer.submonoid α b with
inv_mem' := fun { a } ( ha : a • b = b ) => show a ⁻¹ • b = b by rw [ inv_smul_eq_iff , ha ] }
#align mul_action.stabilizer MulAction.stabilizer
#align add_action.stabilizer AddAction.stabilizer
variable { α }
@[ to_additive ( attr := simp )]
theorem mem_stabilizer_iff { b : β } { a : α } : a ∈ stabilizer α b ↔ a • b = b :=
Iff.rfl : ∀ {a : Prop }, a ↔ a
#align mul_action.mem_stabilizer_iff MulAction.mem_stabilizer_iff
#align add_action.mem_stabilizer_iff AddAction.mem_stabilizer_iff
@[ to_additive ( attr := simp )]
theorem smul_orbit ( a : α ) ( b : β ) : a • orbit α b = orbit α b :=
( smul_orbit_subset a b ). antisymm <|
calc
orbit α b = a • a ⁻¹ • orbit α b := ( smul_inv_smul _ _ ). symm : ∀ {α : Sort ?u.34071} {a b : α }, a = b b = a symm
_ ⊆ a • orbit α b := Set.image_subset : ∀ {α : Type ?u.34973} {β : Type ?u.34974} {a b : Set α f : α → β a ⊆ b f '' a ⊆ f '' b _ ( smul_orbit_subset _ _ )
#align mul_action.smul_orbit MulAction.smul_orbit
#align add_action.vadd_orbit AddAction.vadd_orbit
@[ to_additive ( attr := simp )]
theorem orbit_smul ( a : α ) ( b : β ) : orbit α ( a • b ) = orbit α b :=
( orbit_smul_subset a b ). antisymm <|
calc
orbit α b = orbit α ( a ⁻¹ • a • b ) := by rw [ inv_smul_smul ]
_ ⊆ orbit α ( a • b ) := orbit_smul_subset _ _
#align mul_action.orbit_smul MulAction.orbit_smul
#align add_action.orbit_vadd AddAction.orbit_vadd
/-- The action of a group on an orbit is transitive. -/
@[ to_additive "The action of an additive group on an orbit is transitive."]
instance ( x : β ) : IsPretransitive : (M : Type ?u.40072) → (α : Type ?u.40071) → [inst : SMul M α Prop α ( orbit α x ) :=
⟨ by
∀ (x_1 y : ↑(orbit α x ), ∃ g , g • x_1 = y rintro ⟨ _ , a , rfl : (fun x_1 => x_1 • x ) a = val✝ ⟩ ⟨ _ , b , rfl : (fun x_1 => x_1 • x ) b = val✝ ⟩ mk.intro.mk.intro ∃ g ,
g • { val := (fun x_1 => x_1 • x ) a , property := (_ : ∃ y , (fun x_1 => x_1 • x ) y = (fun x_1 => x_1 • x ) a ) } = { val := (fun x_1 => x_1 • x ) b , property := (_ : ∃ y , (fun x_1 => x_1 • x ) y = (fun x_1 => x_1 • x ) b ) }
∀ (x_1 y : ↑(orbit α x ), ∃ g , g • x_1 = y use b * a ⁻¹ mk.intro.mk.intro (b * a ⁻¹ • { val := (fun x_1 => x_1 • x ) a , property := (_ : ∃ y , (fun x_1 => x_1 • x ) y = (fun x_1 => x_1 • x ) a ) } = { val := (fun x_1 => x_1 • x ) b , property := (_ : ∃ y , (fun x_1 => x_1 • x ) y = (fun x_1 => x_1 • x ) b ) }
∀ (x_1 y : ↑(orbit α x ), ∃ g , g • x_1 = y ext1 mk.intro.mk.intro.a ↑((b * a ⁻¹ • { val := (fun x_1 => x_1 • x ) a , property := (_ : ∃ y , (fun x_1 => x_1 • x ) y = (fun x_1 => x_1 • x ) a ) } ) = ↑{ val := (fun x_1 => x_1 • x ) b , property := (_ : ∃ y , (fun x_1 => x_1 • x ) y = (fun x_1 => x_1 • x ) b ) }
∀ (x_1 y : ↑(orbit α x ), ∃ g , g • x_1 = y simp [ mul_smul ] ⟩
@[ to_additive ]
theorem orbit_eq_iff { a b : β } : orbit α a = orbit α b ↔ a ∈ orbit α b :=
⟨ fun h => h ▸ mem_orbit_self _ , fun ⟨_, hc : (fun x => x • b ) w✝ = a hc ⟩ => hc : (fun x => x • b ) w✝ = a hc ▸ orbit_smul _ _ ⟩
#align mul_action.orbit_eq_iff MulAction.orbit_eq_iff
#align add_action.orbit_eq_iff AddAction.orbit_eq_iff
variable ( α )
@[ to_additive ]
theorem mem_orbit_smul ( g : α ) ( a : β ) : a ∈ orbit α ( g • a ) := by
simp only [ orbit_smul , mem_orbit_self ]
#align mul_action.mem_orbit_smul MulAction.mem_orbit_smul
#align add_action.mem_orbit_vadd AddAction.mem_orbit_vadd
@[ to_additive ]
theorem smul_mem_orbit_smul : ∀ (g h : α ) (a : β ), g • a ∈ orbit α (h • a smul_mem_orbit_smul ( g h : α ) ( a : β ) : g • a ∈ orbit α ( h • a ) := by
simp only [ orbit_smul , mem_orbit ]
#align mul_action.smul_mem_orbit_smul MulAction.smul_mem_orbit_smul
#align add_action.vadd_mem_orbit_vadd AddAction.vadd_mem_orbit_vadd
variable ( β )
/-- The relation 'in the same orbit'. -/
@[ to_additive "The relation 'in the same orbit'."]
def orbitRel : Setoid : Sort ?u.52654 → Sort (max1?u.52654) β where
r a b := a ∈ orbit α b
iseqv :=
⟨ mem_orbit_self , fun { a b } => by simp [ orbit_eq_iff . symm : ∀ {a b : Prop }, (a ↔ b b ↔ a , eq_comm : ∀ {α : Sort ?u.53484} {a b : α }, a = b ↔ b = a ] , fun { a b } => by
simp ( config := { contextual := true }) [ orbit_eq_iff . symm : ∀ {a b : Prop }, (a ↔ b b ↔ a , eq_comm : ∀ {α : Sort ?u.54346} {a b : α }, a = b ↔ b = a ] ⟩
#align mul_action.orbit_rel MulAction.orbitRel
#align add_action.orbit_rel AddAction.orbitRel
variable { α } { β }
/-- When you take a set `U` in `β`, push it down to the quotient, and pull back, you get the union
of the orbit of `U` under `α`. -/
@[ to_additive
"When you take a set `U` in `β`, push it down to the quotient, and pull back, you get the
union of the orbit of `U` under `α`."]
theorem quotient_preimage_image_eq_union_mul ( U : Set β ) :
letI := orbitRel α β
Quotient.mk' ⁻¹' ( Quotient.mk' '' U ) = ⋃ a : α , (· • ·) a '' U := by
letI := orbitRel α β
set f : β → Quotient ( MulAction.orbitRel α β ) := Quotient.mk'
ext x
constructor
· rintro ⟨ y , hy , hxy ⟩
obtain ⟨ a , rfl : (fun x_1 => x_1 • x ) a = y ⟩ := Quotient.exact hxy
rw [ Set.mem_iUnion : ∀ {α : Type ?u.59525} {ι : Sort ?u.59526} {x : α } {s : ι → Set α (x ∈ Set.iUnion fun i => s i ↔ ∃ i , x ∈ s i h.mp.intro.intro.intro ∃ i , x ∈ (fun x x_1 => x • x_1 ) i '' U ] h.mp.intro.intro.intro ∃ i , x ∈ (fun x x_1 => x • x_1 ) i '' U
exact ⟨ a ⁻¹, a • x , hy : (fun x_1 => x_1 • x ) a ∈ U hy , inv_smul_smul a x ⟩
· intro hx
rw [ Set.mem_iUnion : ∀ {α : Type ?u.60532} {ι : Sort ?u.60533} {x : α } {s : ι → Set α (x ∈ Set.iUnion fun i => s i ↔ ∃ i , x ∈ s i ] at hx
obtain ⟨a, u, hu₁, hu₂⟩ : x ∈ (fun x x_1 => x • x_1 ) a '' U a ⟨a, u, hu₁, hu₂⟩ : x ∈ (fun x x_1 => x • x_1 ) a '' U u ⟨a, u, hu₁, hu₂⟩ : x ∈ (fun x x_1 => x • x_1 ) a '' U hu₁ ⟨a, u, hu₁, hu₂⟩ : x ∈ (fun x x_1 => x • x_1 ) a '' U hu₂ : (fun x x_1 => x • x_1 ) a u = x hu₂ ⟨a, u, hu₁, hu₂⟩ : x ∈ (fun x x_1 => x • x_1 ) a '' U := hx : ∃ i , x ∈ (fun x x_1 => x • x_1 ) i '' U hx
rw [ Set.mem_preimage : ∀ {α : Type ?u.60619} {β : Type ?u.60618} {f : α → β s : Set β a : α }, a ∈ f ⁻¹' s ↔ f a ∈ s , Set.mem_image_iff_bex : ∀ {α : Type ?u.60637} {β : Type ?u.60638} {f : α → β s : Set α y : β }, y ∈ f '' s ↔ ∃ x x_1 , f x = y ]
refine' ⟨ a ⁻¹ • x , _ , by simp only [ Quotient.eq' ] ; use a ⁻¹ ⟩
rw [ ← hu₂ : (fun x x_1 => x • x_1 ) a u = x hu₂ h.mpr.intro.intro.intro a ⁻¹ • (fun x x_1 => x • x_1 ) a u ∈ U ] h.mpr.intro.intro.intro a ⁻¹ • (fun x x_1 => x • x_1 ) a u ∈ U
convert hu₁ h.e'_4 a ⁻¹ • (fun x x_1 => x • x_1 ) a u = u
simp only [ inv_smul_smul ]
#align mul_action.quotient_preimage_image_eq_union_mul MulAction.quotient_preimage_image_eq_union_mul
#align add_action.quotient_preimage_image_eq_union_add AddAction.quotient_preimage_image_eq_union_add
@[ to_additive ]
theorem disjoint_image_image_iff { U V : Set β } :
letI := orbitRel α β
Disjoint ( Quotient.mk' '' U ) ( Quotient.mk' '' V ) ↔ ∀ x ∈ U , ∀ a : α , a • x ∉ V := by
Disjoint (Quotient.mk' '' U Quotient.mk' '' V ↔ ∀ (x : β ), x ∈ U ∀ (a : α ), ¬ a • x ∈ V letI := orbitRel α β Disjoint (Quotient.mk' '' U Quotient.mk' '' V ↔ ∀ (x : β ), x ∈ U ∀ (a : α ), ¬ a • x ∈ V
Disjoint (Quotient.mk' '' U Quotient.mk' '' V ↔ ∀ (x : β ), x ∈ U ∀ (a : α ), ¬ a • x ∈ V set f : β → Quotient ( MulAction.orbitRel α β ) := Quotient.mk'
Disjoint (Quotient.mk' '' U Quotient.mk' '' V ↔ ∀ (x : β ), x ∈ U ∀ (a : α ), ¬ a • x ∈ V refine'
⟨ fun h x x_in_U a a_in_V =>
h . le_bot ⟨⟨ x , x_in_U , Quotient.sound ⟨ a ⁻¹, _ ⟩⟩, ⟨ a • x , a_in_V , rfl : ∀ {α : Sort ?u.67317} {a : α }, a = a ⟩⟩, _ ⟩ refine'_1 (fun x_1 => x_1 • a • x ) a ⁻¹ = x refine'_2
Disjoint (Quotient.mk' '' U Quotient.mk' '' V ↔ ∀ (x : β ), x ∈ U ∀ (a : α ), ¬ a • x ∈ V · refine'_1 (fun x_1 => x_1 • a • x ) a ⁻¹ = x