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) 2022 Eric Wieser. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Eric Wieser
! This file was ported from Lean 3 source module group_theory.group_action.sub_mul_action.pointwise
! leanprover-community/mathlib commit 2bbc7e3884ba234309d2a43b19144105a753292e
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.GroupTheory.GroupAction.SubMulAction
/-!
# Pointwise monoid structures on SubMulAction
This file provides `SubMulAction.Monoid` and weaker typeclasses, which show that `SubMulAction`s
inherit the same pointwise multiplications as sets.
To match `Submodule.idemSemiring`, we do not put these in the `Pointwise` locale.
-/
open Pointwise
variable { R M : Type _ }
namespace SubMulAction
section One
variable [ Monoid R ] [ MulAction R M ] [ One M ]
instance : One ( SubMulAction : (R : Type ?u.60) → (M : Type ?u.59) → [inst : SMul R M Type ?u.59 R M )
where one :=
{ carrier := Set.range : {α : Type ?u.779} → {ι : Sort ?u.778} → (ι → α Set α fun r : R => r • ( 1 : M )
smul_mem' := fun r _ ⟨ r' , hr' : (fun r => r • 1 ) r' = x✝¹ hr' ⟩ => hr' : (fun r => r • 1 ) r' = x✝¹ hr' ▸ ⟨ r * r' , mul_smul _ _ _ ⟩ }
theorem coe_one : ↑( 1 : SubMulAction : (R : Type ?u.3299) → (M : Type ?u.3298) → [inst : SMul R M Type ?u.3298 R M ) = Set.range : {α : Type ?u.2536} → {ι : Sort ?u.2535} → (ι → α Set α fun r : R => r • ( 1 : M ) :=
rfl : ∀ {α : Sort ?u.3998} {a : α }, a = a
#align sub_mul_action.coe_one SubMulAction.coe_one
@[ simp ]
theorem mem_one { x : M } : x ∈ ( 1 : SubMulAction : (R : Type ?u.4046) → (M : Type ?u.4045) → [inst : SMul R M Type ?u.4045 R M ) ↔ ∃ r : R , r • ( 1 : M ) = x :=
Iff.rfl : ∀ {a : Prop }, a ↔ a
#align sub_mul_action.mem_one SubMulAction.mem_one
theorem subset_coe_one : ( 1 : Set M ) ⊆ ( 1 : SubMulAction : (R : Type ?u.5573) → (M : Type ?u.5572) → [inst : SMul R M Type ?u.5572 R M ) := fun _ hx =>
⟨ 1 , ( one_smul _ _ ). trans : ∀ {α : Sort ?u.6911} {a b c : α }, a = b b = c a = c trans hx . symm : ∀ {α : Sort ?u.6963} {a b : α }, a = b b = a ⟩
#align sub_mul_action.subset_coe_one SubMulAction.subset_coe_one
end One
section Mul
variable [ Monoid R ] [ MulAction : (α : Type ?u.8458) → Type ?u.8457 → [inst : Monoid α Type (max?u.8458?u.8457) R M ] [ Mul M ] [ IsScalarTower : (M : Type ?u.14405) →
(N : Type ?u.14404) → (α : Type ?u.14403) → [inst : SMul M N [inst : SMul N α [inst : SMul M α Prop R M M ]
instance : Mul ( SubMulAction : (R : Type ?u.9913) → (M : Type ?u.9912) → [inst : SMul R M Type ?u.9912 R M )
where mul p q :=
{ carrier := Set.image2 : {α : Type ?u.10639} → {β : Type ?u.10638} → {γ : Type ?u.10637} → (α → β → γ Set α Set β Set γ (· * ·) p q
smul_mem' := fun r _ ⟨ m₁ , m₂ , hm₁ , hm₂ , h : (fun x x_1 => x * x_1 ) m₁ m₂ = x✝¹ h ⟩ =>
h : (fun x x_1 => x * x_1 ) m₁ m₂ = x✝¹ h ▸ smul_mul_assoc : ∀ {α : Type ?u.10978} {β : Type ?u.10977} [inst : Mul β inst_1 : SMul α β inst_2 : IsScalarTower α β β r : α )
(x y : β ), r • x * y = r • (x * y r m₁ m₂ ▸ Set.mul_mem_mul : ∀ {α : Type ?u.11012} [inst : Mul α s t : Set α a b : α }, a ∈ s b ∈ t a * b ∈ s * t ( p . smul_mem _ hm₁ ) hm₂ }
@[ norm_cast ]
theorem coe_mul ( p q : SubMulAction : (R : Type ?u.13674) → (M : Type ?u.13673) → [inst : SMul R M Type ?u.13673 R M ) : ↑( p * q ) = ( p * q : Set M ) :=
rfl : ∀ {α : Sort ?u.14226} {a : α }, a = a
#align sub_mul_action.coe_mul SubMulAction.coe_mul
theorem mem_mul { p q : SubMulAction : (R : Type ?u.16551) → (M : Type ?u.16550) → [inst : SMul R M Type ?u.16550 R M } { x : M } : x ∈ p * q ↔ ∃ y z , y ∈ p ∧ z ∈ q ∧ y * z = x :=
Set.mem_mul : ∀ {α : Type ?u.16823} [inst : Mul α s t : Set α a : α }, a ∈ s * t ↔ ∃ x y , x ∈ s ∧ y ∈ t ∧ x * y = a
#align sub_mul_action.mem_mul SubMulAction.mem_mul
end Mul
section MulOneClass
variable [ Monoid R ] [ MulAction : (α : Type ?u.19684) → Type ?u.19683 → [inst : Monoid α Type (max?u.19684?u.19683) R M ] [ MulOneClass : Type ?u.16953 → Type ?u.16953 M ] [ IsScalarTower : (M : Type ?u.19701) →
(N : Type ?u.19700) → (α : Type ?u.19699) → [inst : SMul M N [inst : SMul N α [inst : SMul M α Prop R M M ] [ SMulCommClass : (M : Type ?u.18417) → (N : Type ?u.18416) → (α : Type ?u.18415) → [inst : SMul M α [inst : SMul N α Prop R M M ]
-- porting note: giving the instance the name `mulOneClass`
instance mulOneClass : MulOneClass : Type ?u.22417 → Type ?u.22417 ( SubMulAction : (R : Type ?u.22419) → (M : Type ?u.22418) → [inst : SMul R M Type ?u.22418 R M )
where
mul := (· * ·)
one := 1
mul_one a := by
ext x
simp only [ mem_mul , mem_one , mul_smul_comm : ∀ {α : Type ?u.28185} {β : Type ?u.28184} [inst : Mul β inst_1 : SMul α β inst_2 : SMulCommClass α β β s : α )
(x y : β ), x * s • y = s • (x * y , exists_and_left : ∀ {α : Sort ?u.28215} {p : α → Prop b : Prop }, (∃ x , b ∧ p x ) ↔ b ∧ ∃ x , p x , exists_exists_eq_and : ∀ {α : Sort ?u.28229} {β : Sort ?u.28228} {f : α → β p : β → Prop (∃ b , (∃ a , f a = b ) ∧ p b ) ↔ ∃ a , p (f a , mul_one ] h (∃ y , y ∈ a ∧ ∃ a , a • y = x ) ↔ x ∈ a
constructor h.mp (∃ y , y ∈ a ∧ ∃ a , a • y = x ) → x ∈ a h.mpr x ∈ a ∃ y , y ∈ a ∧ ∃ a , a • y = x
· h.mp (∃ y , y ∈ a ∧ ∃ a , a • y = x ) → x ∈ a h.mp (∃ y , y ∈ a ∧ ∃ a , a • y = x ) → x ∈ a h.mpr x ∈ a ∃ y , y ∈ a ∧ ∃ a , a • y = x rintro ⟨ y , hy , r , rfl ⟩
h.mp (∃ y , y ∈ a ∧ ∃ a , a • y = x ) → x ∈ a exact smul_mem _ _ hy
· h.mpr x ∈ a ∃ y , y ∈ a ∧ ∃ a , a • y = x h.mpr x ∈ a ∃ y , y ∈ a ∧ ∃ a , a • y = x intro hx h.mpr ∃ y , y ∈ a ∧ ∃ a , a • y = x
h.mpr x ∈ a ∃ y , y ∈ a ∧ ∃ a , a • y = x exact ⟨ x , hx , 1 , one_smul _ _ ⟩
one_mul a := by
ext x
simp only [ mem_mul , mem_one , smul_mul_assoc : ∀ {α : Type ?u.24476} {β : Type ?u.24475} [inst : Mul β inst_1 : SMul α β inst_2 : IsScalarTower α β β r : α )
(x y : β ), r • x * y = r • (x * y , exists_and_left : ∀ {α : Sort ?u.24506} {p : α → Prop b : Prop }, (∃ x , b ∧ p x ) ↔ b ∧ ∃ x , p x , exists_exists_eq_and : ∀ {α : Sort ?u.24523} {β : Sort ?u.24522} {f : α → β p : β → Prop (∃ b , (∃ a , f a = b ) ∧ p b ) ↔ ∃ a , p (f a , one_mul ] h (∃ a_1 x_1 , x_1 ∈ a ∧ a_1 • x_1 = x ) ↔ x ∈ a
refine' ⟨ _ , fun hx => ⟨ 1 , x , hx , one_smul _ _ ⟩⟩ h (∃ a_1 x_1 , x_1 ∈ a ∧ a_1 • x_1 = x ) → x ∈ a
rintro ⟨r, y, hy, rfl⟩ : ∃ x_1 , x_1 ∈ a ∧ r • x_1 = x r ⟨r, y, hy, rfl⟩ : ∃ x_1 , x_1 ∈ a ∧ r • x_1 = x y ⟨r, y, hy, rfl⟩ : ∃ x_1 , x_1 ∈ a ∧ r • x_1 = x hy ⟨r, y, hy, rfl⟩ : ∃ x_1 , x_1 ∈ a ∧ r • x_1 = x rfl ⟨r, y, hy, rfl⟩ : ∃ x_1 , x_1 ∈ a ∧ r • x_1 = x
exact smul_mem _ _ hy
end MulOneClass
section Semigroup
variable [ Monoid R ] [ MulAction : (α : Type ?u.29593) → Type ?u.29592 → [inst : Monoid α Type (max?u.29593?u.29592) R M ] [ Semigroup : Type ?u.29605 → Type ?u.29605 M ] [ IsScalarTower : (M : Type ?u.29610) →
(N : Type ?u.29609) → (α : Type ?u.29608) → [inst : SMul M N [inst : SMul N α [inst : SMul M α Prop R M M ]
-- porting note: giving the instance the name `semiGroup`
instance semiGroup : Semigroup : Type ?u.32577 → Type ?u.32577 ( SubMulAction : (R : Type ?u.32579) → (M : Type ?u.32578) → [inst : SMul R M Type ?u.32578 R M )
where
mul := (· * ·)
mul_assoc _ _ _ := SetLike.coe_injective ( mul_assoc : ∀ {G : Type ?u.34373} [inst : Semigroup G a b c : G ), a * b * c = a * (b * c ( _ : Set _ ) _ _ )
end Semigroup
section Monoid
variable [ Monoid R ] [ MulAction : (α : Type ?u.34629) → Type ?u.34628 → [inst : Monoid α Type (max?u.34629?u.34628) R M ] [ Monoid M ] [ IsScalarTower : (M : Type ?u.45187) →
(N : Type ?u.45186) → (α : Type ?u.45185) → [inst : SMul M N [inst : SMul N α [inst : SMul M α Prop R M M ] [ SMulCommClass : (M : Type ?u.46837) → (N : Type ?u.46836) → (α : Type ?u.46835) → [inst : SMul M α [inst : SMul N α Prop R M M ]
instance : Monoid ( SubMulAction : (R : Type ?u.40929) → (M : Type ?u.40928) → [inst : SMul R M Type ?u.40928 R M ) :=
{ SubMulAction.semiGroup ,
SubMulAction.mulOneClass with
mul := (· * ·)
one := 1 }
theorem coe_pow ( p : SubMulAction : (R : Type ?u.48315) → (M : Type ?u.48314) → [inst : SMul R M Type ?u.48314 R M ) : ∀ { n : ℕ } ( _ : n ≠ 0 ), ( p ^ n : Set M ) = (( p : Set M ) ^ n )
| 0 , hn => ( hn rfl : ∀ {α : Sort ?u.60926} {a : α }, a = a ). elim
| 1 , _ => by rw [ pow_one : ∀ {M : Type ?u.61187} [inst : Monoid M a : M ), a ^ 1 = a , pow_one : ∀ {M : Type ?u.61335} [inst : Monoid M a : M ), a ^ 1 = a ]
| n + 2, _ => by
↑(p ^ (n + 2 = ↑p ^ (n + 2 rw [ ↑(p ^ (n + 2 = ↑p ^ (n + 2 pow_succ : ∀ {M : Type ?u.61473} [inst : Monoid M a : M ) (n : ℕ ), a ^ (n + 1 = a * a ^ n _ ( n + 1 ), ↑(p * p ^ (n + 1 = ↑p ^ (n + 2 ↑(p ^ (n + 2 = ↑p ^ (n + 2 pow_succ : ∀ {M : Type ?u.61626} [inst : Monoid M a : M ) (n : ℕ ), a ^ (n + 1 = a * a ^ n _ ( n + 1 ), ↑(p * p ^ (n + 1 = ↑p * ↑p ^ (n + 1 ↑(p ^ (n + 2 = ↑p ^ (n + 2 coe_mul , ↑p * ↑(p ^ (n + 1 = ↑p * ↑p ^ (n + 1 ↑(p ^ (n + 2 = ↑p ^ (n + 2 coe_pow _ n . succ_ne_zero ]
#align sub_mul_action.coe_pow SubMulAction.coe_pow
theorem subset_coe_pow ( p : SubMulAction : (R : Type ?u.65904) → (M : Type ?u.65903) → [inst : SMul R M Type ?u.65903 R M ) : ∀ { n : ℕ }, (( p : Set M ) ^ n ) ⊆ ( p ^ n : Set M )
| 0 => by
rw [ pow_zero : ∀ {M : Type ?u.78648} [inst : Monoid M a : M ), a ^ 0 = 1 , pow_zero : ∀ {M : Type ?u.78793} [inst : Monoid M a : M ), a ^ 0 = 1 ]
exact subset_coe_one
| n + 1 => by ↑p ^ (n + 1 ⊆ ↑(p ^ (n + 1 rw [ ↑p ^ (n + 1 ⊆ ↑(p ^ (n + 1 ← Nat.succ_eq_add_one , ↑p ^ (n + 1 ⊆ ↑(p ^ (n + 1 coe_pow _ n . succ_ne_zero ]
#align sub_mul_action.subset_coe_pow SubMulAction.subset_coe_pow
end Monoid
end SubMulAction