doc-next-gen

Mathlib.RingTheory.Ideal.Nonunits

Module docstring

{"# The set of non-invertible elements of a monoid

Main definitions

  • nonunits is the set of non-invertible elements of a monoid.

Main results

  • exists_max_ideal_of_mem_nonunits: every element of nonunits is contained in a maximal ideal "}
nonunits definition
(α : Type*) [Monoid α] : Set α
Full source 
/-- The set of non-invertible elements of a monoid. -/
def nonunits (α : Type*) [Monoid α] : Set α :=
  { a | ¬IsUnit a }
Set of non-invertible elements in a monoid
Informal description
The set of non-invertible elements in a monoid $\alpha$, defined as $\{a \in \alpha \mid \neg \text{IsUnit } a\}$.
mem_nonunits_iff theorem
[Monoid α] : a ∈ nonunits α ↔ ¬IsUnit a
Full source 
@[simp]
theorem mem_nonunits_iff [Monoid α] : a ∈ nonunits αa ∈ nonunits α ↔ ¬IsUnit a :=
  Iff.rfl
Characterization of Non-Units in a Monoid
Informal description
For any monoid $\alpha$ and any element $a \in \alpha$, $a$ belongs to the set of non-invertible elements of $\alpha$ if and only if $a$ is not a unit in $\alpha$.
mul_mem_nonunits_right theorem
[CommMonoid α] : b ∈ nonunits α → a * b ∈ nonunits α
Full source 
theorem mul_mem_nonunits_right [CommMonoid α] : b ∈ nonunits α → a * b ∈ nonunits α :=
  mt isUnit_of_mul_isUnit_right
Right Multiplication Preserves Non-Units in Commutative Monoid
Informal description
Let $\alpha$ be a commutative monoid. For any elements $a, b \in \alpha$, if $b$ is a non-invertible element (i.e., $b \in \text{nonunits}(\alpha)$), then the product $a \cdot b$ is also non-invertible (i.e., $a \cdot b \in \text{nonunits}(\alpha)$).
mul_mem_nonunits_left theorem
[CommMonoid α] : a ∈ nonunits α → a * b ∈ nonunits α
Full source 
theorem mul_mem_nonunits_left [CommMonoid α] : a ∈ nonunits α → a * b ∈ nonunits α :=
  mt isUnit_of_mul_isUnit_left
Left Multiplication Preserves Non-Units in Commutative Monoid
Informal description
Let $\alpha$ be a commutative monoid. For any elements $a, b \in \alpha$, if $a$ is a non-invertible element (i.e., $a \in \text{nonunits}(\alpha)$), then the product $a \cdot b$ is also non-invertible (i.e., $a \cdot b \in \text{nonunits}(\alpha)$).
zero_mem_nonunits theorem
[MonoidWithZero α] : 0 ∈ nonunits α ↔ (0 : α) ≠ 1
Full source 
theorem zero_mem_nonunits [MonoidWithZero α] : 0 ∈ nonunits α0 ∈ nonunits α ↔ (0 : α) ≠ 1 :=
  not_congr isUnit_zero_iff
Zero is Non-invertible if and only if Not Equal to One
Informal description
For a monoid with zero $\alpha$, the zero element $0$ is in the set of non-invertible elements if and only if $0$ is not equal to the multiplicative identity $1$, i.e., $0 \in \text{nonunits}(\alpha) \leftrightarrow 0 \neq 1$.
one_not_mem_nonunits theorem
[Monoid α] : (1 : α) ∉ nonunits α
Full source 
@[simp 1001] -- increased priority to appease `simpNF`
theorem one_not_mem_nonunits [Monoid α] : (1 : α) ∉ nonunits α :=
  not_not_intro isUnit_one
Identity Element is Invertible in a Monoid
Informal description
For any monoid $\alpha$, the multiplicative identity element $1$ is not in the set of non-invertible elements, i.e., $1 \notin \text{nonunits}(\alpha)$.
map_mem_nonunits_iff theorem
[Monoid α] [Monoid β] [FunLike F α β] [MonoidHomClass F α β] (f : F) [IsLocalHom f] (a) : f a ∈ nonunits β ↔ a ∈ nonunits α
Full source 
@[simp (high)]
theorem map_mem_nonunits_iff [Monoid α] [Monoid β] [FunLike F α β] [MonoidHomClass F α β] (f : F)
    [IsLocalHom f] (a) : f a ∈ nonunits βf a ∈ nonunits β ↔ a ∈ nonunits α :=
  ⟨fun h ha => h <| ha.map f, fun h ha => h <| ha.of_map⟩
Characterization of Non-Invertible Elements under Local Homomorphisms
Informal description
Let $\alpha$ and $\beta$ be monoids, and let $F$ be a type of homomorphisms from $\alpha$ to $\beta$ that preserve the monoid structure. For any local homomorphism $f \in F$ and any element $a \in \alpha$, the image $f(a)$ is a non-invertible element in $\beta$ if and only if $a$ is a non-invertible element in $\alpha$. In other words, $f(a) \in \text{nonunits}(\beta) \leftrightarrow a \in \text{nonunits}(\alpha)$.
coe_subset_nonunits theorem
[Semiring α] {I : Ideal α} (h : I ≠ ⊤) : (I : Set α) ⊆ nonunits α
Full source 
theorem coe_subset_nonunits [Semiring α] {I : Ideal α} (h : I ≠ ⊤) : (I : Set α) ⊆ nonunits α :=
  fun _x hx hu => h <| I.eq_top_of_isUnit_mem hx hu
Proper Ideals Consist of Non-Invertible Elements
Informal description
For any semiring $\alpha$ and any proper ideal $I$ of $\alpha$ (i.e., $I \neq \top$), the set underlying $I$ is contained in the set of non-invertible elements of $\alpha$, i.e., $I \subseteq \text{nonunits}(\alpha)$.
exists_max_ideal_of_mem_nonunits theorem
[CommSemiring α] (h : a ∈ nonunits α) : ∃ I : Ideal α, I.IsMaximal ∧ a ∈ I
Full source 
theorem exists_max_ideal_of_mem_nonunits [CommSemiring α] (h : a ∈ nonunits α) :
    ∃ I : Ideal α, I.IsMaximal ∧ a ∈ I := by
  have : Ideal.spanIdeal.span ({a} : Set α) ≠ ⊤ := by
    intro H
    rw [Ideal.span_singleton_eq_top] at H
    contradiction
  rcases Ideal.exists_le_maximal _ this with ⟨I, Imax, H⟩
  use I, Imax
  apply H
  apply Ideal.subset_span
  exact Set.mem_singleton a
Existence of Maximal Ideal Containing a Non-Unit Element in a Commutative Semiring
Informal description
Let $\alpha$ be a commutative semiring and let $a \in \alpha$ be a non-invertible element (i.e., $a \in \text{nonunits}(\alpha)$). Then there exists a maximal ideal $I$ of $\alpha$ such that $a \in I$.