English
The quotient equivalence carries through various functorial and module structures, giving isomorphisms between quotient objects in compatible towers of scalars.
Русский
Квиозиционное эквивалентное соответствие сохраняется сквозь различные структурные переходы и тензорные операции над модулями.
LaTeX
$$quotientEquiv {R} {I,J,I',J'} ... : (I ⧸ J) ≃ₗ[R] (I' ⧸ J')$$
Lean4
/-- Let `I J I' J'` be nonzero fractional ideals in a Dedekind domain with `J ≤ I` and `J' ≤ I'`.
If `I/J = I'/J'` in the group of fractional ideals (i.e. `I * J' = I' * J`),
then `I/J ≃ I'/J'` as quotient `R`-modules. -/
noncomputable def quotientEquiv (I J I' J' : FractionalIdeal R⁰ K) (H : I * J' = I' * J) (h : J ≤ I) (h' : J' ≤ I')
(hJ' : J' ≠ 0) (hI : I ≠ 0) :
(I ⧸ J.coeToSubmodule.comap I.coeToSubmodule.subtype) ≃ₗ[R]
I' ⧸ J'.coeToSubmodule.comap I'.coeToSubmodule.subtype :=
by
haveI : J' ⊓ spanSingleton R⁰ (I'.divMod I J') * I = spanSingleton R⁰ (I'.divMod I J') * J :=
by
have := FractionalIdeal.sup_mul_inf J' (spanSingleton R⁰ (I'.divMod I J') * I)
rwa [FractionalIdeal.sup_eq_add, divMod_spec h' hJ' hI, mul_left_comm, mul_comm J' I, H, mul_comm I' J, ← mul_assoc,
(mul_left_injective₀ _).eq_iff] at this
rintro rfl
exact hJ' (by simpa using h')
refine .ofBijective (Submodule.mapQ _ _ (LinearMap.restrict (Algebra.lsmul R _ _ (I'.divMod I J')) ?_) ?_) ⟨?_, ?_⟩
· intro x hx
refine (divMod_spec h' hJ' hI).le ?_
exact Submodule.mem_sup_right (mul_mem_mul (mem_spanSingleton_self _ _) hx)
· rw [← Submodule.comap_comp, LinearMap.subtype_comp_restrict, LinearMap.domRestrict, Submodule.comap_comp]
refine Submodule.comap_mono ?_
intro x hx
refine (Submodule.mem_inf.mp (this.ge ?_)).1
simp only [val_eq_coe, Algebra.lsmul_coe, smul_eq_mul, mem_coe]
exact mul_mem_mul (mem_spanSingleton_self _ _) hx
· rw [← LinearMap.ker_eq_bot, Submodule.mapQ, Submodule.ker_liftQ, LinearMap.ker_comp, Submodule.ker_mkQ, ←
Submodule.comap_comp, LinearMap.subtype_comp_restrict, ← le_bot_iff, Submodule.map_le_iff_le_comap,
Submodule.comap_bot, Submodule.ker_mkQ, LinearMap.domRestrict, Submodule.comap_comp, ←
Submodule.map_le_iff_le_comap, Submodule.map_comap_eq, Submodule.range_subtype]
by_cases H' : I'.divMod I J' = 0
· obtain rfl : J' = I' := by simpa [H'] using divMod_spec h' hJ' hI
obtain rfl : I = J := mul_left_injective₀ hJ' (H.trans (mul_comm _ _))
exact inf_le_left
rw [← inv_mul_eq_iff_eq_mul₀ (by simpa [spanSingleton_eq_zero_iff] using H'), mul_inf₀ (zero_le _),
inv_mul_cancel_left₀ (by simpa [spanSingleton_eq_zero_iff] using H')] at this
rw [← this, inf_comm, coe_inf]
refine inf_le_inf ?_ le_rfl
intro x hx
rw [spanSingleton_inv]
convert mul_mem_mul (mem_spanSingleton_self _ _) hx
simp [H']
· have H : Submodule.map (Algebra.lsmul R R K (I'.divMod I J')) ↑I = (spanSingleton R⁰ (I'.divMod I J') * I) :=
by
ext x
simp [Submodule.mem_span_singleton_mul]
rw [← LinearMap.range_eq_top, Submodule.mapQ, Submodule.range_liftQ, LinearMap.range_comp, LinearMap.restrict,
LinearMap.range_codRestrict, LinearMap.range_domRestrict, ← top_le_iff, H, ←
LinearMap.range_eq_top.mpr (Submodule.mkQ_surjective _), ← Submodule.map_top, Submodule.map_le_iff_le_comap,
Submodule.comap_map_eq, Submodule.ker_mkQ, ←
Submodule.map_le_map_iff_of_injective I'.coeToSubmodule.injective_subtype, Submodule.map_top, Submodule.map_sup,
Submodule.map_comap_eq, Submodule.map_comap_eq, Submodule.range_subtype, sup_comm, inf_eq_right.mpr,
inf_eq_right.mpr]
· exact le_trans (divMod_spec h' hJ' hI).ge (by simp)
· exact le_trans (by simp) (divMod_spec h' hJ' hI).le
· exact h'
