mathlib docs: ring_theory.algebra

source

@[instance]

def submodule.has_one {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] :

has_one (submodule R A)

Equations

submodule.has_one = {one := submodule.map (algebra.of_id R A).to_linear_map ⊤}

source

theorem submodule.one_eq_map_top {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] :

1 = submodule.map (algebra.of_id R A).to_linear_map ⊤

source

theorem submodule.one_eq_span {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] :

1 = submodule.span R {1}

source

theorem submodule.one_le {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] {P : submodule R A} :

1 ≤ P ↔ 1 ∈ P

source

@[instance]

def submodule.has_mul {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] :

has_mul (submodule R A)

Equations

submodule.has_mul = {mul := λ (M N : submodule R A), ⨆ (s : ↥M), submodule.map (⇑(algebra.lmul R A) s.val) N}

source

theorem submodule.mul_mem_mul {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] {M N : submodule R A} {m n : A} :

m ∈ M → n ∈ N → m * n ∈ M * N

source

theorem submodule.mul_le {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] {M N P : submodule R A} :

M * N ≤ P ↔ ∀ (m : A), m ∈ M → ∀ (n : A), n ∈ N → m * n ∈ P

source

theorem submodule.mul_induction_on {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] {M N : submodule R A} {C : A → Prop} {r : A} :

r ∈ M * N → (∀ (m : A), m ∈ M → ∀ (n : A), n ∈ N → C (m * n)) → C 0 → (∀ (x y : A), C x → C y → C (x + y)) → (∀ (r : R) (x : A), C x → C (r • x)) → C r

source

theorem submodule.span_mul_span (R : Type u) [comm_semiring R] {A : Type v} [semiring A] [algebra R A] (S T : set A) :

submodule.span R S * submodule.span R T = submodule.span R (S * T)

source

theorem submodule.mul_assoc {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] (M N P : submodule R A) :

M * N * P = M * (N * P)

source

@[simp]

theorem submodule.mul_bot {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] (M : submodule R A) :

M * ⊥ = ⊥

source

@[simp]

theorem submodule.bot_mul {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] (M : submodule R A) :

⊥ * M = ⊥

source

@[simp]

theorem submodule.one_mul {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] (M : submodule R A) :

1 * M = M

source

@[simp]

theorem submodule.mul_one {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] (M : submodule R A) :

M * 1 = M

source

theorem submodule.mul_le_mul {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] {M N P Q : submodule R A} :

M ≤ P → N ≤ Q → M * N ≤ P * Q

source

theorem submodule.mul_le_mul_left {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] {M N P : submodule R A} :

M ≤ N → M * P ≤ N * P

source

theorem submodule.mul_le_mul_right {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] {M N P : submodule R A} :

N ≤ P → M * N ≤ M * P

source

theorem submodule.mul_sup {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] (M N P : submodule R A) :

M * (N ⊔ P) = M * N ⊔ M * P

source

theorem submodule.sup_mul {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] (M N P : submodule R A) :

(M ⊔ N) * P = M * P ⊔ N * P

source

theorem submodule.mul_subset_mul {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] (M N : submodule R A) :

↑M * ↑N ⊆ ↑(M * N)

source

theorem submodule.map_mul {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] (M N : submodule R A) {A' : Type u_1} [semiring A'] [algebra R A'] (f : A →ₐ[R] A') :

submodule.map f.to_linear_map (M * N) = submodule.map f.to_linear_map M * submodule.map f.to_linear_map N

source

@[instance]

def submodule.semiring {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] :

semiring (submodule R A)

Equations

submodule.semiring = {add := add_comm_monoid.add submodule.add_comm_monoid_submodule, add_assoc := _, zero := add_comm_monoid.zero submodule.add_comm_monoid_submodule, zero_add := _, add_zero := _, add_comm := _, mul := has_mul.mul submodule.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _}

source

theorem submodule.pow_subset_pow {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] (M : submodule R A) {n : ℕ} :

↑M ^ n ⊆ ↑(M ^ n)

source

def submodule.span.ring_hom {R : Type u} [comm_semiring R] {A : Type v} [semiring A] [algebra R A] :

set.set_semiring A →+* submodule R A

