Documentation

Mathlib.Algebra.Ring.Subsemiring.Support

Supports of subsemirings #

Let R be a ring, and let S be a subsemiring of R. If S generates R as a subring, then the support of S forms an ideal.

Main definitions #

source
theorem Subsemiring.mem_support {R : Type u_1} [Ring R] {S : Subsemiring R} {x : R} :
x ∈ S.toAddSubmonoid.support ↔ x ∈ S ∧ -x ∈ S
source
theorem Subsemiring.isPointed_def {R : Type u_1} [Ring R] {S : Subsemiring R} :
S.toAddSubmonoid.IsPointed ↔ ∀ {x : R}, x ∈ S → -x ∈ S → x = 0
source
theorem Subsemiring.isSpanning_def {R : Type u_1} [Ring R] {S : Subsemiring R} :
S.toAddSubmonoid.IsSpanning ↔ ∀ (a : R), a ∈ S ∨ -a ∈ S
source
def Subsemiring.supportIdeal {R : Type u_1} [Ring R] {S : Subsemiring R} (hS : S.toAddSubmonoid.IsSpanning) :
Ideal R

The support S ∩ -S of a subsemiring S, as an ideal. We restrict to subsemirings that span the whole ring as subrings because the support of a subsemiring does not form an ideal in general.

Equations
Instances For
    source
    @[simp]
    theorem Subsemiring.coe_supportIdeal {R : Type u_1} [Ring R] {S : Subsemiring R} (hS : S.toAddSubmonoid.IsSpanning) :
    ↑(supportIdeal hS) = ↑S ∩ -↑S
    source
    @[simp]
    theorem Subsemiring.mem_supportIdeal {R : Type u_1} [Ring R] {S : Subsemiring R} (hS : S.toAddSubmonoid.IsSpanning) {x : R} :
    x ∈ supportIdeal hS ↔ x ∈ S.toAddSubmonoid.support
    source
    @[simp]
    theorem Subsemiring.supportIdeal_toAddSubgroup {R : Type u_1} [Ring R] {S : Subsemiring R} (hS : S.toAddSubmonoid.IsSpanning) :
    Submodule.toAddSubgroup (supportIdeal hS) = S.toAddSubmonoid.support
    source
    theorem AddSubmonoid.IsSpanning.mem_of_isSquare {R : Type u_1} [CommRing R] (S : Subsemiring R) (hS : S.toAddSubmonoid.IsSpanning) {x : R} :
    IsSquare x → x ∈ S
    source
    theorem AddSubmonoid.IsSpanning.sumSq_le {R : Type u_1} [CommRing R] (S : Subsemiring R) (hS : S.toAddSubmonoid.IsSpanning) :
    Subsemiring.sumSq R ≤ S
    source
    theorem AddSubmonoid.IsSpanning.mem_of_isSumSq {R : Type u_1} [CommRing R] (S : Subsemiring R) (hS : S.toAddSubmonoid.IsSpanning) {x : R} (hx : IsSumSq x) :
    x ∈ S