Local rings homomorphisms #

We prove basic properties of local rings homomorphisms.

source

theorem isLocalHom_id (R : Type u_4) [Semiring R] :

IsLocalHom (RingHom.id R)

source

@[deprecated isLocalHom_id]

theorem isLocalRingHom_id (R : Type u_4) [Semiring R] :

IsLocalHom (RingHom.id R)

Alias of isLocalHom_id.

source

theorem isLocalHom_toRingHom {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] {F : Type u_4} [FunLike F R S] [RingHomClass F R S] (f : F) [IsLocalHom f] :

IsLocalHom ↑f

source

@[deprecated isLocalHom_toRingHom]

theorem isLocalRingHom_toRingHom {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] {F : Type u_4} [FunLike F R S] [RingHomClass F R S] (f : F) [IsLocalHom f] :

IsLocalHom ↑f

Alias of isLocalHom_toRingHom.

source

theorem RingHom.isLocalHom_comp {R : Type u_1} {S : Type u_2} {T : Type u_3} [Semiring R] [Semiring S] [Semiring T] (g : S →+* T) (f : R →+* S) [IsLocalHom g] [IsLocalHom f] :

IsLocalHom (g.comp f)

source

@[deprecated RingHom.isLocalHom_comp]

theorem RingHom.isLocalRingHom_comp {R : Type u_1} {S : Type u_2} {T : Type u_3} [Semiring R] [Semiring S] [Semiring T] (g : S →+* T) (f : R →+* S) [IsLocalHom g] [IsLocalHom f] :

IsLocalHom (g.comp f)

Alias of RingHom.isLocalHom_comp.

source

theorem isLocalHom_of_comp {R : Type u_1} {S : Type u_2} {T : Type u_3} [Semiring R] [Semiring S] [Semiring T] (f : R →+* S) (g : S →+* T) [IsLocalHom (g.comp f)] :

IsLocalHom f

source

@[deprecated isLocalHom_of_comp]

theorem isLocalRingHom_of_comp {R : Type u_1} {S : Type u_2} {T : Type u_3} [Semiring R] [Semiring S] [Semiring T] (f : R →+* S) (g : S →+* T) [IsLocalHom (g.comp f)] :

IsLocalHom f

Alias of isLocalHom_of_comp.

source

theorem RingHom.domain_isLocalRing {R : Type u_4} {S : Type u_5} [CommSemiring R] [CommSemiring S] [IsLocalRing S] (f : R →+* S) [IsLocalHom f] :

IsLocalRing R

If f : R →+* S is a local ring hom, then R is a local ring if S is.

source

@[deprecated RingHom.domain_isLocalRing]

theorem RingHom.domain_localRing {R : Type u_4} {S : Type u_5} [CommSemiring R] [CommSemiring S] [IsLocalRing S] (f : R →+* S) [IsLocalHom f] :

IsLocalRing R

Alias of RingHom.domain_isLocalRing.

If f : R →+* S is a local ring hom, then R is a local ring if S is.

source

theorem map_nonunit {R : Type u_1} {S : Type u_2} [CommSemiring R] [IsLocalRing R] [CommSemiring S] [IsLocalRing S] (f : R →+* S) [IsLocalHom f] (a : R) (h : a ∈ IsLocalRing.maximalIdeal R) :

f a ∈ IsLocalRing.maximalIdeal S

The image of the maximal ideal of the source is contained within the maximal ideal of the target.

source

theorem IsLocalRing.local_hom_TFAE {R : Type u_1} {S : Type u_2} [CommSemiring R] [IsLocalRing R] [CommSemiring S] [IsLocalRing S] (f : R →+* S) :

[IsLocalHom f, ⇑f '' ↑(IsLocalRing.maximalIdeal R).toAddSubmonoid ⊆ ↑(IsLocalRing.maximalIdeal S), Ideal.map f (IsLocalRing.maximalIdeal R) ≤ IsLocalRing.maximalIdeal S, IsLocalRing.maximalIdeal R ≤ Ideal.comap f (IsLocalRing.maximalIdeal S), Ideal.comap f (IsLocalRing.maximalIdeal S) = IsLocalRing.maximalIdeal 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

source

theorem IsLocalRing.of_surjective {R : Type u_1} {S : Type u_2} [CommSemiring R] [IsLocalRing R] [CommSemiring S] [Nontrivial S] (f : R →+* S) [IsLocalHom f] (hf : Function.Surjective ⇑f) :

IsLocalRing S

source

theorem IsLocalHom.of_surjective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Nontrivial S] [IsLocalRing R] (f : R →+* S) (hf : Function.Surjective ⇑f) :

IsLocalHom f

source

theorem Function.Surjective.isLocalHom {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Nontrivial S] [IsLocalRing R] (f : R →+* S) (hf : Function.Surjective ⇑f) :

IsLocalHom f

Alias of IsLocalHom.of_surjective.

source

theorem IsLocalRing.surjective_units_map_of_local_ringHom {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Surjective ⇑f) (h : IsLocalHom f) :

Function.Surjective ⇑(Units.map ↑f)

If f : R →+* S is a surjective local ring hom, then the induced units map is surjective.

source

@[instance 100]

instance IsLocalRing.instIsLocalHomRingHomOfNontrivial {K : Type u_4} {R : Type u_5} [DivisionRing K] [CommRing R] [Nontrivial R] (f : K →+* R) :

IsLocalHom f

Every ring hom f : K →+* R from a division ring K to a nontrivial ring R is a local ring hom.

Equations

⋯ = ⋯

source

@[deprecated IsLocalRing.local_hom_TFAE]

theorem LocalRing.local_hom_TFAE {R : Type u_1} {S : Type u_2} [CommSemiring R] [IsLocalRing R] [CommSemiring S] [IsLocalRing S] (f : R →+* S) :

Alias of IsLocalRing.local_hom_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

source

@[deprecated IsLocalRing.of_surjective]

theorem LocalRing.of_surjective {R : Type u_1} {S : Type u_2} [CommSemiring R] [IsLocalRing R] [CommSemiring S] [Nontrivial S] (f : R →+* S) [IsLocalHom f] (hf : Function.Surjective ⇑f) :

IsLocalRing S

Alias of IsLocalRing.of_surjective.

source

@[deprecated IsLocalRing.surjective_units_map_of_local_ringHom]

theorem LocalRing.surjective_units_map_of_local_ringHom {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) (hf : Function.Surjective ⇑f) (h : IsLocalHom f) :

Function.Surjective ⇑(Units.map ↑f)

Alias of IsLocalRing.surjective_units_map_of_local_ringHom.

If f : R →+* S is a surjective local ring hom, then the induced units map is surjective.

source

theorem RingEquiv.isLocalRing {A : Type u_4} {B : Type u_5} [CommSemiring A] [IsLocalRing A] [CommSemiring B] (e : A ≃+* B) :

IsLocalRing B

source

@[deprecated RingEquiv.isLocalRing]

theorem RingEquiv.localRing {A : Type u_4} {B : Type u_5} [CommSemiring A] [IsLocalRing A] [CommSemiring B] (e : A ≃+* B) :

IsLocalRing B

Alias of RingEquiv.isLocalRing.

HepLean Documentation

Mathlib.RingTheory.LocalRing.RingHom.Basic

Local rings homomorphisms #