surjective_units_map_of_local_ringHom

English

If f is a local ring hom and surjective on the underlying ring, the induced units map is surjective.

Русский

Если f — локальный гомоморфизм и сюръективен на основаниях, отображение единиц монад суръективно.

LaTeX

$$$\text{IsLocalHom}(f) \Rightarrow \text{Function.Surjective}(f) \Rightarrow \text{Surjective}(Units.map(f))$$$

Lean4

/-- If `f : R →+* S` is a surjective local ring hom, then the induced units map is surjective. -/
theorem surjective_units_map_of_local_ringHom [Semiring R] [Semiring S] (f : R →+* S) (hf : Function.Surjective f)
    (h : IsLocalHom f) : Function.Surjective (Units.map <| f.toMonoidHom) :=
  by
  intro a
  obtain ⟨b, hb⟩ := hf (a : S)
  use (isUnit_of_map_unit f b (by rw [hb]; exact Units.isUnit _)).unit
  ext
  exact hb

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