Theorems · Theorem · commutative algebra

Ideal.injective_quotient_le_comap_map

∀ {R : Type u_1} [inst : CommRing R] (P : Ideal (Polynomial R)),
  Function.Injective
    ⇑(Ideal.quotientMap (Ideal.map (Polynomial.mapRingHom (Ideal.Quotient.mk (Ideal.comap Polynomial.C P))) P)
        (Polynomial.mapRingHom (Ideal.Quotient.mk (Ideal.comap Polynomial.C P))) ⋯)

Let P be an ideal in R[x]. The map R[x]/P → (R / (P ∩ R))[x] / (P / (P ∩ R)) is injective.

Defined in: Mathlib.RingTheory.Ideal.GoingUp
Cited by: 1 results in Mathlib
Foundations: Depth 107 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommRing

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites30

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coestatement · cited by 62,936
CommRingstatement and proof · cited by 17,173
RingHomstatement · cited by 10,189
Polynomialstatement and proof · cited by 5,681
Idealstatement and proof · cited by 4,748
Bot.botproof · cited by 4,720
HasQuotient.Quotientstatement · cited by 2,301
le_antisymmproof · cited by 2,068
Polynomial.Cstatement and proof · cited by 1,598
le_rflproof · cited by 1,558
Polynomial.coeffproof · cited by 1,045
Ideal.mapstatement · cited by 692

Cited by1

Results whose statement or proof uses this declaration.

Polynomial.quotient_mk_comp_C_isIntegral_of_isJacobsonRingproof · cited by 2