R be a non-unital ring. This file defines the "bundled" non-unital subring type
NonUnitalSubring R, a type whose terms correspond to non-unital subrings of
This is the preferred way to talk about non-unital subrings in mathlib.
Main definitions #
Notation used here:
NonUnitalSubring R: the type of non-unital subrings of a ring
instance : CompleteLattice (NonUnitalSubring R): the complete lattice structure on the non-unital subrings.
NonUnitalSubring.center: the center of a non-unital ring
NonUnitalSubring.closure: non-unital subring closure of a set, i.e., the smallest non-unital subring that includes the set.
eq_locus f g : NonUnitalSubring R: given non-unital ring homomorphisms
f g : R →ₙ+* S, the non-unital subring of
f x = g x
Implementation notes #
A non-unital subring is implemented as a
NonUnitalSubsemiring which is also an
Lattice inclusion (e.g.
⊓) is used rather than set notation (
∈ is defined as membership of a non-unital subring's underlying set.
NonUnitalSubring R is the type of non-unital subrings of
R. A non-unital subring of
is a subset
s that is a multiplicative subsemigroup and an additive subgroup. Note in particular
that it shares the same 0 as R.
NonUnitalSubring R from a set
s, a subsemigroup
sm, and an additive
sa such that
x ∈ s ↔ x ∈ sm ↔ x ∈ sa.
Partial order #
NonUnitalSubring is isomorphic to its image under an injective function
Center of a ring #
An induction principle for closure membership. If
p holds for
1, and all elements
s, and is preserved under addition, negation, and multiplication, then
p holds for all
elements of the closure of
The difference with
NonUnitalSubring.closure_induction is that this acts on the
An induction principle for closure membership, for predicates with two arguments.
NonUnitalSubrings is isomorphic to their product as rings.
The underlying set of a non-empty directed Sup of
NonUnitalSubrings is just a union of the
NonUnitalSubrings. Note that this fails without the directedness assumption (the union of two
NonUnitalSubrings is typically not a
Restriction of a ring homomorphism to its range interpreted as a
This is the bundled version of
If two ring homomorphisms are equal on a set, then they are equal on its