Theorems · Definition · commutative algebra

RingHom.CodescendsAlong

({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) →
  ({R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop) → Prop

A property of ring homomorphisms Q codescends along Q' if whenever R' →+* R' ⊗[R] S satisfies Q and R →+* R' satisfies Q', then R →+* S satisfies Q.

Defined in

Mathlib.RingTheory.RingHomProperties

Cited by

17 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms