domain_isLocalRing — Mathlib

English

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

Русский

Если g (функциональный) R →+* S локален и S локально, то R локально.

LaTeX

$$$\text{IsLocalHom}(f) \Rightarrow (\text{IsLocalRing } S) \Rightarrow \text{IsLocalRing } R$$$

Lean4

/-- If `f : R →+* S` is a local ring hom, then `R` is a local ring if `S` is. -/
theorem domain_isLocalRing {R S : Type*} [Semiring R] [CommSemiring S] [IsLocalRing S] (f : R →+* S) [IsLocalHom f] :
    IsLocalRing R := by
  haveI : Nontrivial R := f.domain_nontrivial
  apply IsLocalRing.of_nonunits_add
  intro a b
  simp_rw [← map_mem_nonunits_iff f, f.map_add]
  exact IsLocalRing.nonunits_add

Похожие утверждения