English
The symmetric bijection in normalizedFactorsEquivOfQuotEquiv respects inversion.
Русский
Симметричная биекция в нормализованных факторах уважает инверсию.
LaTeX
$$normalizedFactorsEquivOfQuotEquiv_symm$$
Lean4
/-- The bijection between the sets of normalized factors of I and J induced by a ring
isomorphism `f : R/I ≅ A/J`. -/
def normalizedFactorsEquivOfQuotEquiv (hI : I ≠ ⊥) (hJ : J ≠ ⊥) :
{L : Ideal R | L ∈ normalizedFactors I} ≃ {M : Ideal A | M ∈ normalizedFactors J}
where
toFun
j :=
⟨idealFactorsEquivOfQuotEquiv f ⟨↑j, dvd_of_mem_normalizedFactors j.prop⟩,
idealFactorsEquivOfQuotEquiv_mem_normalizedFactors_of_mem_normalizedFactors f hJ j.prop⟩
invFun
j :=
⟨(idealFactorsEquivOfQuotEquiv f).symm ⟨↑j, dvd_of_mem_normalizedFactors j.prop⟩,
by
rw [idealFactorsEquivOfQuotEquiv_symm]
exact idealFactorsEquivOfQuotEquiv_mem_normalizedFactors_of_mem_normalizedFactors f.symm hI j.prop⟩
left_inv := fun ⟨j, hj⟩ => by simp
right_inv := fun ⟨j, hj⟩ => by simp [-Set.coe_setOf]
