GradedCompletion.lean`

25 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.SectionCompletion.isNoetherianRing_of_finiteType line 10
lemma OAI.SectionCompletion.adicComplete_of_finiteType line 17
def OAI.SectionCompletion.degreeIdeal line 32
Source documentation
The descending coefficient filtration on the graded polynomial algebra.
```
def degreeIdeal (n : ℕ) : Ideal (polynomials T) :=
…
```
Mentions: OAI.SectionCompletion.polynomials
lemma OAI.SectionCompletion.mem_degreeIdeal line 35
lemma OAI.SectionCompletion.degreeIdeal_one_pow_le line 40
lemma OAI.SectionCompletion.monomial_mem_degreeIdeal_one line 45

lemma OAI.SectionCompletion.degreeIdeal_cofinal line 55

Source documentation

Finite positive homogeneous generation makes the degree and augmentation filtrations cofinal; this is the estimate used in the manuscript, lines 224–237.

lemma degreeIdeal_cofinal {σ : Type} [Fintype σ] (v : σ → K) (d : σ → ℕ)
    (hd : ∀ i, d i ≠ 0) (hv : ∀ i, v i ∈ T (d i))
    (hspan : ∀ j, T j = HomogeneousGeneration.spanPiece v d j)
    (D : ℕ) (hD : 0 < D) (hbound : ∀ i, d i ≤ D) (n : ℕ) :
    degreeIdeal T (n * D) ≤ degreeIdeal T 1 ^ n := by
…

Mentions: OAI.HomogeneousGeneration.spanPiece, OAI.SectionCompletion.degreeIdeal

def OAI.SectionCompletion.truncation line 133
Source documentation
A finite polynomial truncation of a coefficient-compatible series.
```
def truncation (n : ℕ) (p : series T) : polynomials T :=
…
```
Mentions: OAI.SectionCompletion.series, OAI.SectionCompletion.polynomials
lemma OAI.SectionCompletion.coeff_truncation line 141
lemma OAI.SectionCompletion.truncation_sub_mem_pow line 149
def OAI.SectionCompletion.quotientTruncation line 161
Source documentation
Truncation at the cofinal degree gives a genuine quotient algebra map.
```
def quotientTruncation (n : ℕ) : series T →ₐ[k] polynomials T ⧸ degreeIdeal T 1 ^ n where
…
```
Mentions: OAI.SectionCompletion.series, OAI.SectionCompletion.polynomials, OAI.SectionCompletion.degreeIdeal
lemma OAI.SectionCompletion.quotientTruncation_compatible line 206
def OAI.SectionCompletion.toCompletion line 216
Source documentation
The coefficient ring maps canonically to the vertex-adic completion.
```
def toCompletion : series T →ₐ[k] AdicCompletion (degreeIdeal T 1) (polynomials T) :=
…
```
Mentions: OAI.SectionCompletion.series, OAI.SectionCompletion.degreeIdeal, OAI.SectionCompletion.polynomials
lemma OAI.SectionCompletion.eval_toCompletion line 220
lemma OAI.SmallCM.completion_eval_compatible line 230
lemma OAI.SmallCM.mk_out_completion_eval line 241
lemma OAI.SectionCompletion.quotient_coeff_eq line 254
def OAI.SectionCompletion.fromCompletion line 263
Source documentation
Compatible vertex-adic residues determine each homogeneous coefficient.
```
def fromCompletion (x : AdicCompletion (degreeIdeal T 1) (polynomials T)) : series T :=
…
```
Mentions: OAI.SectionCompletion.degreeIdeal, OAI.SectionCompletion.polynomials, OAI.SectionCompletion.series
lemma OAI.SectionCompletion.coeff_fromCompletion line 269
lemma OAI.SectionCompletion.from_toCompletion line 280
lemma OAI.SectionCompletion.to_fromCompletion line 294
def OAI.SectionCompletion.completionEquiv line 316
Source documentation
Literal identification of the graded coefficient completion and the completion at the positive-degree ideal; no standard grading is assumed.
```
def completionEquiv : series T ≃ₐ[k] AdicCompletion (degreeIdeal T 1) (polynomials T) where
…
```
Mentions: OAI.SectionCompletion.series, OAI.SectionCompletion.degreeIdeal, OAI.SectionCompletion.polynomials
lemma OAI.SectionCompletion.mem_degreeIdeal_one line 327
lemma OAI.SectionCompletion.degreeIdeal_one_isMaximal line 332
lemma OAI.ExplicitCone.rationalCone_trdeg line 363