Local rings #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Define local rings as commutative rings having a unique maximal ideal.
Main definitions #
local_ring: A predicate on commutative semirings, stating that for any pair of elements that adds up to1, one of them is a unit. This is shown to be equivalent to the condition that there exists a unique maximal ideal.local_ring.maximal_ideal: The unique maximal ideal for a local rings. Its carrier set is the set of non units.is_local_ring_hom: A predicate on semiring homomorphisms, requiring that it maps nonunits to nonunits. For local rings, this means that the image of the unique maximal ideal is again contained in the unique maximal ideal.local_ring.residue_field: The quotient of a local ring by its maximal ideal.
@[class]
- to_nontrivial : nontrivial R
- is_unit_or_is_unit_of_add_one : ∀ {a b : R}, a + b = 1 → is_unit a ∨ is_unit b
A semiring is local if it is nontrivial and a or b is a unit whenever a + b = 1.
Note that local_ring is a predicate.
Instances of this typeclass
theorem
local_ring.of_is_unit_or_is_unit_of_is_unit_add
{R : Type u}
[comm_semiring R]
[nontrivial R]
(h : ∀ (a b : R), is_unit (a + b) → is_unit a ∨ is_unit b) :
theorem
local_ring.of_nonunits_add
{R : Type u}
[comm_semiring R]
[nontrivial R]
(h : ∀ (a b : R), a ∈ nonunits R → b ∈ nonunits R → a + b ∈ nonunits R) :
A semiring is local if it is nontrivial and the set of nonunits is closed under the addition.
theorem
local_ring.of_unique_max_ideal
{R : Type u}
[comm_semiring R]
(h : ∃! (I : ideal R), I.is_maximal) :
A semiring is local if it has a unique maximal ideal.
theorem
local_ring.of_unique_nonzero_prime
{R : Type u}
[comm_semiring R]
(h : ∃! (P : ideal R), P ≠ ⊥ ∧ P.is_prime) :
theorem
local_ring.is_unit_or_is_unit_of_is_unit_add
{R : Type u}
[comm_semiring R]
[local_ring R]
{a b : R}
(h : is_unit (a + b)) :
theorem
local_ring.nonunits_add
{R : Type u}
[comm_semiring R]
[local_ring R]
{a b : R}
(ha : a ∈ nonunits R)
(hb : b ∈ nonunits R) :
The ideal of elements that are not units.
Equations
- local_ring.maximal_ideal R = {carrier := nonunits R (monoid_with_zero.to_monoid R), add_mem' := _, zero_mem' := _, smul_mem' := _}
Instances for local_ring.maximal_ideal
@[protected, instance]
theorem
local_ring.maximal_ideal_unique
(R : Type u)
[comm_semiring R]
[local_ring R] :
∃! (I : ideal R), I.is_maximal
theorem
local_ring.eq_maximal_ideal
{R : Type u}
[comm_semiring R]
[local_ring R]
{I : ideal R}
(hI : I.is_maximal) :
theorem
local_ring.le_maximal_ideal
{R : Type u}
[comm_semiring R]
[local_ring R]
{J : ideal R}
(hJ : J ≠ ⊤) :
@[simp]
theorem
local_ring.mem_maximal_ideal
{R : Type u}
[comm_semiring R]
[local_ring R]
(x : R) :
x ∈ local_ring.maximal_ideal R ↔ x ∈ nonunits R
theorem
local_ring.of_is_unit_or_is_unit_one_sub_self
{R : Type u}
[comm_ring R]
[nontrivial R]
(h : ∀ (a : R), is_unit a ∨ is_unit (1 - a)) :
theorem
local_ring.is_unit_or_is_unit_one_sub_self
{R : Type u}
[comm_ring R]
[local_ring R]
(a : R) :
theorem
local_ring.is_unit_of_mem_nonunits_one_sub_self
{R : Type u}
[comm_ring R]
[local_ring R]
(a : R)
(h : 1 - a ∈ nonunits R) :
is_unit a
theorem
local_ring.is_unit_one_sub_self_of_mem_nonunits
{R : Type u}
[comm_ring R]
[local_ring R]
(a : R)
(h : a ∈ nonunits R) :
theorem
local_ring.of_surjective'
{R : Type u}
{S : Type v}
[comm_ring R]
[local_ring R]
[comm_ring S]
[nontrivial S]
(f : R →+* S)
(hf : function.surjective ⇑f) :
theorem
local_ring.jacobson_eq_maximal_ideal
{R : Type u}
[comm_ring R]
[local_ring R]
(I : ideal R)
(h : I ≠ ⊤) :
@[class]
structure
is_local_ring_hom
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(f : R →+* S) :
Prop
A local ring homomorphism is a homomorphism f between local rings such that a in the domain
is a unit if f a is a unit for any a. See local_ring.local_hom_tfae for other equivalent
definitions.
Instances of this typeclass
@[protected, instance]
@[protected, instance]
def
is_local_ring_hom_comp
{R : Type u}
{S : Type v}
{T : Type w}
[semiring R]
[semiring S]
[semiring T]
(g : S →+* T)
(f : R →+* S)
[is_local_ring_hom g]
[is_local_ring_hom f] :
is_local_ring_hom (g.comp f)
theorem
of_irreducible_map
{R : Type u}
{S : Type v}
[semiring R]
[semiring S]
(f : R →+* S)
[h : is_local_ring_hom f]
{x : R}
(hfx : irreducible (⇑f x)) :
theorem
ring_hom.domain_local_ring
{R : Type u_1}
{S : Type u_2}
[comm_semiring R]
[comm_semiring S]
[H : local_ring S]
(f : R →+* S)
[is_local_ring_hom f] :
If f : R →+* S is a local ring hom, then R is a local ring if S is.
theorem
map_nonunit
{R : Type u}
{S : Type v}
[comm_semiring R]
[local_ring R]
[comm_semiring S]
[local_ring S]
(f : R →+* S)
[is_local_ring_hom f]
(a : R)
(h : a ∈ local_ring.maximal_ideal R) :
⇑f a ∈ local_ring.maximal_ideal S
The image of the maximal ideal of the source is contained within the maximal ideal of the target.
theorem
local_ring.local_hom_tfae
{R : Type u}
{S : Type v}
[comm_semiring R]
[local_ring R]
[comm_semiring S]
[local_ring S]
(f : R →+* S) :
[is_local_ring_hom f, ⇑f '' (local_ring.maximal_ideal R).carrier ⊆ ↑(local_ring.maximal_ideal S), ideal.map f (local_ring.maximal_ideal R) ≤ local_ring.maximal_ideal S, local_ring.maximal_ideal R ≤ ideal.comap f (local_ring.maximal_ideal S), ideal.comap f (local_ring.maximal_ideal S) = local_ring.maximal_ideal R].tfae
A ring homomorphism between local rings is a local ring hom iff it reflects units, i.e. any preimage of a unit is still a unit. https://stacks.math.columbia.edu/tag/07BJ
theorem
local_ring.of_surjective
{R : Type u}
{S : Type v}
[comm_semiring R]
[local_ring R]
[comm_semiring S]
[nontrivial S]
(f : R →+* S)
[is_local_ring_hom f]
(hf : function.surjective ⇑f) :
theorem
local_ring.surjective_units_map_of_local_ring_hom
{R : Type u}
{S : Type v}
[comm_ring R]
[comm_ring S]
(f : R →+* S)
(hf : function.surjective ⇑f)
(h : is_local_ring_hom f) :
If f : R →+* S is a surjective local ring hom, then the induced units map is surjective.
The residue field of a local ring is the quotient of the ring by its maximal ideal.
Equations
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
Equations
The quotient map from a local ring to its residue field.
Equations
Instances for local_ring.residue
@[protected, instance]
Equations
@[protected, instance]
def
local_ring.residue_field.lift
{R : Type u_1}
{S : Type u_2}
[comm_ring R]
[local_ring R]
[field S]
(f : R →+* S)
[is_local_ring_hom f] :
A local ring homomorphism into a field can be descended onto the residue field.
Equations
theorem
local_ring.residue_field.lift_comp_residue
{R : Type u_1}
{S : Type u_2}
[comm_ring R]
[local_ring R]
[field S]
(f : R →+* S)
[is_local_ring_hom f] :
(local_ring.residue_field.lift f).comp (local_ring.residue R) = f
@[simp]
theorem
local_ring.residue_field.lift_residue_apply
{R : Type u_1}
{S : Type u_2}
[comm_ring R]
[local_ring R]
[field S]
(f : R →+* S)
[is_local_ring_hom f]
(x : R) :
⇑(local_ring.residue_field.lift f) (⇑(local_ring.residue R) x) = ⇑f x
def
local_ring.residue_field.map
{R : Type u}
{S : Type v}
[comm_ring R]
[local_ring R]
[comm_ring S]
[local_ring S]
(f : R →+* S)
[is_local_ring_hom f] :
The map on residue fields induced by a local homomorphism between local rings
Equations
@[simp]
Applying residue_field.map to the identity ring homomorphism gives the identity
ring homomorphism.
theorem
local_ring.residue_field.map_comp
{R : Type u}
{S : Type v}
{T : Type w}
[comm_ring R]
[local_ring R]
[comm_ring S]
[local_ring S]
[comm_ring T]
[local_ring T]
(f : T →+* R)
(g : R →+* S)
[is_local_ring_hom f]
[is_local_ring_hom g] :
The composite of two residue_field.maps is the residue_field.map of the composite.
theorem
local_ring.residue_field.map_comp_residue
{R : Type u}
{S : Type v}
[comm_ring R]
[local_ring R]
[comm_ring S]
[local_ring S]
(f : R →+* S)
[is_local_ring_hom f] :
(local_ring.residue_field.map f).comp (local_ring.residue R) = (local_ring.residue S).comp f
theorem
local_ring.residue_field.map_residue
{R : Type u}
{S : Type v}
[comm_ring R]
[local_ring R]
[comm_ring S]
[local_ring S]
(f : R →+* S)
[is_local_ring_hom f]
(r : R) :
⇑(local_ring.residue_field.map f) (⇑(local_ring.residue R) r) = ⇑(local_ring.residue S) (⇑f r)
theorem
local_ring.residue_field.map_id_apply
{R : Type u}
[comm_ring R]
[local_ring R]
(x : local_ring.residue_field R) :
⇑(local_ring.residue_field.map (ring_hom.id R)) x = x
@[simp]
theorem
local_ring.residue_field.map_map
{R : Type u}
{S : Type v}
{T : Type w}
[comm_ring R]
[local_ring R]
[comm_ring S]
[local_ring S]
[comm_ring T]
[local_ring T]
(f : R →+* S)
(g : S →+* T)
(x : local_ring.residue_field R)
[is_local_ring_hom f]
[is_local_ring_hom g] :
⇑(local_ring.residue_field.map g) (⇑(local_ring.residue_field.map f) x) = ⇑(local_ring.residue_field.map (g.comp f)) x
def
local_ring.residue_field.map_equiv
{R : Type u}
{S : Type v}
[comm_ring R]
[local_ring R]
[comm_ring S]
[local_ring S]
(f : R ≃+* S) :
A ring isomorphism defines an isomorphism of residue fields.
@[simp]
theorem
local_ring.residue_field.map_equiv_apply
{R : Type u}
{S : Type v}
[comm_ring R]
[local_ring R]
[comm_ring S]
[local_ring S]
(f : R ≃+* S)
(ᾰ : local_ring.residue_field R) :
@[simp]
theorem
local_ring.residue_field.map_equiv.symm
{R : Type u}
{S : Type v}
[comm_ring R]
[local_ring R]
[comm_ring S]
[local_ring S]
(f : R ≃+* S) :
@[simp]
theorem
local_ring.residue_field.map_equiv_trans
{R : Type u}
{S : Type v}
{T : Type w}
[comm_ring R]
[local_ring R]
[comm_ring S]
[local_ring S]
[comm_ring T]
[local_ring T]
(e₁ : R ≃+* S)
(e₂ : S ≃+* T) :
@[simp]
The group homomorphism from ring_aut R to ring_aut k where k
is the residue field of R.
Equations
- local_ring.residue_field.map_aut = {to_fun := local_ring.residue_field.map_equiv _inst_2, map_one' := _, map_mul' := _}
@[simp]
theorem
local_ring.residue_field.map_aut_apply
{R : Type u}
[comm_ring R]
[local_ring R]
(f : R ≃+* R) :
@[protected, instance]
def
local_ring.residue_field.mul_semiring_action
{R : Type u}
[comm_ring R]
[local_ring R]
(G : Type u_1)
[group G]
[mul_semiring_action G R] :
If G acts on R as a mul_semiring_action, then it also acts on residue_field R.
@[simp]
theorem
local_ring.residue_field.residue_smul
{R : Type u}
[comm_ring R]
[local_ring R]
(G : Type u_1)
[group G]
[mul_semiring_action G R]
(g : G)
(r : R) :
⇑(local_ring.residue R) (g • r) = g • ⇑(local_ring.residue R) r
theorem
local_ring.ker_eq_maximal_ideal
{R : Type u}
{K : Type u'}
[comm_ring R]
[local_ring R]
[field K]
(φ : R →+* K)
(hφ : function.surjective ⇑φ) :
@[protected, reducible]
theorem
ring_equiv.local_ring
{A : Type u_1}
{B : Type u_2}
[comm_semiring A]
[local_ring A]
[comm_semiring B]
(e : A ≃+* B) :