StableUnderCompositionWithLocalizationAwayTarget

English

A property P of ring homs stable under localization implies the same property for the localization away maps from the source subalgebra to the target when considering subalgebras A,B with adjoined sets.

Русский

Свойство P локализации сохраняется для отображений локализации вдали, если рассматривать подалгебры A,B и их объединение.

LaTeX

$$$P(\\text{away map}) \\Rightarrow P(\\text{localized map})$$$

Lean4

/-- A property `P` of ring homs satisfies `RingHom.StableUnderCompositionWithLocalizationAway`
if whenever `P` holds for `f` it also holds for the composition with
localization maps on the target. -/
def StableUnderCompositionWithLocalizationAwayTarget : Prop :=
  ∀ ⦃R S : Type u⦄ (T : Type u) [CommRing R] [CommRing S] [CommRing T] [Algebra S T] (s : S) [IsLocalization.Away s T]
    (f : R →+* S), P f → P ((algebraMap S T).comp f)

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