Pointwise action on sets #
This file proves that several kinds of actions of a type α on another type β transfer to actions
of α/Set α on Set β.
Implementation notes #
- We put all instances in the locale
Pointwise, so that these instances are not available by default. Note that we do not mark them as reducible (as argued by note [reducible non-instances]) since we expect the locale to be open whenever the instances are actually used (and making the instances reducible changes the behavior ofsimp.
Translation/scaling of sets #
theorem
Set.op_smul_set_subset_mul
{α : Type u_2}
[Mul α]
{s t : Set α}
{a : α}
:
a ∈ t → MulOpposite.op a • s ⊆ s * t
theorem
Set.op_vadd_set_subset_add
{α : Type u_2}
[Add α]
{s t : Set α}
{a : α}
:
a ∈ t → AddOpposite.op a +ᵥ s ⊆ s + t
@[simp]
theorem
Set.iUnion_op_smul_set
{α : Type u_2}
[Mul α]
(s t : Set α)
:
⋃ a ∈ t, MulOpposite.op a • s = s * t
@[simp]
theorem
Set.iUnion_op_vadd_set
{α : Type u_2}
[Add α]
(s t : Set α)
:
⋃ a ∈ t, AddOpposite.op a +ᵥ s = s + t
theorem
Set.mul_pair
{α : Type u_2}
[Mul α]
(s : Set α)
(a b : α)
:
s * {a, b} = MulOpposite.op a • s ∪ MulOpposite.op b • s
theorem
Set.add_pair
{α : Type u_2}
[Add α]
(s : Set α)
(a b : α)
:
s + {a, b} = (AddOpposite.op a +ᵥ s) ∪ (AddOpposite.op b +ᵥ s)
theorem
Set.smulCommClass_set
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[SMul α γ]
[SMul β γ]
[SMulCommClass α β γ]
:
SMulCommClass α β (Set γ)
theorem
Set.vaddCommClass_set
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[VAdd α γ]
[VAdd β γ]
[VAddCommClass α β γ]
:
VAddCommClass α β (Set γ)
theorem
Set.smulCommClass_set'
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[SMul α γ]
[SMul β γ]
[SMulCommClass α β γ]
:
SMulCommClass α (Set β) (Set γ)
theorem
Set.vaddCommClass_set'
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[VAdd α γ]
[VAdd β γ]
[VAddCommClass α β γ]
:
VAddCommClass α (Set β) (Set γ)
theorem
Set.smulCommClass_set''
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[SMul α γ]
[SMul β γ]
[SMulCommClass α β γ]
:
SMulCommClass (Set α) β (Set γ)
theorem
Set.vaddCommClass_set''
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[VAdd α γ]
[VAdd β γ]
[VAddCommClass α β γ]
:
VAddCommClass (Set α) β (Set γ)
theorem
Set.smulCommClass
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[SMul α γ]
[SMul β γ]
[SMulCommClass α β γ]
:
SMulCommClass (Set α) (Set β) (Set γ)
theorem
Set.vaddCommClass
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[VAdd α γ]
[VAdd β γ]
[VAddCommClass α β γ]
:
VAddCommClass (Set α) (Set β) (Set γ)
theorem
Set.isScalarTower
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[SMul α β]
[SMul α γ]
[SMul β γ]
[IsScalarTower α β γ]
:
IsScalarTower α β (Set γ)
theorem
Set.vaddAssocClass
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[VAdd α β]
[VAdd α γ]
[VAdd β γ]
[VAddAssocClass α β γ]
:
VAddAssocClass α β (Set γ)
theorem
Set.isScalarTower'
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[SMul α β]
[SMul α γ]
[SMul β γ]
[IsScalarTower α β γ]
:
IsScalarTower α (Set β) (Set γ)
theorem
Set.vaddAssocClass'
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[VAdd α β]
[VAdd α γ]
[VAdd β γ]
[VAddAssocClass α β γ]
:
VAddAssocClass α (Set β) (Set γ)
theorem
Set.isScalarTower''
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[SMul α β]
[SMul α γ]
[SMul β γ]
[IsScalarTower α β γ]
:
IsScalarTower (Set α) (Set β) (Set γ)
theorem
Set.vaddAssocClass''
{α : Type u_2}
{β : Type u_3}
{γ : Type u_4}
[VAdd α β]
[VAdd α γ]
[VAdd β γ]
[VAddAssocClass α β γ]
:
VAddAssocClass (Set α) (Set β) (Set γ)
theorem
Set.isCentralScalar
{α : Type u_2}
{β : Type u_3}
[SMul α β]
[SMul αᵐᵒᵖ β]
[IsCentralScalar α β]
:
IsCentralScalar α (Set β)
theorem
Set.isCentralVAdd
{α : Type u_2}
{β : Type u_3}
[VAdd α β]
[VAdd αᵃᵒᵖ β]
[IsCentralVAdd α β]
:
IsCentralVAdd α (Set β)
def
Set.smulZeroClassSet
{α : Type u_2}
{β : Type u_3}
[Zero β]
[SMulZeroClass α β]
:
SMulZeroClass α (Set β)
If scalar multiplication by elements of α sends (0 : β) to zero,
then the same is true for (0 : Set β).
Equations
- Set.smulZeroClassSet = SMulZeroClass.mk ⋯
Instances For
def
Set.distribSMulSet
{α : Type u_2}
{β : Type u_3}
[AddZeroClass β]
[DistribSMul α β]
:
DistribSMul α (Set β)
If the scalar multiplication (· • ·) : α → β → β is distributive,
then so is (· • ·) : α → Set β → Set β.
Equations
- Set.distribSMulSet = DistribSMul.mk ⋯
Instances For
def
Set.distribMulActionSet
{α : Type u_2}
{β : Type u_3}
[Monoid α]
[AddMonoid β]
[DistribMulAction α β]
:
DistribMulAction α (Set β)
A distributive multiplicative action of a monoid on an additive monoid β gives a distributive
multiplicative action on Set β.
Equations
- Set.distribMulActionSet = DistribMulAction.mk ⋯ ⋯
Instances For
def
Set.mulDistribMulActionSet
{α : Type u_2}
{β : Type u_3}
[Monoid α]
[Monoid β]
[MulDistribMulAction α β]
:
MulDistribMulAction α (Set β)
A multiplicative action of a monoid on a monoid β gives a multiplicative action on Set β.
Equations
- Set.mulDistribMulActionSet = MulDistribMulAction.mk ⋯ ⋯
Instances For
theorem
Set.instNoZeroSMulDivisors
{α : Type u_2}
{β : Type u_3}
[Zero α]
[Zero β]
[SMul α β]
[NoZeroSMulDivisors α β]
:
NoZeroSMulDivisors (Set α) (Set β)
theorem
Set.noZeroSMulDivisors_set
{α : Type u_2}
{β : Type u_3}
[Zero α]
[Zero β]
[SMul α β]
[NoZeroSMulDivisors α β]
:
NoZeroSMulDivisors α (Set β)
theorem
Set.instNoZeroDivisors
{α : Type u_2}
[Zero α]
[Mul α]
[NoZeroDivisors α]
:
NoZeroDivisors (Set α)
theorem
Set.image_smul_distrib
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[MulOneClass α]
[MulOneClass β]
[FunLike F α β]
[MonoidHomClass F α β]
(f : F)
(a : α)
(s : Set α)
:
theorem
Set.image_vadd_distrib
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[AddZeroClass α]
[AddZeroClass β]
[FunLike F α β]
[AddMonoidHomClass F α β]
(f : F)
(a : α)
(s : Set α)
:
theorem
Set.smul_zero_subset
{α : Type u_2}
{β : Type u_3}
[Zero β]
[SMulZeroClass α β]
(s : Set α)
:
theorem
Set.Nonempty.smul_zero
{α : Type u_2}
{β : Type u_3}
[Zero β]
[SMulZeroClass α β]
{s : Set α}
(hs : s.Nonempty)
:
theorem
Set.zero_mem_smul_set
{α : Type u_2}
{β : Type u_3}
[Zero β]
[SMulZeroClass α β]
{t : Set β}
{a : α}
(h : 0 ∈ t)
:
theorem
Set.zero_mem_smul_set_iff
{α : Type u_2}
{β : Type u_3}
[Zero β]
[SMulZeroClass α β]
{t : Set β}
{a : α}
[Zero α]
[NoZeroSMulDivisors α β]
(ha : a ≠ 0)
:
Note that we have neither SMulWithZero α (Set β) nor SMulWithZero (Set α) (Set β)
because 0 * ∅ ≠ 0.
theorem
Set.zero_smul_subset
{α : Type u_2}
{β : Type u_3}
[Zero α]
[Zero β]
[SMulWithZero α β]
(t : Set β)
:
theorem
Set.Nonempty.zero_smul
{α : Type u_2}
{β : Type u_3}
[Zero α]
[Zero β]
[SMulWithZero α β]
{t : Set β}
(ht : t.Nonempty)
:
@[simp]
theorem
Set.zero_smul_set
{α : Type u_2}
{β : Type u_3}
[Zero α]
[Zero β]
[SMulWithZero α β]
{s : Set β}
(h : s.Nonempty)
:
A nonempty set is scaled by zero to the singleton set containing 0.
theorem
Set.zero_smul_set_subset
{α : Type u_2}
{β : Type u_3}
[Zero α]
[Zero β]
[SMulWithZero α β]
(s : Set β)
:
theorem
Set.subsingleton_zero_smul_set
{α : Type u_2}
{β : Type u_3}
[Zero α]
[Zero β]
[SMulWithZero α β]
(s : Set β)
:
(0 • s).Subsingleton
theorem
Set.exists_smul_inter_smul_subset_smul_inv_mul_inter_inv_mul
{α : Type u_2}
[Group α]
(s t : Set α)
(a b : α)
:
Any intersection of translates of two sets s and t can be covered by a single translate of
(s⁻¹ * s) ∩ (t⁻¹ * t).
This is useful to show that the intersection of approximate subgroups is an approximate subgroup.
theorem
Set.exists_vadd_inter_vadd_subset_vadd_neg_add_inter_neg_add
{α : Type u_2}
[AddGroup α]
(s t : Set α)
(a b : α)
:
Any intersection of translates of two sets s and t can be covered by a single translate of
(-s + s) ∩ (-t + t).
This is useful to show that the intersection of approximate subgroups is an approximate subgroup.
theorem
Set.smul_graphOn
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[Group α]
[CommGroup β]
[FunLike F α β]
[MonoidHomClass F α β]
(x : α × β)
(s : Set α)
(f : F)
:
x • Set.graphOn (⇑f) s = Set.graphOn (fun (a : α) => x.2 / f x.1 * f a) (x.1 • s)
theorem
Set.vadd_graphOn
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[AddGroup α]
[AddCommGroup β]
[FunLike F α β]
[AddMonoidHomClass F α β]
(x : α × β)
(s : Set α)
(f : F)
:
x +ᵥ Set.graphOn (⇑f) s = Set.graphOn (fun (a : α) => x.2 - f x.1 + f a) (x.1 +ᵥ s)
theorem
Set.smul_graphOn_univ
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[Group α]
[CommGroup β]
[FunLike F α β]
[MonoidHomClass F α β]
(x : α × β)
(f : F)
:
x • Set.graphOn (⇑f) Set.univ = Set.graphOn (fun (a : α) => x.2 / f x.1 * f a) Set.univ
theorem
Set.vadd_graphOn_univ
{F : Type u_1}
{α : Type u_2}
{β : Type u_3}
[AddGroup α]
[AddCommGroup β]
[FunLike F α β]
[AddMonoidHomClass F α β]
(x : α × β)
(f : F)
:
x +ᵥ Set.graphOn (⇑f) Set.univ = Set.graphOn (fun (a : α) => x.2 - f x.1 + f a) Set.univ
theorem
Set.smul_set_univ₀
{α : Type u_2}
{β : Type u_3}
[GroupWithZero α]
[MulAction α β]
{a : α}
(ha : a ≠ 0)
:
theorem
Set.smul_univ₀'
{α : Type u_2}
{β : Type u_3}
[GroupWithZero α]
[MulAction α β]
{s : Set α}
(hs : s.Nontrivial)
:
@[simp]
@[simp]