IsStableUnderBaseChange — Mathlib

English

The categorical notion of stability under base-change for ring-homomorphism properties.

Русский

Категориальное понятие устойчивости к базовому изменению для свойств гомоморфизмов колец.

LaTeX

$$$\text{IsStableUnderBaseChange}(P) := \forall (R,S,R',S'), [\text{conditions}] : P(\alpha) \Rightarrow P(\beta).$$$

Lean4

/-- A morphism property `P` is `IsStableUnderBaseChange` if `P(S →+* A)` implies
`P(B →+* A ⊗[S] B)`. -/
def IsStableUnderBaseChange : Prop :=
  ∀ (R S R' S') [CommRing R] [CommRing S] [CommRing R'] [CommRing S'],
    ∀ [Algebra R S] [Algebra R R'] [Algebra R S'] [Algebra S S'] [Algebra R' S'],
      ∀ [IsScalarTower R S S'] [IsScalarTower R R' S'],
        ∀ [Algebra.IsPushout R S R' S'], P (algebraMap R S) → P (algebraMap R' S')

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