OAI/AlgebraicGeometry/SurfaceCones/KummerProjCover.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Identification of smooth coefficient algebras with homogeneous Proj charts.

  1. lemma OAI.SourceSymmetry.coefficientChart_normal line 11
  2. lemma OAI.SourceSymmetry.coefficientChart_smooth line 16
  3. def OAI.SourceSymmetry.coefficientCartierChart line 21
  4. lemma OAI.SourceSymmetry.generator_eq_ratio_mul_at line 25
  5. lemma OAI.SourceSymmetry.generator_mem_coefficientCartierChart line 33
  6. lemma OAI.SourceSymmetry.algebra_le_coefficientCartierChart line 41
  7. lemma OAI.SourceSymmetry.normalizedCone_le_coefficientCartierChart line 47
  8. lemma OAI.SourceSymmetry.integral_polynomial_mem_coefficientCartierChart line 53
  9. lemma OAI.SourceSymmetry.normalized_coefficient_mem_coefficientChart line 61
  10. abbrev OAI.SourceSymmetry.projChart line 69
  11. def OAI.SourceSymmetry.projChartEquiv line 72
  12. lemma OAI.SourceSymmetry.projChart_smooth line 78
  13. abbrev OAI.SourceSymmetry.projSection line 84
  14. def OAI.SourceSymmetry.projOpenIso line 87
  15. lemma OAI.SourceSymmetry.integral_eq_scalar line 101
  16. lemma OAI.SourceSymmetry.integral_image_scalars line 110
  17. lemma OAI.SourceSymmetry.adjoin_image_scalars line 128
  18. lemma OAI.SourceSymmetry.homogeneous_mem_of_integral_adjoin line 153

    Source documentation

    Integral homogeneous extensions acquire no nonvertex point over the common vanishing of the generators.

    lemma homogeneous_mem_of_integral_adjoin {k B A : Type*}
    [Field k] [IsAlgClosed k] [CommRing B] [CommRing A]
    [Algebra k B] [Algebra k A]
    (𝒜 : ℕ → Submodule k A) [GradedAlgebra 𝒜]
    (s : Set B) (f : Algebra.adjoin k s →ₐ[k] A)
    (hint : f.toRingHom.IsIntegral) (P : HomogeneousIdeal 𝒜) [P.toIdeal.IsPrime]
    (hgen : ∀ a (ha : a ∈ s), f ⟨a, Algebra.subset_adjoin ha⟩ ∈ P)
    {n : ℕ} (hn : 0 < n) {b : A} (hb : b ∈ 𝒜 n) : b ∈ P := by
…

    Mentions: OAI.SourceSymmetry.A

  19. abbrev OAI.SourceSymmetry.S line 194
  20. abbrev OAI.SourceSymmetry.grading line 195
  21. def OAI.SourceSymmetry.normalizationInclusion line 197
  22. lemma OAI.SourceSymmetry.normalization_generator line 203
  23. lemma OAI.SourceSymmetry.normalizationInclusion_integral line 209
  24. lemma OAI.SourceSymmetry.homogeneous_integral_mem line 223
  25. lemma OAI.SourceSymmetry.exists_section_nonvanishing line 232
  26. lemma OAI.SourceSymmetry.section_linear_pow_add line 243
  27. lemma OAI.SourceSymmetry.section_linear_pow_sub line 251
  28. lemma OAI.SourceSymmetry.section_mem_of_good_mem line 259
  29. abbrev OAI.SourceSymmetry.GoodIndex line 284
  30. def OAI.SourceSymmetry.smoothOpen line 286
  31. lemma OAI.SourceSymmetry.smoothOpen_cover line 289