isUnit_piRingHom_algebraMap_comp_piEvalRingHom

English

For a fixed r, the away localization S of R at r has finite presentation as an R-algebra.

Русский

Для фиксированного r away-локализация S R при r имеет конечную презентацию как R-алгебра.

LaTeX

$$IsLocalization.Away.finitePresentation$$

Lean4

/-- Let `M` be a submonoid of a direct product of commutative rings `R i`, and let `M' i` denote
the projection of `M` onto each corresponding factor. Given a ring homomorphism from the direct
product `Π i, R i` to the product of the localizations of each `R i` at `M' i`, every `y : M`
maps to a unit under this homomorphism. -/
theorem isUnit_piRingHom_algebraMap_comp_piEvalRingHom (y : M) :
    IsUnit ((Pi.ringHom fun i ↦ (algebraMap (R i) (S i)).comp (Pi.evalRingHom R i)) y) :=
  Pi.isUnit_iff.mpr fun i ↦ map_units _ (⟨y.1 i, y, y.2, rfl⟩ : M.map (Pi.evalRingHom R i))

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