OAI/Geometry/Anticanonical/DeckRecovery.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Recovery of invariant anticanonical sections across unramified deck coverings.

  1. def OAI.DeckRecovery.productDiffeomorph line 26
  2. def OAI.DeckRecovery.translationDiffeomorph line 39
  3. def OAI.DeckRecovery.actionDiffeomorph line 48
  4. def OAI.DeckRecovery.doubleSplit line 72
  5. theorem OAI.DeckRecovery.contMDiff_doubleSplit line 78
  6. def OAI.DeckRecovery.splitFamily line 95
  7. theorem OAI.DeckRecovery.splitFamily_nonzero line 107
  8. theorem OAI.DeckRecovery.doubleSplit_natural line 127
  9. theorem OAI.DeckRecovery.splitFamily_equivariant line 150
  10. theorem OAI.DeckRecovery.hermitian_norm_preserving_inner line 169
  11. def OAI.DeckRecovery.monodromy line 191
  12. theorem OAI.DeckRecovery.native_deck_liouville_recovery line 197