Subrings #
Let R
be a ring. This file defines the "bundled" subring type Subring R
, a type
whose terms correspond to subrings of R
. This is the preferred way to talk
about subrings in mathlib. Unbundled subrings (s : Set R
and IsSubring s
)
are not in this file, and they will ultimately be deprecated.
We prove that subrings are a complete lattice, and that you can map
(pushforward) and
comap
(pull back) them along ring homomorphisms.
We define the closure
construction from Set R
to Subring R
, sending a subset of R
to the subring it generates, and prove that it is a Galois insertion.
Main definitions #
Notation used here:
(R : Type u) [Ring R] (S : Type u) [Ring S] (f g : R →+* S)
(A : Subring R) (B : Subring S) (s : Set R)
Subring R
: the type of subrings of a ringR
.instance : CompleteLattice (Subring R)
: the complete lattice structure on the subrings.Subring.center
: the center of a ringR
.Subring.closure
: subring closure of a set, i.e., the smallest subring that includes the set.Subring.gi
:closure : Set M → Subring M
and coercion(↑) : Subring M → et M
form aGaloisInsertion
.comap f B : Subring A
: the preimage of a subringB
along the ring homomorphismf
map f A : Subring B
: the image of a subringA
along the ring homomorphismf
.eqLocus f g : Subring R
: given ring homomorphismsf g : R →+* S
, the subring ofR
wheref x = g x
Implementation notes #
A subring is implemented as a subsemiring which is also an additive subgroup. The initial PR was as a submonoid which is also an additive subgroup.
Lattice inclusion (e.g. ≤
and ⊓
) is used rather than set notation (⊆
and ∩
), although
∈
is defined as membership of a subring's underlying set.
Tags #
subring, subrings
SubringClass S R
states that S
is a type of subsets s ⊆ R
that
are both a multiplicative submonoid and an additive subgroup.
Instances
Equations
- ⋯ = ⋯
Alias of intCast_mem
.
Equations
- SubringClass.toHasIntCast s = { intCast := fun (n : ℤ) => ⟨↑n, ⋯⟩ }
A subring of a ring inherits a ring structure
Equations
- SubringClass.toRing s = Function.Injective.ring Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
A subring of a CommRing
is a CommRing
.
Equations
- SubringClass.toCommRing s = Function.Injective.commRing Subtype.val ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
A subring of a domain is a domain.
Equations
- ⋯ = ⋯
The natural ring hom from a subring of ring R
to R
.
Equations
- SubringClass.subtype s = { toFun := Subtype.val, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
Instances For
Subring R
is the type of subrings of R
. A subring of R
is a subset s
that is a
multiplicative submonoid and an additive subgroup. Note in particular that it shares the
same 0 and 1 as R.
Instances For
Reinterpret a Subring
as an AddSubgroup
.
Equations
- self.toAddSubgroup = { carrier := self.carrier, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
Instances For
Equations
- ⋯ = ⋯
Copy of a subring with a new carrier
equal to the old one. Useful to fix definitional
equalities.
Equations
- S.copy s hs = { carrier := s, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
Instances For
Construct a Subring R
from a set s
, a submonoid sm
, and an additive
subgroup sa
such that x ∈ s ↔ x ∈ sm ↔ x ∈ sa
.
Equations
- Subring.mk' s sm sa hm ha = { toSubmonoid := sm.copy s ⋯, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
Instances For
A Subsemiring
containing -1 is a Subring
.
Equations
- s.toSubring hneg = { toSubsemiring := s, neg_mem' := ⋯ }
Instances For
A subring of a ring inherits a ring structure
Equations
- s.toRing = SubringClass.toRing s
A subring of a CommRing
is a CommRing
.
Equations
- s.toCommRing = SubringClass.toCommRing s
A subring of a non-trivial ring is non-trivial.
Equations
- ⋯ = ⋯
A subring of a ring with no zero divisors has no zero divisors.
Equations
- ⋯ = ⋯
Partial order #
top #
comap #
The preimage of a subring along a ring homomorphism is a subring.
Equations
- Subring.comap f s = { carrier := ⇑f ⁻¹' s.carrier, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
Instances For
map #
The image of a subring along a ring homomorphism is a subring.
Equations
- Subring.map f s = { carrier := ⇑f '' s.carrier, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
Instances For
A subring is isomorphic to its image under an injective function
Equations
- s.equivMapOfInjective f hf = { toEquiv := Equiv.Set.image (⇑f) (↑s) hf, map_mul' := ⋯, map_add' := ⋯ }
Instances For
range #
The range of a ring homomorphism is a fintype, if the domain is a fintype.
Note: this instance can form a diamond with Subtype.fintype
in the
presence of Fintype S
.
Equations
- f.fintypeRange = Set.fintypeRange ⇑f
bot #
Equations
- Subring.instBot = { bot := (Int.castRingHom R).range }
inf #
Equations
- Subring.instInfSet = { sInf := fun (s : Set (Subring R)) => Subring.mk' (⋂ t ∈ s, ↑t) (⨅ t ∈ s, t.toSubmonoid) (⨅ t ∈ s, t.toAddSubgroup) ⋯ ⋯ }
Subrings of a ring form a complete lattice.
Equations
- Subring.instCompleteLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯
Center of a ring #
The center of a ring R
is the set of elements that commute with everything in R
Equations
- Subring.center R = { carrier := Set.center R, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
Instances For
Equations
- Subring.decidableMemCenter x = decidable_of_iff' (∀ (g : R), g * x = x * g) ⋯
The center is commutative.
Equations
- Subring.instCommRingSubtypeMemCenter = CommRing.mk ⋯
The centralizer of a set inside a ring as a Subring
.
Equations
- Subring.centralizer s = { toSubsemiring := Subsemiring.centralizer s, neg_mem' := ⋯ }
Instances For
subring closure of a subset #
The subring generated by a set includes the set.
An induction principle for closure membership. If p
holds for 0
, 1
, and all elements
of s
, and is preserved under addition, negation, and multiplication, then p
holds for all
elements of the closure of s
.
An induction principle for closure membership, for predicates with two arguments.
closure
forms a Galois insertion with the coercion to set.
Equations
- Subring.gi R = { choice := fun (s : Set R) (x : ↑(Subring.closure s) ≤ s) => Subring.closure s, gc := ⋯, le_l_u := ⋯, choice_eq := ⋯ }
Instances For
Closure of a subring S
equals S
.
The underlying set of a non-empty directed sSup of subrings is just a union of the subrings. Note that this fails without the directedness assumption (the union of two subrings is typically not a subring)
Restriction of a ring homomorphism to its range interpreted as a subsemiring.
This is the bundled version of Set.rangeFactorization
.
Equations
- f.rangeRestrict = f.codRestrict f.range ⋯
Instances For
The range of a surjective ring homomorphism is the whole of the codomain.
The image under a ring homomorphism of the subring generated by a set equals the subring generated by the image of the set.
The ring homomorphism associated to an inclusion of subrings.
Equations
- Subring.inclusion h = S.subtype.codRestrict T ⋯
Instances For
Makes the identity isomorphism from a proof two subrings of a multiplicative monoid are equal.
Equations
- RingEquiv.subringCongr h = { toEquiv := Equiv.setCongr ⋯, map_mul' := ⋯, map_add' := ⋯ }
Instances For
Restrict a ring homomorphism with a left inverse to a ring isomorphism to its
RingHom.range
.
Equations
- RingEquiv.ofLeftInverse h = { toFun := fun (x : R) => f.rangeRestrict x, invFun := fun (x : ↥f.range) => (g ∘ ⇑f.range.subtype) x, left_inv := h, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
Instances For
Given an equivalence e : R ≃+* S
of rings and a subring s
of R
,
subringMap e s
is the induced equivalence between s
and s.map e
Equations
- e.subringMap = e.subsemiringMap s.toSubsemiring
Instances For
Actions by Subring
s #
These are just copies of the definitions about Subsemiring
starting from
Subsemiring.MulAction
.
When R
is commutative, Algebra.ofSubring
provides a stronger result than those found in
this file, which uses the same scalar action.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Note that this provides IsScalarTower S R R
which is needed by smul_mul_assoc
.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
The action by a subring is the action by the underlying ring.
Equations
- S.instDistribMulActionSubtypeMem = inferInstanceAs (DistribMulAction (↥S.toSubsemiring) α)
The action by a subring is the action by the underlying ring.
Equations
- S.instMulDistribMulActionSubtypeMem = inferInstanceAs (MulDistribMulAction (↥S.toSubsemiring) α)
The action by a subring is the action by the underlying ring.
Equations
- S.instSMulWithZeroSubtypeMem = inferInstanceAs (SMulWithZero (↥S.toSubsemiring) α)
The action by a subring is the action by the underlying ring.
Equations
- S.instMulActionWithZeroSubtypeMem = S.mulActionWithZero
The action by a subring is the action by the underlying ring.
Equations
- S.instModuleSubtypeMem = S.module
The action by a subsemiring is the action by the underlying ring.
Equations
- S.instMulSemiringActionSubtypeMem = inferInstanceAs (MulSemiringAction (↥S.toSubmonoid) α)
The center of a semiring acts commutatively on that semiring.
Equations
- ⋯ = ⋯
The center of a semiring acts commutatively on that semiring.
Equations
- ⋯ = ⋯