LeanPool.BrauerGroupNew.TwoSidedIdeal

Imported Lean Pool material for LeanPool.BrauerGroupNew.TwoSidedIdeal.

def TwoSidedIdeal.span' {R : Type u_3} [Ring R] (s : Set R) : TwoSidedIdeal R

The two-sided ideal generated by finite sums xL * y * xR with y ∈ s.

Equations

• TwoSidedIdeal.span' s = TwoSidedIdeal.mk' {x : R | ∃ (ι : Type) (fin : Fintype ι) (xL : ι → R) (xR : ι → R) (y : ι → ↑s), x = ∑ i : ι, xL i * ↑(y i) * xR i} ⋯ ⋯ ⋯ ⋯ ⋯

theorem TwoSidedIdeal.mem_span'_iff_exists_fin {R : Type u_3} [Ring R] (s : Set R) (x : R) : x ∈ span' s ↔ ∃ (ι : Type) (x_1 : Fintype ι) (xL : ι → R) (xR : ι → R) (y : ι → ↑s), x = ∑ i : ι, xL i * ↑(y i) * xR i

theorem TwoSidedIdeal.mem_span_iff_exists_fin {R : Type u_3} [Ring R] (s : Set R) (x : R) : x ∈ span s ↔ ∃ (ι : Type) (x_1 : Fintype ι) (xL : ι → R) (xR : ι → R) (y : ι → ↑s), x = ∑ i : ι, xL i * ↑(y i) * xR i

theorem TwoSidedIdeal.mem_span_ideal_iff_exists_fin {R : Type u_3} [Ring R] (s : Ideal R) (x : R) : x ∈ span ↑s ↔ ∃ (ι : Type) (x_1 : Fintype ι) (xR : ι → R) (y : ι → ↥s), x = ∑ i : ι, ↑(y i) * xR i

theorem TwoSidedIdeal.coe_bot_set {R : Type u_3} [Ring R] : ↑⊥ = {0}

theorem TwoSidedIdeal.coe_top_set {R : Type u_3} [Ring R] : ↑⊤ = Set.univ

instance TwoSidedIdeal.instNontrivial_leanPool (A : Type u) [Ring A] [Nontrivial A] : Nontrivial (TwoSidedIdeal A)

theorem IsSimpleRing.iff_eq_zero_or_injective' (A : Type u) [Ring A] (k : Type u_5) [CommRing k] [Algebra k A] [Nontrivial A] : IsSimpleRing A ↔ ∀ ⦃B : Type u⦄ [inst : Ring B] [inst_1 : Algebra k B] (f : A →ₐ[k] B), TwoSidedIdeal.ker f = ⊤ ∨ Function.Injective ⇑f