theorem mem_maximalideal_pow (Λ : Type u_1) [CommRing Λ] [IsLocalRing Λ] (r k : ℕ) (x : MvPowerSeries (Fin r) Λ) : x ∈ IsLocalRing.maximalIdeal (MvPowerSeries (Fin r) Λ) ^ k ↔ ∀ (n : Fin r →₀ ℕ), (MvPowerSeries.coeff Λ n) x ∈ IsLocalRing.maximalIdeal Λ ^ (k - n.degree)

theorem eventually_in_maxideal_pow (Λ : Type u_1) [CommRing Λ] [IsLocalRing Λ] (r : ℕ) [TopologicalSpace Λ] (h : ∀ (k : ℕ), (IsLocalRing.maximalIdeal Λ ^ k).carrier ∈ nhds 0) (N : ℕ) : ∀ᶠ (x : MvPowerSeries (Fin r) Λ) in nhds 0, x ∈ IsLocalRing.maximalIdeal (MvPowerSeries (Fin r) Λ) ^ N

instance instIsCompleteMvPowerSeriesFin (Λ : Type u_1) [CommRing Λ] [IsLocalRing Λ] (r : ℕ) [Deformation.IsComplete Λ] : Deformation.IsComplete (MvPowerSeries (Fin r) Λ)

instance instIsResidueAlgebraMvPowerSeriesFin (Λ : Type u_1) [CommRing Λ] [IsLocalRing Λ] (r : ℕ) : IsResidueAlgebra Λ (MvPowerSeries (Fin r) Λ)

