English
There is a natural bijection between divisors of I and divisors of J induced by a quotient equivalence f: R/I ≃+* A/J.
Русский
Существует естественная биекция между делителями I и делителями J, индуцированная эквивалентом тquotient f.
LaTeX
$$idealFactorsEquivOfQuotEquiv$$
Lean4
/-- The bijection between ideals of `R` dividing `I` and the ideals of `A` dividing `J` induced by
an isomorphism `f : R/I ≅ A/J`. -/
def idealFactorsEquivOfQuotEquiv : {p : Ideal R | p ∣ I} ≃o {p : Ideal A | p ∣ J} :=
by
have f_surj : Function.Surjective (f : R ⧸ I →+* A ⧸ J) := f.surjective
have fsym_surj : Function.Surjective (f.symm : A ⧸ J →+* R ⧸ I) := f.symm.surjective
refine OrderIso.ofHomInv (idealFactorsFunOfQuotHom f_surj) (idealFactorsFunOfQuotHom fsym_surj) ?_ ?_
· have := idealFactorsFunOfQuotHom_comp fsym_surj f_surj
simp only [RingEquiv.comp_symm, idealFactorsFunOfQuotHom_id] at this
rw [← this, OrderHom.coe_eq, OrderHom.coe_eq]
· have := idealFactorsFunOfQuotHom_comp f_surj fsym_surj
simp only [RingEquiv.symm_comp, idealFactorsFunOfQuotHom_id] at this
rw [← this, OrderHom.coe_eq, OrderHom.coe_eq]
