theorem
mem_maxideal_sq1
{Λ : Type u_1}
[CommRing Λ]
[IsLocalRing Λ]
{r : ℕ}
(x : MvPowerSeries (Fin r) Λ)
:
x ∈ IsLocalRing.maximalIdeal (MvPowerSeries (Fin r) Λ) ^ 2 →
(MvPowerSeries.constantCoeff (Fin r) Λ) x ∈ IsLocalRing.maximalIdeal Λ ^ 2 ∧ ∀ (i : Fin r), (MvPowerSeries.coeff Λ (Finsupp.single i 1)) x ∈ IsLocalRing.maximalIdeal Λ
theorem
mem_maxideal_sq2
{Λ : Type u_1}
[CommRing Λ]
[IsLocalRing Λ]
{r : ℕ}
(x : MvPowerSeries (Fin r) Λ)
:
((MvPowerSeries.constantCoeff (Fin r) Λ) x = 0 ∧ ∀ (i : Fin r), (MvPowerSeries.coeff Λ (Finsupp.single i 1)) x = 0) →
x ∈ IsLocalRing.maximalIdeal (MvPowerSeries (Fin r) Λ) ^ 2
theorem
mem_t
{Λ : Type u_1}
[CommRing Λ]
[IsLocalRing Λ]
{r : ℕ}
(x : MvPowerSeries (Fin r) Λ)
:
x ∈ denom_ideal Λ (MvPowerSeries (Fin r) Λ) ↔ (MvPowerSeries.constantCoeff (Fin r) Λ) x ∈ IsLocalRing.maximalIdeal Λ ∧ ∀ (i : Fin r), (MvPowerSeries.coeff Λ (Finsupp.single i 1)) x ∈ IsLocalRing.maximalIdeal Λ
theorem
coeff_0_out
{Λ : Type u_1}
[CommRing Λ]
[IsLocalRing Λ]
{r : ℕ}
(x y : MvPowerSeries (Fin r) Λ)
(h :
(Ideal.Quotient.mk (denom_ideal Λ (MvPowerSeries (Fin r) Λ))) x = (Ideal.Quotient.mk (denom_ideal Λ (MvPowerSeries (Fin r) Λ))) y)
:
(IsLocalRing.residue Λ) ((MvPowerSeries.constantCoeff (Fin r) Λ) x) = (IsLocalRing.residue Λ) ((MvPowerSeries.constantCoeff (Fin r) Λ) y)
theorem
coeff_single_out
{Λ : Type u_1}
[CommRing Λ]
[IsLocalRing Λ]
{r : ℕ}
(x y : MvPowerSeries (Fin r) Λ)
(i : Fin r)
(h :
(Ideal.Quotient.mk (denom_ideal Λ (MvPowerSeries (Fin r) Λ))) x = (Ideal.Quotient.mk (denom_ideal Λ (MvPowerSeries (Fin r) Λ))) y)
:
(IsLocalRing.residue Λ) ((MvPowerSeries.coeff Λ (Finsupp.single i 1)) x) = (IsLocalRing.residue Λ) ((MvPowerSeries.coeff Λ (Finsupp.single i 1)) y)
noncomputable def
R2_algEquiv_fwd
{Λ : Type u_1}
[CommRing Λ]
[IsLocalRing Λ]
{r : ℕ}
:
MvPowerSeries (Fin r) Λ ⧸ denom_ideal Λ (MvPowerSeries (Fin r) Λ) →ₐ[Λ] TrivSqZeroExt (IsLocalRing.ResidueField Λ) (Fin r → IsLocalRing.ResidueField Λ)
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
R2_algEquiv_fwd_apply
{Λ : Type u_1}
[CommRing Λ]
[IsLocalRing Λ]
{r : ℕ}
(x : MvPowerSeries (Fin r) Λ ⧸ denom_ideal Λ (MvPowerSeries (Fin r) Λ))
:
R2_algEquiv_fwd x = TrivSqZeroExt.inl ((IsLocalRing.residue Λ) ((MvPowerSeries.constantCoeff (Fin r) Λ) (Quotient.out x))) + TrivSqZeroExt.inr fun (i : Fin r) =>
(IsLocalRing.residue Λ) ((MvPowerSeries.coeff Λ (Finsupp.single i 1)) (Quotient.out x))
noncomputable def
R2_algEquiv_bwd
{Λ : Type u_1}
[CommRing Λ]
[IsLocalRing Λ]
{r : ℕ}
:
TrivSqZeroExt (IsLocalRing.ResidueField Λ) (Fin r → IsLocalRing.ResidueField Λ) →
MvPowerSeries (Fin r) Λ ⧸ denom_ideal Λ (MvPowerSeries (Fin r) Λ)
Equations
- R2_algEquiv_bwd x = Submodule.Quotient.mk ((MvPowerSeries.C (Fin r) Λ) (Quotient.out x.fst) + ∑ i : Fin r, Quotient.out (x.snd i) • MvPowerSeries.X i)
Instances For
noncomputable def
R2_algEquiv
{Λ : Type u_1}
[CommRing Λ]
[IsLocalRing Λ]
{r : ℕ}
:
(MvPowerSeries (Fin r) Λ ⧸ denom_ideal Λ (MvPowerSeries (Fin r) Λ)) ≃ₐ[Λ] TrivSqZeroExt (IsLocalRing.ResidueField Λ) (Fin r → IsLocalRing.ResidueField Λ)
Equations
- R2_algEquiv = { toFun := (↑↑R2_algEquiv_fwd.toRingHom).toFun, invFun := R2_algEquiv_bwd, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }