OAI/AlgebraicGeometry/LogKodaira/Basic.lean

GitHub source file

70 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ReverseLogKodaira.complexBase line 18

    Also declared: ComparatorChallenges/LogKodairaFiberNegative.lean:16 (same declaration text).

  2. abbrev OAI.ReverseLogKodaira.projectiveGrading line 20

    Also declared: ComparatorChallenges/LogKodairaFiberNegative.lean:18 (same declaration text).

  3. abbrev OAI.ReverseLogKodaira.complexProjectiveSpace line 22

    Also declared: ComparatorChallenges/LogKodairaFiberNegative.lean:20 (same declaration text).

  4. def OAI.ReverseLogKodaira.projectiveConstants line 24

    Also declared: ComparatorChallenges/LogKodairaFiberNegative.lean:22 (same declaration text).

  5. def OAI.ReverseLogKodaira.complexProjectiveStructure line 31

    Also declared: ComparatorChallenges/LogKodairaFiberNegative.lean:29 (same declaration text).

  6. structure OAI.ReverseLogKodaira.SmoothProjectiveVariety line 35

    Also declared: ComparatorChallenges/LogKodairaFiberNegative.lean:33 (same declaration text).

  7. instance OAI.ReverseLogKodaira.SmoothProjectiveVariety.(instance at line 48) line 48
  8. def OAI.ReverseLogKodaira.SmoothProjectiveVariety.globalConstants line 52

    Also declared: ComparatorChallenges/LogKodairaFiberNegative.lean:50 (same declaration text).

  9. def OAI.ReverseLogKodaira.SmoothProjectiveVariety.constants line 56

    Also declared: ComparatorChallenges/LogKodairaFiberNegative.lean:54 (same declaration text).

  10. instance OAI.ReverseLogKodaira.SmoothProjectiveVariety.(instance at line 59) line 59
  11. instance OAI.ReverseLogKodaira.SmoothProjectiveVariety.(instance at line 62) line 62
  12. def OAI.ReverseLogKodaira.SmoothProjectiveVariety.functionFieldConstants line 66

    Also declared: ComparatorChallenges/LogKodairaFiberNegative.lean:64 (same declaration text).

  13. instance OAI.ReverseLogKodaira.SmoothProjectiveVariety.(instance at line 69) line 69
  14. lemma OAI.ReverseLogKodaira.SmoothProjectiveVariety.germ_constants line 72

    Also declared: ComparatorChallenges/LogKodairaFiberNegative.lean:70 (same declaration text).

  15. instance OAI.ReverseLogKodaira.SmoothProjectiveVariety.(instance at line 80) line 80
  16. instance OAI.ReverseLogKodaira.SmoothProjectiveVariety.affineFiniteType line 84
  17. instance OAI.ReverseLogKodaira.SmoothProjectiveVariety.functionFieldFinTrdeg line 93
  18. lemma OAI.ReverseLogKodaira.SmoothProjectiveVariety.exists_standardSmooth_affine line 108
  19. lemma OAI.ReverseLogKodaira.SmoothProjectiveVariety.rank_rationalDifferentials line 129
  20. instance OAI.ReverseLogKodaira.SmoothProjectiveVariety.finite_rationalDifferentials line 146
  21. lemma OAI.ReverseLogKodaira.SmoothProjectiveVariety.finrank_rationalDifferentials line 150
  22. abbrev OAI.ReverseLogKodaira.SmoothProjectiveVariety.RationalCanonical line 156

    Also declared: ComparatorChallenges/LogKodairaFiberNegative.lean:82 (same declaration text).

  23. lemma OAI.ReverseLogKodaira.SmoothProjectiveVariety.finrank_rationalCanonical line 160
  24. abbrev OAI.ReverseLogKodaira.SmoothProjectiveVariety.RationalPluriform line 166

    Also declared: ComparatorChallenges/LogKodairaFiberNegative.lean:85 (same declaration text).

  25. instance OAI.ReverseLogKodaira.SmoothProjectiveVariety.(instance at line 169) line 169
  26. lemma OAI.ReverseLogKodaira.SmoothProjectiveVariety.nonempty_pluriformEquiv line 173
  27. lemma OAI.ReverseLogKodaira.SmoothProjectiveVariety.finrank_rationalPluriform line 180
  28. instance OAI.ReverseLogKodaira.SmoothProjectiveVariety.finite_rationalPluriform line 185
  29. instance OAI.ReverseLogKodaira.SmoothProjectiveVariety.nontrivial_rationalPluriform line 189
  30. def OAI.ReverseLogKodaira.SmoothProjectiveVariety.regularPluriformLattice line 195

    Also declared: ComparatorChallenges/LogKodairaFiberNegative.lean:91 (same declaration text).

  31. def OAI.ReverseLogKodaira.SmoothProjectiveVariety.IsCartierIdeal line 204

    Also declared: ComparatorChallenges/LogKodairaFiberNegative.lean:100 (same declaration text).

  32. lemma OAI.ReverseLogKodaira.SmoothProjectiveVariety.isCartierIdeal_one line 209
  33. structure OAI.ReverseLogKodaira.SmoothProjectiveVariety.ReducedSNCBoundary line 219

    Also declared: ComparatorChallenges/LogKodairaFiberNegative.lean:104 (same declaration text).

  34. def OAI.ReverseLogKodaira.SmoothProjectiveVariety.ReducedSNCBoundary.empty line 232
  35. def OAI.ReverseLogKodaira.SmoothProjectiveVariety.ReducedSNCBoundary.ideal line 243

    Also declared: ComparatorChallenges/LogKodairaFiberNegative.lean:116 (same declaration text).

  36. def OAI.ReverseLogKodaira.SmoothProjectiveVariety.ReducedSNCBoundary.support line 247

    Also declared: ComparatorChallenges/LogKodairaFiberNegative.lean:120 (same declaration text).

  37. lemma OAI.ReverseLogKodaira.SmoothProjectiveVariety.ReducedSNCBoundary.ideal_empty line 250
  38. lemma OAI.ReverseLogKodaira.SmoothProjectiveVariety.ReducedSNCBoundary.support_empty line 254
  39. def OAI.ReverseLogKodaira.SmoothProjectiveVariety.ReducedSNCBoundary.IsLogPluriform line 259

    Also declared: ComparatorChallenges/LogKodairaFiberNegative.lean:123 (same declaration text).

  40. lemma OAI.ReverseLogKodaira.SmoothProjectiveVariety.ReducedSNCBoundary.isLogPluriform_zero line 266

    Also declared: ComparatorChallenges/LogKodairaFiberNegative.lean:130 (same declaration text).

  41. lemma OAI.ReverseLogKodaira.SmoothProjectiveVariety.ReducedSNCBoundary.isLogPluriform_add line 271

    Also declared: ComparatorChallenges/LogKodairaFiberNegative.lean:135 (same declaration text).

  42. lemma OAI.ReverseLogKodaira.SmoothProjectiveVariety.ReducedSNCBoundary.isLogPluriform_smul line 278

    Also declared: ComparatorChallenges/LogKodairaFiberNegative.lean:142 (same declaration text).

  43. def OAI.ReverseLogKodaira.SmoothProjectiveVariety.ReducedSNCBoundary.sections line 289

    Also declared: ComparatorChallenges/LogKodairaFiberNegative.lean:153 (same declaration text).

  44. def OAI.ReverseLogKodaira.SmoothProjectiveVariety.ReducedSNCBoundary.HasImageDimensionAtLeast line 298

    Also declared: ComparatorChallenges/LogKodairaFiberNegative.lean:162 (same declaration text).

  45. def OAI.ReverseLogKodaira.SmoothProjectiveVariety.ReducedSNCBoundary.kodaira line 306

    Also declared: ComparatorChallenges/LogKodairaFiberNegative.lean:170 (same declaration text).

  46. lemma OAI.ReverseLogKodaira.SmoothProjectiveVariety.ReducedSNCBoundary.imageDimension_le_transcendenceDegree line 309
  47. lemma OAI.ReverseLogKodaira.SmoothProjectiveVariety.ReducedSNCBoundary.kodaira_le_transcendenceDegree line 317
  48. lemma OAI.ReverseLogKodaira.SmoothProjectiveVariety.ReducedSNCBoundary.kodaira_ne_top line 327
  49. lemma OAI.ReverseLogKodaira.SmoothProjectiveVariety.ReducedSNCBoundary.hasImageDimensionAtLeast_zero_iff line 333
  50. theorem OAI.ReverseLogKodaira.SmoothProjectiveVariety.ReducedSNCBoundary.kodaira_eq_bot_iff line 344
  51. structure OAI.ReverseLogKodaira.SmoothProjectiveVariety.ComplexPoint line 366

    Also declared: ComparatorChallenges/LogKodairaFiberNegative.lean:176 (same declaration text).

  52. def OAI.ReverseLogKodaira.SmoothProjectiveVariety.complexBasePoint line 371

    Also declared: ComparatorChallenges/LogKodairaFiberNegative.lean:181 (same declaration text).

  53. def OAI.ReverseLogKodaira.SmoothProjectiveVariety.ComplexPoint.point line 374

    Also declared: ComparatorChallenges/LogKodairaFiberNegative.lean:184 (same declaration text).

  54. def OAI.ReverseLogKodaira.SmoothProjectiveVariety.ReducedSNCBoundary.complement line 378

    Also declared: ComparatorChallenges/LogKodairaFiberNegative.lean:188 (same declaration text).

  55. structure OAI.ReverseLogKodaira.SmoothProjectiveVariety.BoundaryFibration line 383

    Also declared: ComparatorChallenges/LogKodairaFiberNegative.lean:193 (same declaration text).

  56. structure OAI.ReverseLogKodaira.SmoothProjectiveVariety.StratumSmoothFibration line 393

    Also declared: ComparatorChallenges/LogKodairaFiberNegative.lean:203 (same declaration text).

  57. structure OAI.ReverseLogKodaira.SmoothProjectiveVariety.FiberModel line 403

    Also declared: ComparatorChallenges/LogKodairaFiberNegative.lean:213 (same declaration text).

  58. def OAI.ReverseLogKodaira.SmoothProjectiveVariety.VeryGenerally line 413

    Also declared: ComparatorChallenges/LogKodairaFiberNegative.lean:223 (same declaration text).

  59. def OAI.ReverseLogKodaira.ReverseInequalityStatement line 423
  60. def OAI.ReverseLogKodaira.LogarithmicSubadditivityStatement line 435
  61. def OAI.ReverseLogKodaira.LogarithmicAdditivityStatement line 443
  62. def OAI.ReverseLogKodaira.MainTheoremStatement line 453
  63. theorem OAI.ReverseLogKodaira.SmoothProjectiveVariety.appLE_constants line 462
  64. lemma OAI.ReverseLogKodaira.SmoothProjectiveVariety.complexPoint_preimage_top line 484
  65. def OAI.ReverseLogKodaira.SmoothProjectiveVariety.complexPointEvaluation line 492
  66. def OAI.ReverseLogKodaira.SmoothProjectiveVariety.chartToFunctionField line 499
  67. lemma OAI.ReverseLogKodaira.SmoothProjectiveVariety.complexPointEvaluation_constants line 508
  68. lemma OAI.ReverseLogKodaira.SmoothProjectiveVariety.chartToFunctionField_constants line 527
  69. theorem OAI.ReverseLogKodaira.SmoothProjectiveVariety.fiber_scalar_compatibility line 541
  70. theorem OAI.ReverseLogKodaira.SmoothProjectiveVariety.fiber_chart_base_scalar line 558