OAI/AlgebraicGeometry/SurfaceCones/CompletionParameters.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

Degree-one Noether normalization needed for the actual section cone. The generators and all replacements are homogeneous of degree one.

  1. lemma OAI.HomogeneousNoetherNormalization.cone_monomial line 17
  2. lemma OAI.HomogeneousNoetherNormalization.coeff_cone_aeval line 29
  3. lemma OAI.HomogeneousNoetherNormalization.homogeneous_relation line 40
  4. lemma OAI.HomogeneousNoetherNormalization.eval_scalar line 74
  5. lemma OAI.HomogeneousNoetherNormalization.exists_projective_nonvanishing line 87
  6. lemma OAI.HomogeneousNoetherNormalization.coeff_prod_sum line 110
  7. lemma OAI.HomogeneousNoetherNormalization.affine_degree line 122
  8. lemma OAI.HomogeneousNoetherNormalization.affine_aeval_degree line 128
  9. lemma OAI.HomogeneousNoetherNormalization.affine_aeval_top_coeff line 145
  10. lemma OAI.HomogeneousNoetherNormalization.integral_head_of_relation line 171
  11. lemma OAI.HomogeneousNoetherNormalization.cone_aeval_homogeneous line 213
  12. def OAI.HomogeneousNoetherNormalization.cone line 224
  13. lemma OAI.HomogeneousNoetherNormalization.cone_gen_mem line 227
  14. lemma OAI.HomogeneousNoetherNormalization.cone_shift_le line 230
  15. lemma OAI.HomogeneousNoetherNormalization.cone_shift_integral line 239
  16. theorem OAI.HomogeneousNoetherNormalization.exists_linear_normalization line 272

    Source documentation

    Linear changes only: unlike ordinary normalization, the parameters stay in degree one. The integral map is the literal inclusion into the input cone.

    theorem exists_linear_normalization [Infinite k] {n : ℕ} (v : Fin n → L) :
    ∃ m ≤ n, ∃ w : Fin m → L, ∃ h : cone (k := k) w ≤ cone v,
…

    Mentions: OAI.HomogeneousNoetherNormalization.cone

  17. def OAI.HomogeneousNoetherNormalization.coneEval line 301
  18. lemma OAI.HomogeneousNoetherNormalization.coneEval_surjective line 305
  19. instance OAI.HomogeneousNoetherNormalization.finiteType_cone line 313
  20. lemma OAI.HomogeneousNoetherNormalization.inclusion_finite line 316
  21. theorem OAI.HomogeneousNoetherNormalization.exists_finite_linear_normalization line 329

    Source documentation

    For a cone of transcendence degree r, exactly r parameters suffice, all of them linear rather than arbitrary Noether-normalization polynomials.

    theorem exists_finite_linear_normalization [Infinite k] {n r : ℕ} (v : Fin n → L)
    (hr : Algebra.trdeg k (cone (k := k) v) = r) :
…

    Mentions: OAI.HomogeneousNoetherNormalization.cone

  22. lemma OAI.ExplicitCone.polynomialAlgebra_trdeg line 360
  23. lemma OAI.ExplicitCone.exists_linear_parameters line 364
  24. lemma OAI.SmallCM.precomplete_pi line 388
  25. lemma OAI.SmallCM.finite_of_adic_finite_quotient line 401

    Source documentation

    Adic Nakayama without assuming the target finitely generated.

    lemma finite_of_adic_finite_quotient {A M : Type*} [CommRing A]
    [AddCommGroup M] [Module A M] (I : Ideal A)
    [IsPrecomplete I A] [IsHausdorff I M]
    [Module.Finite A (M ⧸ (I • ⊤ : Submodule A M))] : Module.Finite A M := by
…
  26. lemma OAI.SmallCM.finite_fiber_of_maximal_map line 417

    Source documentation

    A finite closed fiber stays finite after completion whenever the image of the original maximal ideal generates the completed maximal ideal.

    lemma finite_fiber_of_maximal_map {k B R : Type*} [Field k] [IsAlgClosed k]
    [CommRing B] [Algebra k B] [CommRing R] [IsNoetherianRing R]
    [IsLocalRing R] [Algebra k R]
    [Module.Finite k (IsLocalRing.ResidueField R)]
    (g : B →ₐ[k] R) (I m : Ideal B) (hIm : I ≤ m)
    (hm : m.map g.toRingHom = IsLocalRing.maximalIdeal R)
    [Module.Finite k (B ⧸ I)] : Module.Finite k (R ⧸ I.map g.toRingHom) := by
…
  27. lemma OAI.SmallCM.finite_of_finite_mapped_fiber line 456
  28. lemma OAI.SmallCM.finite_polynomial_origin_fiber line 477

    Source documentation

    The fiber over the origin of a finite polynomial-algebra map is finite as a vector space over the coefficient field.

    lemma finite_polynomial_origin_fiber {k B σ : Type*} [Field k]
    [CommRing B] [Algebra k B] (f : MvPolynomial σ k →ₐ[k] B)
    (hf : f.Finite) :
    Module.Finite k (B ⧸ Ideal.span (Set.range (fun i => f (MvPolynomial.X i)))) := by
…
  29. lemma OAI.SectionCompletion.completionEquiv_polynomial line 506
  30. lemma OAI.SectionCompletion.maximal_polynomialToSeries line 524
  31. def OAI.SectionCompletion.linearPolynomialMap line 562
  32. lemma OAI.SectionCompletion.polynomial_subst_X line 567
  33. lemma OAI.SectionCompletion.finite_linear_substitution line 582

    Source documentation

    Completion of finite degree-one Noether normalization stays finite, proved directly by closed-fiber finiteness and adic Nakayama.

    lemma finite_linear_substitution [Algebra.FiniteType k (polynomials T)]
    (hzero : T 0 = LinearMap.range (Algebra.linearMap k K))
    (hfin : (linearPolynomialMap T w hw).Finite) :
    (SectionGenerated.substHom T w (fun _ => 1) (fun _ => one_ne_zero) hw).Finite := by
…

    Mentions: OAI.SectionCompletion.polynomials, OAI.SectionCompletion.linearPolynomialMap, OAI.SectionGenerated.substHom

  34. lemma OAI.GradedNormalization.finite_normalization_map line 633
  35. lemma OAI.GradedNormalization.finite_normalized_linear_parameters line 647
  36. lemma OAI.ExplicitCone.exists_finite_linear_completed_parameters line 676
  37. lemma OAI.HomogeneousParameters.prod_monomials line 694
  38. lemma OAI.HomogeneousParameters.linearIndependent_degree_fiber line 706
  39. lemma OAI.SectionGenerated.linear_subst_eq_zero line 729
  40. lemma OAI.SectionGenerated.linear_subst_injective line 745
  41. lemma OAI.SectionGenerated.substHom_injective_linear line 758
  42. lemma OAI.ExplicitCone.exists_finite_injective_completed_parameters line 769