Products of ideals and the auxiliary set bothMul

Sets up bothMul a b = aRb, the algebra IdealProd.ringSubsetProdIdeal, and the monoid structure on TwoSidedIdeal R used throughout the Artin–Wedderburn development.

def LeanPool.ArtinWedderburn.bothMul {R : Type u_1} [Ring R] (a b : R) : Set R

The set aRb = {a * r * b | r : R} of two-sided products through R.

Equations

• LeanPool.ArtinWedderburn.bothMul a b = {x : R | ∃ (r : R), x = a * r * b}

def LeanPool.ArtinWedderburn.«term(_⬝_⬝_)» : Lean.ParserDescr

Notation (a ⬝ R ⬝ b) for bothMul R a b.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev LeanPool.ArtinWedderburn.IdealProd.ringSubsetProdIdeal {R : Type u_1} [Ring R] (A B : Set R) : Ideal R

The (left) ideal generated by all pairwise products a * b with a ∈ A, b ∈ B.

Equations

• LeanPool.ArtinWedderburn.IdealProd.ringSubsetProdIdeal A B = Ideal.span (A * B)

@[implicit_reducible]

instance LeanPool.ArtinWedderburn.IdealProd.instMulIdealLeanPool {R : Type u_1} [Ring R] : Mul (Ideal R)

Equations

• LeanPool.ArtinWedderburn.IdealProd.instMulIdealLeanPool = { mul := fun (I J : Ideal R) => Ideal.span (↑I * ↑J) }

@[reducible, inline]

abbrev LeanPool.ArtinWedderburn.TwoSidedIdealProd.ringSubsetProdTwoSidedIdeal {R : Type u_1} [Ring R] (A B : Set R) : TwoSidedIdeal R

The two-sided ideal generated by all pairwise products a * b with a ∈ A, b ∈ B.

Equations

• LeanPool.ArtinWedderburn.TwoSidedIdealProd.ringSubsetProdTwoSidedIdeal A B = TwoSidedIdeal.span (A * B)

@[implicit_reducible]

instance LeanPool.ArtinWedderburn.TwoSidedIdealProd.instMulTwoSidedIdealLeanPool {R : Type u_1} [Ring R] : Mul (TwoSidedIdeal R)

Equations

• LeanPool.ArtinWedderburn.TwoSidedIdealProd.instMulTwoSidedIdealLeanPool = { mul := fun (I J : TwoSidedIdeal R) => LeanPool.ArtinWedderburn.TwoSidedIdealProd.ringSubsetProdTwoSidedIdeal ↑I ↑J }

theorem LeanPool.ArtinWedderburn.TwoSidedIdealProd.univ_mul_ideal_eq_ideal {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) : Set.univ * ↑I = ↑I

theorem LeanPool.ArtinWedderburn.TwoSidedIdealProd.mul_univ_ideal_eq_ideal {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) : ↑I * Set.univ = ↑I

@[simp]

theorem LeanPool.ArtinWedderburn.TwoSidedIdealProd.mul_two_sided_ideal_eq_span {R : Type u_1} [Ring R] (I J : TwoSidedIdeal R) : I * J = ringSubsetProdTwoSidedIdeal ↑I ↑J

theorem LeanPool.ArtinWedderburn.TwoSidedIdealProd.ideal_get_pair_wise_prod {R : Type u_1} [Ring R] (I J : TwoSidedIdeal R) : ↑(I * J) = ↑(AddSubgroup.closure {x : R | ∃ i ∈ I, ∃ j ∈ J, i * j = x})

theorem LeanPool.ArtinWedderburn.TwoSidedIdealProd.ideal_eq_set_eq {R : Type u_1} [Ring R] (I J : TwoSidedIdeal R) (h : ↑I = ↑J) : I = J

theorem LeanPool.ArtinWedderburn.TwoSidedIdealProd.ideal_eq_span {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) : I = TwoSidedIdeal.span ↑I

