OAI/Geometry/Anticanonical/BranchedQuotient.lean

GitHub source file

204 declarations, 0 contain sorry, 0 declared as axioms

Branched sphere quotients and obstructions to holomorphic lifts.

  1. structure OAI.QuotientLift.SphereTangentSection line 16
  2. lemma OAI.QuotientLift.twice_dslope_differentiable line 23
  3. theorem OAI.QuotientLift.section_polynomial line 29
  4. theorem OAI.QuotientLift.invariant_section_zero line 70
  5. def OAI.QuotientLift.quotientCoordinate line 89
  6. theorem OAI.QuotientLift.quotient_fibers line 91
  7. theorem OAI.QuotientLift.quotient_surjective_finite line 105
  8. theorem OAI.QuotientLift.no_anticanonical_lift line 128
  9. def OAI.QuotientLift.constantAffineSection line 142
  10. theorem OAI.QuotientLift.downstairs_nonzero line 149
  11. def OAI.QuotientLift.signSection line 153
  12. def OAI.QuotientLift.inversionSection line 161
  13. def OAI.QuotientLift.coefficients line 170
  14. def OAI.QuotientLift.sectionHermitian line 174
  15. theorem OAI.QuotientLift.coefficients_injective line 177
  16. lemma OAI.QuotientLift.sign_coefficients line 205
  17. lemma OAI.QuotientLift.inversion_coefficients line 216
  18. theorem OAI.QuotientLift.sign_preserves_Hermitian line 229
  19. theorem OAI.QuotientLift.inversion_preserves_Hermitian line 235
  20. abbrev OAI.QuotientLift.Sphere line 244
  21. def OAI.QuotientLift.inversionPoint line 248
  22. theorem OAI.QuotientLift.inversionPoint_involutive line 252
  23. theorem OAI.QuotientLift.inversionPoint_continuous line 261
  24. def OAI.QuotientLift.inversionHomeomorph line 299
  25. lemma OAI.QuotientLift.inversionHomeomorph_apply line 307
  26. def OAI.QuotientLift.affineChart line 310
  27. def OAI.QuotientLift.infinityChart line 313
  28. lemma OAI.QuotientLift.affineChart_source line 316
  29. lemma OAI.QuotientLift.affineChart_target line 319
  30. lemma OAI.QuotientLift.affineChart_coe line 322
  31. lemma OAI.QuotientLift.affineChart_symm line 325
  32. instance OAI.QuotientLift.sphereChartedSpace line 328
  33. lemma OAI.QuotientLift.infinityChart_source line 341
  34. lemma OAI.QuotientLift.infinityChart_target line 350
  35. lemma OAI.QuotientLift.infinityChart_symm line 353
  36. lemma OAI.QuotientLift.infinityChart_coe line 358
  37. lemma OAI.QuotientLift.infinityChart_infty line 363
  38. lemma OAI.QuotientLift.chart_self_contDiff line 367
  39. lemma OAI.QuotientLift.affine_infinity_contDiff line 373
  40. lemma OAI.QuotientLift.infinity_affine_contDiff line 385
  41. theorem OAI.QuotientLift.sphere_is_complex_manifold line 399
  42. def OAI.QuotientLift.signPoint line 414
  43. def OAI.QuotientLift.quotientPoint line 416
  44. theorem OAI.QuotientLift.quotientPoint_fibers line 420
  45. theorem OAI.QuotientLift.quotientPoint_surjective line 444
  46. theorem OAI.QuotientLift.sphere_compact_connected line 452
  47. lemma OAI.QuotientLift.quotientPoint_inversion line 455
  48. def OAI.QuotientLift.reciprocalQuotientCoordinate line 463
  49. lemma OAI.QuotientLift.quotientPoint_reciprocal line 465
  50. lemma OAI.QuotientLift.reciprocalQuotientCoordinate_contDiffAt line 476
  51. lemma OAI.QuotientLift.denominator_near_zero line 481
  52. lemma OAI.QuotientLift.quotientPoint_coe_continuous line 484
  53. theorem OAI.QuotientLift.quotientPoint_continuous line 502
  54. theorem OAI.QuotientLift.quotientPoint_isQuotientMap line 514
  55. lemma OAI.QuotientLift.sphere_chartAt_infty line 517
  56. lemma OAI.QuotientLift.sphere_chartAt_coe line 521
  57. lemma OAI.QuotientLift.infinityChart_inversion_coe line 525
  58. lemma OAI.QuotientLift.sphere_analyticAt_of_chart line 531
  59. theorem OAI.QuotientLift.quotientPoint_analytic line 543
  60. def OAI.QuotientLift.polynomialSection line 570
  61. lemma OAI.QuotientLift.polynomialSection_coefficients line 580
  62. theorem OAI.QuotientLift.coefficients_surjective line 586
  63. def OAI.QuotientLift.coefficientEquiv line 589
  64. instance OAI.QuotientLift.sectionAddCommGroup line 593
  65. instance OAI.QuotientLift.sectionModule line 594
  66. def OAI.QuotientLift.coefficientLinearEquiv line 596
  67. instance OAI.QuotientLift.sectionNormedAddCommGroup line 599
  68. instance OAI.QuotientLift.sectionInnerProductSpace line 603
  69. theorem OAI.QuotientLift.section_inner line 606
  70. theorem OAI.QuotientLift.sign_preserves_norm line 613
  71. theorem OAI.QuotientLift.inversion_preserves_norm line 617
  72. lemma OAI.QuotientLift.coefficients_zero line 621
  73. lemma OAI.QuotientLift.zero_affine line 625
  74. lemma OAI.QuotientLift.zero_infinity line 632
  75. theorem OAI.QuotientLift.constantAffineSection_ne_zero line 639
  76. theorem OAI.QuotientLift.invariant_section_eq_zero line 644
  77. lemma OAI.QuotientLift.signPoint_involutive line 656
  78. lemma OAI.QuotientLift.inversion_signPoint line 660
  79. lemma OAI.QuotientLift.signSection_involutive line 667
  80. lemma OAI.QuotientLift.inversionSection_involutive line 673
  81. lemma OAI.QuotientLift.inversion_signSection line 678
  82. lemma OAI.QuotientLift.inversionPoint_analytic line 683
  83. lemma OAI.QuotientLift.signPoint_continuous line 711
  84. lemma OAI.QuotientLift.infinityChart_sign_inversion line 714
  85. lemma OAI.QuotientLift.signPoint_analytic line 720
  86. abbrev OAI.QuotientLift.Klein line 742
  87. def OAI.QuotientLift.sphereAct line 744
  88. def OAI.QuotientLift.sectionAct line 748
  89. lemma OAI.QuotientLift.zmod_two_cases line 752
  90. instance OAI.QuotientLift.kleinSphereAction line 756
  91. instance OAI.QuotientLift.kleinSectionAction line 775
  92. theorem OAI.QuotientLift.sphereAct_analytic line 794
  93. theorem OAI.QuotientLift.sectionAct_preserves_norm line 805
  94. lemma OAI.QuotientLift.coefficients_add line 810
  95. lemma OAI.QuotientLift.coefficients_smul line 814
  96. lemma OAI.QuotientLift.signSection_add line 818
  97. lemma OAI.QuotientLift.inversionSection_add line 824
  98. lemma OAI.QuotientLift.signSection_smul line 830
  99. lemma OAI.QuotientLift.inversionSection_smul line 836
  100. theorem OAI.QuotientLift.sectionAct_add line 842
  101. theorem OAI.QuotientLift.sectionAct_smul line 847
  102. theorem OAI.QuotientLift.quotientPoint_orbits line 852
  103. theorem OAI.QuotientLift.no_nonzero_invariant_section line 865
  104. theorem OAI.QuotientLift.klein_action_not_free line 873
  105. def OAI.QuotientLift.sectionValue line 882
  106. lemma OAI.QuotientLift.affineChart_comp_symm line 887
  107. lemma OAI.QuotientLift.infinityChart_comp_symm line 891
  108. lemma OAI.QuotientLift.tangent_triv_affine line 895
  109. lemma OAI.QuotientLift.tangent_triv_infty line 901
  110. lemma OAI.QuotientLift.tangent_triv_infty_coe line 907
  111. def OAI.QuotientLift.tangentCoordinates line 923
  112. lemma OAI.QuotientLift.tangentCoordinates_affine line 926
  113. lemma OAI.QuotientLift.tangentCoordinates_infty line 929
  114. lemma OAI.QuotientLift.tangentCoordinates_infty_coe line 932
  115. lemma OAI.QuotientLift.tangent_section_infty_chart line 935
  116. lemma OAI.QuotientLift.sphere_to_complex_analyticAt_iff line 946
  117. theorem OAI.QuotientLift.sectionValue_analytic line 955
  118. abbrev OAI.QuotientLift.HolomorphicVectorField line 980
  119. def OAI.QuotientLift.toTangentSection line 983
  120. lemma OAI.QuotientLift.infinityChart_symm_analytic line 986
  121. def OAI.QuotientLift.nativeValue line 993
  122. def OAI.QuotientLift.affineCoefficient line 995
  123. def OAI.QuotientLift.infinityCoefficient line 997
  124. lemma OAI.QuotientLift.affineCoefficient_holomorphic line 1000
  125. lemma OAI.QuotientLift.infinityCoefficient_holomorphic line 1015
  126. def OAI.QuotientLift.fromTangentSection line 1027
  127. lemma OAI.QuotientLift.SphereTangentSection.ext line 1037
  128. lemma OAI.QuotientLift.section_eq_polynomial line 1045
  129. lemma OAI.QuotientLift.affine_as_coefficients line 1050
  130. lemma OAI.QuotientLift.infinity_as_coefficients line 1055
  131. lemma OAI.QuotientLift.affine_add line 1061
  132. lemma OAI.QuotientLift.infinity_add line 1066
  133. lemma OAI.QuotientLift.affine_smul line 1071
  134. lemma OAI.QuotientLift.infinity_smul line 1076
  135. lemma OAI.QuotientLift.from_toTangentSection line 1081
  136. lemma OAI.QuotientLift.to_fromTangentSection line 1089
  137. theorem OAI.QuotientLift.toTangentSection_bijective line 1100
  138. theorem OAI.QuotientLift.toTangentSection_add line 1104
  139. theorem OAI.QuotientLift.toTangentSection_smul line 1112
  140. def OAI.QuotientLift.tangentSectionLinearEquiv line 1120
  141. def OAI.QuotientLift.sphereDerivative line 1127
  142. lemma OAI.QuotientLift.sphereDerivative_chart line 1130
  143. lemma OAI.QuotientLift.sphereDerivative_sign line 1140
  144. lemma OAI.QuotientLift.sphereDerivative_inversion_infty line 1167
  145. lemma OAI.QuotientLift.sphereDerivative_inversion_zero line 1179
  146. lemma OAI.QuotientLift.sphereDerivative_inversion_coe line 1191
  147. def OAI.QuotientLift.chartValue line 1203
  148. lemma OAI.QuotientLift.sign_action_natural line 1205
  149. lemma OAI.QuotientLift.inversion_action_natural line 1210
  150. lemma OAI.QuotientLift.sphereDerivative_comp line 1224
  151. theorem OAI.QuotientLift.tangent_action_natural line 1231
  152. theorem OAI.QuotientLift.no_nonzero_invariant_holomorphic_vectorfield line 1255
  153. instance OAI.QuotientLift.nativeNormedAddCommGroup line 1273
  154. instance OAI.QuotientLift.nativeInnerProductSpace line 1277
  155. def OAI.QuotientLift.nativeSectionAct line 1280
  156. theorem OAI.QuotientLift.nativeSectionAct_preserves_norm line 1283
  157. theorem OAI.QuotientLift.native_downstairs_nonzero line 1290
  158. lemma OAI.QuotientLift.quotientCoordinate_derivative_one line 1295
  159. lemma OAI.QuotientLift.sphereDerivative_quotient_one line 1302
  160. theorem OAI.QuotientLift.native_no_anticanonical_lift line 1313
  161. abbrev OAI.QuotientLift.AnticanonicalFiber line 1325
  162. def OAI.QuotientLift.determinantValue line 1327
  163. def OAI.QuotientLift.IsHolomorphicDeterminantSection line 1330
  164. theorem OAI.QuotientLift.downstairs_anticanonical_section line 1334
  165. theorem OAI.QuotientLift.no_nonzero_invariant_anticanonical_section line 1353
  166. lemma OAI.QuotientLift.nativeSectionAct_equiv line 1378
  167. def OAI.QuotientLift.determinantSectionMap line 1387
  168. theorem OAI.QuotientLift.determinantSectionMap_injective line 1397
  169. abbrev OAI.QuotientLift.AnticanonicalSections line 1403
  170. def OAI.QuotientLift.anticanonicalSectionEquiv line 1405
  171. theorem OAI.QuotientLift.mem_anticanonicalSections_iff line 1408
  172. instance OAI.QuotientLift.anticanonicalNormedAddCommGroup line 1420
  173. instance OAI.QuotientLift.anticanonicalInnerProductSpace line 1424
  174. def OAI.QuotientLift.anticanonicalSectionAct line 1427
  175. theorem OAI.QuotientLift.anticanonicalSectionAct_preserves_norm line 1430
  176. theorem OAI.QuotientLift.anticanonicalSectionAct_natural line 1437
  177. theorem OAI.QuotientLift.anticanonicalSectionAct_one line 1458
  178. theorem OAI.QuotientLift.anticanonicalSectionAct_mul line 1465
  179. theorem OAI.QuotientLift.branched_quotient_anticanonical_obstruction line 1477
  180. abbrev OAI.QuotientLift.ZeroComplex line 1498
  181. abbrev OAI.QuotientLift.SplitModel line 1499
  182. abbrev OAI.QuotientLift.SplitSpace line 1500
  183. def OAI.QuotientLift.translation line 1502
  184. def OAI.QuotientLift.productAct line 1504
  185. def OAI.QuotientLift.productQuotient line 1507
  186. instance OAI.QuotientLift.zeroTranslationLattice line 1509
  187. theorem OAI.QuotientLift.translation_range line 1513
  188. theorem OAI.QuotientLift.productAct_one line 1523
  189. theorem OAI.QuotientLift.productAct_mul line 1530
  190. theorem OAI.QuotientLift.productAct_analytic line 1538
  191. theorem OAI.QuotientLift.productQuotient_analytic line 1550
  192. theorem OAI.QuotientLift.productQuotient_isQuotientMap line 1555
  193. theorem OAI.QuotientLift.productQuotient_orbits line 1562
  194. abbrev OAI.QuotientLift.ZeroCanonicalFiber line 1573
  195. def OAI.QuotientLift.zeroCanonicalFrame line 1576
  196. theorem OAI.QuotientLift.zeroCanonicalFrame_nowhere_zero line 1579
  197. theorem OAI.QuotientLift.zeroCanonicalFrame_holomorphic line 1584
  198. theorem OAI.QuotientLift.zeroCanonicalFrame_invariant line 1591
  199. theorem OAI.QuotientLift.literal_product_quotient_data line 1602
  200. theorem OAI.QuotientLift.anticanonicalSectionAct_add line 1615
  201. theorem OAI.QuotientLift.anticanonicalSectionAct_smul line 1624
  202. def OAI.QuotientLift.anticanonicalMonodromy line 1632
  203. theorem OAI.QuotientLift.no_monodromy_invariant_anticanonical_section line 1646
  204. theorem OAI.QuotientLift.literal_source_instance_obstruction line 1652