English
The underlying function of quotQuotEquivCommₐ R I J equals the underlying function of quotQuotEquivComm I J.
Русский
Функциональная часть quotQuotEquivCommₐ R I J равна функции quotQuotEquivComm I J.
LaTeX
$$$\text{coe} (quotQuotEquivCommₐ\, R\, I\, J) = \text{coe} (quotQuotEquivComm\, I\, J)$$$
Lean4
/-- `I ^ n ⧸ I ^ (n + 1)` can be viewed as a quotient module and as ideal of `R ⧸ I ^ (n + 1)`.
This definition gives the `R`-linear equivalence between the two. -/
noncomputable def powQuotPowSuccLinearEquivMapMkPowSuccPow :
((I ^ n : Ideal R) ⧸ (I • ⊤ : Submodule R (I ^ n : Ideal R))) ≃ₗ[R]
Ideal.map (Ideal.Quotient.mk (I ^ (n + 1))) (I ^ n) :=
by
refine
{
LinearMap.codRestrict (Submodule.restrictScalars _ (Ideal.map (Ideal.Quotient.mk (I ^ (n + 1))) (I ^ n)))
(Submodule.mapQ (I • ⊤) (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ?_) ?_,
Equiv.ofBijective _ ⟨?_, ?_⟩ with }
· intro
simp [Submodule.mem_smul_top_iff, pow_succ']
· intro x
obtain ⟨⟨y, hy⟩, rfl⟩ := Submodule.Quotient.mk_surjective _ x
simp [Ideal.mem_sup_left hy]
· intro a b
obtain ⟨⟨x, hx⟩, rfl⟩ := Submodule.Quotient.mk_surjective _ a
obtain ⟨⟨y, hy⟩, rfl⟩ := Submodule.Quotient.mk_surjective _ b
simp [Ideal.Quotient.eq, Submodule.Quotient.eq, Submodule.mem_smul_top_iff, pow_succ']
· intro ⟨x, hx⟩
rw [Ideal.mem_map_iff_of_surjective _ Ideal.Quotient.mk_surjective] at hx
obtain ⟨y, hy, rfl⟩ := hx
refine ⟨Submodule.Quotient.mk ⟨y, hy⟩, ?_⟩
simp
