Theorems · Definition · commutative algebra

RingHom.liftOfRightInverse

{A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      [inst : Ring A] →
        [inst_1 : Ring B] →
          [inst_2 : Ring C] →
            (f : A →+* B) →
              (f_inv : B → A) → Function.RightInverse f_inv ⇑f → { g // RingHom.ker f ≤ RingHom.ker g } ≃ (B →+* C)

liftOfRightInverse f hf g hg is the unique ring homomorphism φ * such that φ.comp f = g (RingHom.liftOfRightInverse_comp), * where f : A →+* B has a right inverse f_inv (hf), * and g : B →+* C satisfies hg : f.ker ≤ g.ker. See RingHom.eq_liftOfRightInverse for the uniqueness lemma. `` A . | \ f | \ g | \ v \⌟ B -> C ∃!φ ``

Defined in

Mathlib.RingTheory.Ideal.Maps

Cited by

7 results in Mathlib

Foundations

Depth 33 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

RingRingRing