theorem LeanPool.ArtinWedderburn.TwoSidedIdealProd.prod_le_ideal {R : Type u_1} [Ring R] (I J : TwoSidedIdeal R) : I * J ≤ I

theorem LeanPool.ArtinWedderburn.TwoSidedIdealProd.prod_le_ideal' {R : Type u_1} [Ring R] (I J : TwoSidedIdeal R) : I * J ≤ J

theorem LeanPool.ArtinWedderburn.TwoSidedIdealProd.mul_top {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) : I * ⊤ = I

theorem LeanPool.ArtinWedderburn.TwoSidedIdealProd.top_mul {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) : ⊤ * I = I

theorem LeanPool.ArtinWedderburn.TwoSidedIdealProd.ideal_prod_subgroup_pair_products {R : Type u_1} [Ring R] (I J : TwoSidedIdeal R) : ↑(I * J) = ↑(AddSubgroup.closure (↑I * ↑J))

theorem LeanPool.ArtinWedderburn.TwoSidedIdealProd.subgroup_product_eq {R : Type u_1} [Ring R] (A B C : AddSubgroup R) : AddSubgroup.closure (↑(AddSubgroup.closure (↑A * ↑B)) * ↑C) = AddSubgroup.closure (↑A * ↑B * ↑C)

theorem LeanPool.ArtinWedderburn.TwoSidedIdealProd.product_subgroup_eq {R : Type u_1} [Ring R] (A B C : AddSubgroup R) : AddSubgroup.closure (↑A * ↑(AddSubgroup.closure (↑B * ↑C))) = AddSubgroup.closure (↑A * ↑B * ↑C)

def LeanPool.ArtinWedderburn.TwoSidedIdealProd.twoSidedIdealToSubgroup {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) : AddSubgroup R

Forget the multiplicative structure of a two-sided ideal, viewing it as an additive subgroup.

Equations

• LeanPool.ArtinWedderburn.TwoSidedIdealProd.twoSidedIdealToSubgroup I = { carrier := ↑I, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

theorem LeanPool.ArtinWedderburn.TwoSidedIdealProd.subgroup_of_ideal_carrier_eq_carrier {R : Type u_1} [Ring R] (I : TwoSidedIdeal R) : ↑(twoSidedIdealToSubgroup I) = ↑I

theorem LeanPool.ArtinWedderburn.TwoSidedIdealProd.ideal_product_subgroup_eq {R : Type u_1} [Ring R] (A B C : TwoSidedIdeal R) : AddSubgroup.closure (↑(AddSubgroup.closure (↑A * ↑B)) * ↑C) = AddSubgroup.closure (↑A * ↑B * ↑C)

theorem LeanPool.ArtinWedderburn.TwoSidedIdealProd.product_ideal_subgroup_eq {R : Type u_1} [Ring R] (A B C : TwoSidedIdeal R) : AddSubgroup.closure (↑A * ↑(AddSubgroup.closure (↑B * ↑C))) = AddSubgroup.closure (↑A * ↑B * ↑C)

theorem LeanPool.ArtinWedderburn.TwoSidedIdealProd.ideal_mul_assoc {R : Type u_1} [Ring R] (I J K : TwoSidedIdeal R) : I * J * K = I * (J * K)

@[implicit_reducible]

instance LeanPool.ArtinWedderburn.TwoSidedIdealProd.instSemigroupTwoSidedIdealLeanPool {R : Type u_1} [Ring R] : Semigroup (TwoSidedIdeal R)

Equations

• LeanPool.ArtinWedderburn.TwoSidedIdealProd.instSemigroupTwoSidedIdealLeanPool = { toMul := LeanPool.ArtinWedderburn.TwoSidedIdealProd.instMulTwoSidedIdealLeanPool, mul_assoc := ⋯ }

@[implicit_reducible]

instance LeanPool.ArtinWedderburn.TwoSidedIdealProd.MulTwoSidedisMonoid {R : Type u_1} [Ring R] : Monoid (TwoSidedIdeal R)

Equations

• One or more equations did not get rendered due to their size.