OAI/AlgebraicGeometry/SurfaceCones/RingProperties.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SectionCompletion.initial line 15

   Source documentation

   The initial homogeneous polynomial, including zero.

   noncomputable def initial (f : PowerSeries K) : Polynomial K :=
   …

2. lemma OAI.SectionCompletion.initial_zero line 18
3. lemma OAI.SectionCompletion.initial_one line 21
4. lemma OAI.SectionCompletion.initial_mul line 24
5. lemma OAI.SectionCompletion.initial_pow line 33
6. lemma OAI.SectionCompletion.initial_eq line 38
7. lemma OAI.SectionCompletion.initial_ne_zero line 42
8. lemma OAI.SectionCompletion.initial_mem line 48
9. lemma OAI.SectionCompletion.initial_isAlmostIntegral line 52
10. lemma OAI.SectionCompletion.initial_mem_of_isAlmostIntegral line 70
11. lemma OAI.SectionCompletion.mem_of_isAlmostIntegral line 79

    Source documentation

    Normality is detected one homogeneous initial term at a time.

    lemma mem_of_isAlmostIntegral [IsNoetherianRing (polynomials T)]
        [IsIntegrallyClosedIn (polynomials T) (Polynomial K)] {f : PowerSeries K}
        (hf : IsAlmostIntegral (series T) f) : f ∈ series T := by
    …

    Mentions: OAI.SectionCompletion.polynomials, OAI.SectionCompletion.series

12. lemma OAI.SectionCompletion.isIntegrallyClosed_series line 113

    Source documentation

    The coefficient product of a normal Noetherian graded algebra is normal. The ambient function-field power-series ring is a DVR; denominators transfer almost integrality to it, where the preceding initial-term induction applies.

    lemma isIntegrallyClosed_series [IsNoetherianRing (polynomials T)]
        [IsIntegrallyClosedIn (polynomials T) (Polynomial K)] :
        IsIntegrallyClosed (series T) := by
    …

    Mentions: OAI.SectionCompletion.polynomials, OAI.SectionCompletion.series

13. lemma OAI.GradedNormalization.normalized_completion_properties line 162

    Source documentation

    The normalized cone coefficient completion is Noetherian, normal, local and complete, with the prescribed residue field.

    lemma normalized_completion_properties [IsAlgClosed k] [Algebra.FiniteType k B]
        [IsFractionRing B (RatFunc L)]
        (hB : ∀ a : k, ∀ p ∈ B, scale a p ∈ B)
        (hzero : ∀ p ∈ B, p.coeff 0 ∈ (⊥ : Subalgebra k L)) :
        let R := SectionCompletion.series (piece B)
    …

    Mentions: OAI.GradedNormalization.scale, OAI.SectionCompletion.series, OAI.GradedNormalization.piece

14. instance OAI.ExplicitCone.completedRing_isIntegrallyClosed line 189
15. instance OAI.ExplicitCone.completedRing_isAdicComplete line 193
16. lemma OAI.ExplicitCone.completedRing_residue_bijective line 199
17. lemma OAI.SmallCM.mvPolynomial_maximal_height line 209
18. lemma OAI.SmallCM.finiteType_maximal_height line 232

    Source documentation

    All closed points of an affine integral variety have full height.

    lemma finiteType_maximal_height (k B : Type) [Field k] [CommRing B] [IsDomain B]
        [Algebra k B] [Algebra.FiniteType k B] (M : Ideal B) [M.IsMaximal] :
        (M.height : WithBot ℕ∞) = ringKrullDim B := by
    …

19. lemma OAI.SmallCM.completion_at_maximal_dimension line 254
20. lemma OAI.SectionCompletion.series_dimension line 280
21. lemma OAI.ExplicitCone.polynomialAlgebra_dimension line 310
22. lemma OAI.ExplicitCone.gradedAlgebra_dimension line 315
23. lemma OAI.ExplicitCone.completedRing_dimension line 333