lean-ga / for_mathlib.algebra.center_submonoid

source

def algebra.center_submonoid.to_sub_mul_action {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (self : algebra.center_submonoid R A) :

sub_mul_action R A

Instances for ↥algebra.center_submonoid.to_sub_mul_action

algebra.center_submonoid.to_sub_mul_action.nonempty

source

def algebra.center_submonoid.to_submonoid {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (self : algebra.center_submonoid R A) :

submonoid A

source

structure algebra.center_submonoid (R : Type u_1) (A : Type u_2) [comm_semiring R] [semiring A] [algebra R A] :

Type u_2

carrier : set A
mul_mem' : ∀ {a b : A}, a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
one_mem' : 1 ∈ self.carrier
smul_mem' : ∀ (c : R) {x : A}, x ∈ self.carrier → c • x ∈ self.carrier

A center_submonoid is a submonoid that includes the central ring of the algebra

Instances for algebra.center_submonoid

algebra.center_submonoid.has_sizeof_inst
algebra.center_submonoid.set_like
algebra.center_submonoid.submonoid_class
algebra.center_submonoid.zero_mem_class

source

@[protected, instance]

def algebra.center_submonoid.set_like {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] :

set_like (algebra.center_submonoid R A) A

Equations

algebra.center_submonoid.set_like = {coe := algebra.center_submonoid.carrier _inst_3, coe_injective' := _}

source

@[protected, instance]

def algebra.center_submonoid.submonoid_class {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] :

submonoid_class (algebra.center_submonoid R A) A

source

@[protected, instance]

def algebra.center_submonoid.to_sub_mul_action.nonempty {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (S : algebra.center_submonoid R A) :

nonempty ↥(S.to_sub_mul_action)

source

@[protected, instance]

def algebra.center_submonoid.zero_mem_class {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] :

zero_mem_class (algebra.center_submonoid R A) A

source

theorem algebra.center_submonoid.smul_mem {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (S : algebra.center_submonoid R A) (r : R) {a : A} :

a ∈ S → r • a ∈ S

source

@[protected]

theorem algebra.center_submonoid.mul_mem {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (S : algebra.center_submonoid R A) {a b : A} :

a ∈ S → b ∈ S → a * b ∈ S

source

@[protected]

theorem algebra.center_submonoid.one_mem {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (S : algebra.center_submonoid R A) :

1 ∈ S

source

@[protected]

theorem algebra.center_submonoid.zero_mem {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (S : algebra.center_submonoid R A) :

0 ∈ S

source

@[simp]

theorem algebra.center_submonoid.algebra_map_mem {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (S : algebra.center_submonoid R A) (r : R) :

⇑(algebra_map R A) r ∈ S

source

def algebra.center_submonoid.closure (R : Type u_1) {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (s : set A) :

algebra.center_submonoid R A

Equations

algebra.center_submonoid.closure R s = let c : submonoid A := submonoid.closure (set.range ⇑(algebra_map R A) ∪ s) in {carrier := c.carrier, mul_mem' := _, one_mem' := _, smul_mem' := _}

source

@[simp]

theorem algebra.center_submonoid.subset_closure (R : Type u_1) {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] {s : set A} :

s ⊆ ↑(algebra.center_submonoid.closure R s)

source

@[simp]

theorem algebra.center_submonoid.closure_to_submonoid (R : Type u_1) {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] {s : set A} :

(algebra.center_submonoid.closure R s).to_submonoid = submonoid.closure (set.range ⇑(algebra_map R A) ∪ s)

source

@[protected, instance]

def algebra.center_submonoid.mul_action {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (S : algebra.center_submonoid R A) :

mul_action R ↥S

Equations

S.mul_action = S.to_sub_mul_action.mul_action

source

@[protected, instance]

def algebra.center_submonoid.monoid_with_zero {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (S : algebra.center_submonoid R A) :

monoid_with_zero ↥S

Equations

S.monoid_with_zero = {mul := monoid.mul S.to_submonoid.to_monoid, mul_assoc := _, one := monoid.one S.to_submonoid.to_monoid, one_mul := _, mul_one := _, npow := monoid.npow S.to_submonoid.to_monoid, npow_zero' := _, npow_succ' := _, zero := 0, zero_mul := _, mul_zero := _}

source

@[protected, instance]

def algebra.center_submonoid.nontrivial {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (S : algebra.center_submonoid R A) [nontrivial A] :

nontrivial ↥S

source

@[simp, norm_cast]

theorem algebra.center_submonoid.coe_zero {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (S : algebra.center_submonoid R A) :

↑0 = 0

source

@[simp, norm_cast]

theorem algebra.center_submonoid.coe_smul {R : Type u_1} {A : Type u_2} [comm_semiring R] [semiring A] [algebra R A] (S : algebra.center_submonoid R A) (k : R) (v : ↥S) :

↑(k • v) = k • ↑v

source

@[simp]

theorem algebra.center_submonoid.neg_mem {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [algebra R A] (S : algebra.center_submonoid R A) (v : A) :

v ∈ S → -v ∈ S

source

@[protected, instance]

def algebra.center_submonoid.has_neg {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [algebra R A] (S : algebra.center_submonoid R A) :

has_neg ↥S

Equations

S.has_neg = S.to_sub_mul_action.has_neg

source

@[simp, norm_cast]

theorem algebra.center_submonoid.coe_neg {R : Type u_1} {A : Type u_2} [comm_ring R] [ring A] [algebra R A] (S : algebra.center_submonoid R A) (v : ↥S) :

↑-v = -↑v

mathlib3 documentation

Submonoids including the central ring #