def seq {R : Type u_1} [CommRing R] [IsLocalRing R] (J : ℕ → Ideal R) (hJ : Antitone J) (k : ℕ) : ℕᵒᵈ →o { p : Ideal R // IsLocalRing.maximalIdeal R ^ k ≤ p }

Equations

• seq J hJ k = { toFun := fun (l : ℕᵒᵈ) => ⟨J l ⊔ IsLocalRing.maximalIdeal R ^ k, ⋯⟩, monotone' := ⋯ }

instance instIsArtinianRingQuotientIdealHPowNatMaximalIdealOfIsNoetherianRing_schlessinger {R : Type u_1} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (k : ℕ) : IsArtinianRing (R ⧸ IsLocalRing.maximalIdeal R ^ k)

theorem WellFoundedLT.antitone_chain_condition {α : Type u_2} [PartialOrder α] [h : WellFoundedLT α] (a : ℕᵒᵈ →o α) : ∃ (n : ℕᵒᵈ), ∀ m ≤ n, a n = a m

theorem N_def {R : Type u_1} [CommRing R] [IsLocalRing R] (J : ℕ → Ideal R) (hJ : Antitone J) [IsNoetherianRing R] (k i : ℕ) : (seq J hJ k) (⋯.choose k) ≤ (seq J hJ k) i

theorem JN_le {R : Type u_1} [CommRing R] [IsLocalRing R] (J : ℕ → Ideal R) (hJ : Antitone J) (hmJ : ∀ (n : ℕ), IsLocalRing.maximalIdeal R ^ n ≤ J n) [IsNoetherianRing R] (k : ℕ) : J (⋯.choose k) ⊔ IsLocalRing.maximalIdeal R ^ k ≤ J k

theorem indstep {R : Type u_1} [CommRing R] [IsLocalRing R] (J : ℕ → Ideal R) (hJ : Antitone J) [IsNoetherianRing R] {k : ℕ} (x₀ : ↥(J (⋯.choose k))) : ∃ (x : ↥(J (⋯.choose (k + 1)))), ↑x₀ - ↑x ∈ IsLocalRing.maximalIdeal R ^ k

noncomputable def seqx_aux {R : Type u_1} [CommRing R] [IsLocalRing R] (J : ℕ → Ideal R) (hJ : Antitone J) [IsNoetherianRing R] (i : ℕ) (x : ↥(J (⋯.choose i))) (n : ℕ) : ↥(J (⋯.choose (i + n)))

Equations

• seqx_aux J hJ i x Nat.zero = x
• seqx_aux J hJ i x n.succ = ⋯.choose

theorem seqx_aux_prop {R : Type u_1} [CommRing R] [IsLocalRing R] (J : ℕ → Ideal R) (hJ : Antitone J) [IsNoetherianRing R] (i : ℕ) (x : ↥(J (⋯.choose i))) (n : ℕ) : ↑(seqx_aux J hJ i x n) - ↑(seqx_aux J hJ i x (n + 1)) ∈ IsLocalRing.maximalIdeal R ^ (i + n)

noncomputable def seqx {R : Type u_1} [CommRing R] [IsLocalRing R] (J : ℕ → Ideal R) (hJ : Antitone J) [IsNoetherianRing R] (i : ℕ) (x : ↥(J (⋯.choose i))) : ℕ → R

Equations

• seqx J hJ i x n = if i ≤ n then ↑(seqx_aux J hJ i x (n - i)) else ↑x

theorem seqx_mem {R : Type u_1} [CommRing R] [IsLocalRing R] (J : ℕ → Ideal R) (hJ : Antitone J) (hmJ : ∀ (n : ℕ), IsLocalRing.maximalIdeal R ^ n ≤ J n) [IsNoetherianRing R] (i : ℕ) (x : ↥(J (⋯.choose i))) (k : ℕ) : seqx J hJ i x k ∈ J k

theorem adiccauchy {R : Type u_1} [CommRing R] [IsLocalRing R] (J : ℕ → Ideal R) (hJ : Antitone J) [IsNoetherianRing R] (i : ℕ) (x : ↥(J (⋯.choose i))) : AdicCompletion.IsAdicCauchy (IsLocalRing.maximalIdeal R) R (seqx J hJ i x)

theorem sametopo' {R : Type u_1} [CommRing R] [IsLocalRing R] (J : ℕ → Ideal R) (hJ : Antitone J) (hmJ : ∀ (n : ℕ), IsLocalRing.maximalIdeal R ^ n ≤ J n) [IsNoetherianRing R] [Deformation.IsComplete R] (n : ℕ) : ∃ (k : ℕ), J k ≤ IsLocalRing.maximalIdeal R ^ n ⊔ iInf J

Stacks Tag 06SE

def J_aux {R : Type u_1} [CommRing R] [IsLocalRing R] (J : ℕ → Ideal R) : ℕ → Ideal R

Equations

• J_aux J 0 = ⊤
• J_aux J 1 = IsLocalRing.maximalIdeal R ⊔ J 0
• J_aux J n.succ.succ = J n

theorem J_aux_anti {R : Type u_1} [CommRing R] [IsLocalRing R] (J : ℕ → Ideal R) (hJ : Antitone J) : Antitone (J_aux J)

theorem J_aux_hmJ {R : Type u_1} [CommRing R] [IsLocalRing R] (J : ℕ → Ideal R) (hmJ : ∀ (n : ℕ), IsLocalRing.maximalIdeal R ^ (n + 2) ≤ J n) (n : ℕ) : IsLocalRing.maximalIdeal R ^ n ≤ J_aux J n

@[simp]

theorem J_aux_iInf {R : Type u_1} [CommRing R] [IsLocalRing R] (J : ℕ → Ideal R) : iInf (J_aux J) = iInf J

@[simp]

theorem J_le_aux_max_2 {R : Type u_1} [CommRing R] [IsLocalRing R] (J : ℕ → Ideal R) (hJ : Antitone J) (k : ℕ) : J (max k 2) ≤ J_aux J k

theorem sametopo {R : Type u_1} [CommRing R] [IsLocalRing R] (J : ℕ → Ideal R) (hJ : Antitone J) [IsNoetherianRing R] [Deformation.IsComplete R] (hmJ : ∀ (n : ℕ), IsLocalRing.maximalIdeal R ^ (n + 2) ≤ J n) (n : ℕ) : ∃ (k : ℕ), J k ≤ IsLocalRing.maximalIdeal R ^ n ⊔ iInf J