algEquivQuotient — Mathlib

English

Let A be a commutative ring, g ∈ A[X] be distinguished with respect to an ideal I of A, and A be adically complete with respect to I. Then the natural map from polynomial quotients to power-series quotients induces an algebra isomorphism between A[X]/(g) and A⟦X⟧/(g).

Русский

Пусть A — коммутативное кольцо, g ∈ A[X] является различимым по отношению к идеалу I (A[I]-адично полно), и A адически полнопо отношению к I. Тогда естественный гомоморфизм порождает изоморфизм между кольцами частных A[X]/(g) и A⟦X⟧/(g).

LaTeX

$$$A[X] / (g) \cong_A A\llbracket X\rrbracket / (g)$$$

Lean4

/-- A distinguished polynomial `g` induces a natural isomorphism `A[X] / (g) ≃ₐ[A] A⟦X⟧ / (g)`. -/
@[simps! apply symm_apply]
noncomputable def _root_.Polynomial.IsDistinguishedAt.algEquivQuotient :
    (A[X] ⧸ Ideal.span { g }) ≃ₐ[A] A⟦X⟧ ⧸ Ideal.span {(g : A⟦X⟧)}
    where
  __ :=
    Ideal.quotientMapₐ _ (Polynomial.coeToPowerSeries.algHom A) fun a ha ↦
      by
      obtain ⟨b, hb⟩ := Ideal.mem_span_singleton'.1 ha
      simp only [Ideal.mem_comap, Polynomial.coeToPowerSeries.algHom_apply, Algebra.algebraMap_self, map_id, id_eq,
        Ideal.mem_span_singleton']
      exact ⟨b, by simp [← hb]⟩
  invFun := Ideal.Quotient.mk _ ∘ H.isWeierstrassDivisorAt'.mod'
  left_inv
    f := by
    rcases subsingleton_or_nontrivial A with _ | _
    · have : Subsingleton A[X] := inferInstance
      have : Subsingleton (A[X] ⧸ Ideal.span { g }) := Quot.Subsingleton
      exact Subsingleton.elim _ _
    have hI : I ≠ ⊤ := by
      rintro rfl
      exact not_subsingleton _ ‹IsAdicComplete ⊤ A›.toIsHausdorff.subsingleton
    have := Ideal.Quotient.nontrivial hI
    obtain ⟨f, hfdeg, rfl⟩ : ∃ r : A[X], r.degree < g.degree ∧ Ideal.Quotient.mk _ r = f :=
      by
      obtain ⟨f, rfl⟩ := Ideal.Quotient.mk_surjective f
      refine ⟨f %ₘ g, Polynomial.degree_modByMonic_lt f H.monic, ?_⟩
      rw [Eq.comm, Ideal.Quotient.mk_eq_mk_iff_sub_mem, Ideal.mem_span_singleton']
      exact ⟨f /ₘ g, by rw [Polynomial.modByMonic_eq_sub_mul_div _ H.monic]; ring⟩
    have h1 : g.degree = ((g : A⟦X⟧).map (Ideal.Quotient.mk I)).order.toNat :=
      by
      convert H.degree_eq_coe_lift_order_map g 1 (by rwa [constantCoeff_one, ← Ideal.ne_top_iff_one]) (by simp)
      exact (ENat.lift_eq_toNat_of_lt_top _).symm
    dsimp
    rw [Ideal.Quotient.mk_eq_mk_iff_sub_mem, Ideal.mem_span_singleton']
    exact ⟨0, by simp [H.isWeierstrassDivisorAt'.mod_coe_eq_self (hfdeg.trans_eq h1)]⟩
  right_inv f := by exact H.isWeierstrassDivisorAt'.mk_mod'_eq_self

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