idealFactorsFunOfQuotHom — Mathlib

English

There is a map from ideals of R dividing I to ideals of A dividing J induced by a surjective quotient hom f: R/I → A/J.

Русский

Существует отображение от идеалов R, делящих I, к идеалам A, делящих J, индуцируемое сюръективным гомоморфизмом по тquotient.

LaTeX

$$$\\text{idealFactorsFunOfQuotHom}\\,f : \\{p\\mid I\\} \\to_o \\{p'\\mid J\\}$$$

Lean4

/-- The map from ideals of `R` dividing `I` to the ideals of `A` dividing `J` induced by
  a homomorphism `f : R/I →+* A/J` -/
@[simps]
def idealFactorsFunOfQuotHom {f : R ⧸ I →+* A ⧸ J} (hf : Function.Surjective f) :
    { p : Ideal R // p ∣ I } →o { p : Ideal A // p ∣ J }
    where
  toFun
    X :=
    ⟨comap (Ideal.Quotient.mk J) (map f (map (Ideal.Quotient.mk I) X)),
      by
      have : RingHom.ker (Ideal.Quotient.mk J) ≤ comap (Ideal.Quotient.mk J) (map f (map (Ideal.Quotient.mk I) X)) :=
        ker_le_comap (Ideal.Quotient.mk J)
      rw [mk_ker] at this
      exact dvd_iff_le.mpr this⟩
  monotone' := by
    rintro ⟨X, hX⟩ ⟨Y, hY⟩ h
    rw [← Subtype.coe_le_coe, Subtype.coe_mk, Subtype.coe_mk] at h ⊢
    rw [Subtype.coe_mk, comap_le_comap_iff_of_surjective (Ideal.Quotient.mk J) Ideal.Quotient.mk_surjective,
      map_le_iff_le_comap, Subtype.coe_mk, comap_map_of_surjective _ hf (map (Ideal.Quotient.mk I) Y)]
    suffices map (Ideal.Quotient.mk I) X ≤ map (Ideal.Quotient.mk I) Y by exact le_sup_of_le_left this
    rwa [map_le_iff_le_comap, comap_map_of_surjective (Ideal.Quotient.mk I) Ideal.Quotient.mk_surjective, ←
      RingHom.ker_eq_comap_bot, mk_ker, sup_eq_left.mpr <| le_of_dvd hY]

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