span is a semiring homomorphism (recall multiplication is pointwise multiplication of subsets on either side).

Equations

submodule.span.ring_hom = {to_fun := submodule.span R algebra.to_semimodule, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}

source

theorem submodule.mul_mem_mul_rev {R : Type u} [comm_semiring R] {A : Type v} [comm_semiring A] [algebra R A] {M N : submodule R A} {m n : A} :

m ∈ M → n ∈ N → n * m ∈ M * N

source

theorem submodule.mul_comm {R : Type u} [comm_semiring R] {A : Type v} [comm_semiring A] [algebra R A] (M N : submodule R A) :

M * N = N * M

source

@[instance]

def submodule.comm_semiring {R : Type u} [comm_semiring R] {A : Type v} [comm_semiring A] [algebra R A] :

comm_semiring (submodule R A)

Equations

submodule.comm_semiring = {add := semiring.add submodule.semiring, add_assoc := _, zero := semiring.zero submodule.semiring, zero_add := _, add_zero := _, add_comm := _, mul := semiring.mul submodule.semiring, mul_assoc := _, one := semiring.one submodule.semiring, one_mul := _, mul_one := _, zero_mul := _, mul_zero := _, left_distrib := _, right_distrib := _, mul_comm := _}

source

@[instance]

def submodule.semimodule_set (R : Type u) [comm_semiring R] (A : Type v) [comm_semiring A] [algebra R A] :

semimodule (set.set_semiring A) (submodule R A)

Equations

submodule.semimodule_set R A = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := λ (s : set.set_semiring A) (P : submodule R A), submodule.span R s * P}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}

source

theorem submodule.smul_def {R : Type u} [comm_semiring R] {A : Type v} [comm_semiring A] [algebra R A] {s : set.set_semiring A} {P : submodule R A} :

s • P = submodule.span R s * P

source

theorem submodule.smul_le_smul {R : Type u} [comm_semiring R] {A : Type v} [comm_semiring A] [algebra R A] {s t : set.set_semiring A} {M N : submodule R A} :

s.down ≤ t.down → M ≤ N → s • M ≤ t • N

source

theorem submodule.smul_singleton {R : Type u} [comm_semiring R] {A : Type v} [comm_semiring A] [algebra R A] (a : A) (M : submodule R A) :

{a}.up • M = submodule.map (algebra.lmul_left R A a) M

source

@[instance]

def submodule.has_div {R : Type u} [comm_semiring R] {A : Type v} [comm_semiring A] [algebra R A] :

has_div (submodule R A)

The elements of I / J are the x such that x • J ⊆ I.

In fact, we define x ∈ I / J to be ∀ y ∈ J, x * y ∈ I (see mem_div_iff_forall_mul_mem), which is equivalent to x • J ⊆ I (see mem_div_iff_smul_subset), but nicer to use in proofs.

This is the general form of the ideal quotient, traditionally written $I : J$.

Equations

submodule.has_div = {div := λ (I J : submodule R A), {carrier := {x : A | ∀ (y : A), y ∈ J → x * y ∈ I}, zero_mem' := _, add_mem' := _, smul_mem' := _}}

source

theorem submodule.mem_div_iff_forall_mul_mem {R : Type u} [comm_semiring R] {A : Type v} [comm_semiring A] [algebra R A] {x : A} {I J : submodule R A} :

x ∈ I / J ↔ ∀ (y : A), y ∈ J → x * y ∈ I

source

theorem submodule.mem_div_iff_smul_subset {R : Type u} [comm_semiring R] {A : Type v} [comm_semiring A] [algebra R A] {x : A} {I J : submodule R A} :

x ∈ I / J ↔ x • ↑J ⊆ ↑I

source

theorem submodule.le_div_iff {R : Type u} [comm_semiring R] {A : Type v} [comm_semiring A] [algebra R A] {I J K : submodule R A} :

I ≤ J / K ↔ ∀ (x : A), x ∈ I → ∀ (z : A), z ∈ K → x * z ∈ J

mathlib documentation

ring_theory.algebra_operations

General documentation

Additional documentation

Library

mathlib documentation

ring_theory.​algebra_operations

General documentation

Additional documentation

Library

ring_theory.algebra_operations