Theorems · Definition · commutative algebra

RingHom.pullback

{R : Type u_1} →
  {S : Type u_2} →
    {T : Type u_3} →
      [inst : Ring R] → [inst_1 : Ring S] → [inst_2 : Semiring T] → (R →+* T) → (S →+* T) → Subring (R × S)

The subring of pairs (r, s) : R × S such that f r = g s, i.e., the pullback of f : R →+* T and g : S →+* T as a subring of R × S.

Defined in

Mathlib.RingTheory.LocalRing.Pullback

Cited by

6 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext, Quot.sound

Assumes

RingRingSemiring