OAI/Algebra/BogomolovPop/Canonical.lean

GitHub source file

79 declarations, 0 contain sorry, 0 declared as axioms

Canonical Galois transport, bracket compatibility and quotient-map well-definedness.

  1. instance OAI.BogomolovPop.PiA.nonarchimedean line 15
  2. instance OAI.BogomolovPop.additive_nonarchimedean line 19
  3. instance OAI.BogomolovPop.PiA.allLevelsEll line 25
  4. instance OAI.BogomolovPop.PiA.padicModule line 42
  5. instance OAI.BogomolovPop.PiA.padicContinuousSMul line 45
  6. instance OAI.BogomolovPop.PiA.additiveT2 line 48
  7. theorem OAI.BogomolovPop.PiA.continuous_linear line 51
  8. theorem OAI.BogomolovPop.scalarStep_iff_unit line 56
  9. theorem OAI.BogomolovPop.delta_commute line 70
  10. instance OAI.BogomolovPop.Delta.commGroup line 81
  11. theorem OAI.BogomolovPop.centralProjection_continuous line 85
  12. instance OAI.BogomolovPop.Delta.compactSpace line 90
  13. instance OAI.BogomolovPop.PiC.nonarchimedean line 95
  14. instance OAI.BogomolovPop.Delta.nonarchimedean line 98
  15. theorem OAI.BogomolovPop.PiC.pow_tendsto_one line 105
  16. theorem OAI.BogomolovPop.Delta.pow_tendsto_one line 113
  17. instance OAI.BogomolovPop.Delta.allLevelsEll line 118
  18. instance OAI.BogomolovPop.Delta.additiveT2 line 134
  19. instance OAI.BogomolovPop.Delta.padicModule line 137
  20. instance OAI.BogomolovPop.Delta.padicContinuousSMul line 140
  21. theorem OAI.BogomolovPop.Delta.continuous_linear line 143
  22. theorem OAI.BogomolovPop.map_sourceCommutator line 148
  23. theorem OAI.BogomolovPop.sourceCommutator_mul_left_of_central line 153
  24. theorem OAI.BogomolovPop.bracket_on_lifts line 164
  25. theorem OAI.BogomolovPop.bracket_mul_left line 169
  26. theorem OAI.BogomolovPop.bracket_swap line 188
  27. theorem OAI.BogomolovPop.bracket_mul_right line 197
  28. theorem OAI.BogomolovPop.bracket_alternating line 202
  29. theorem OAI.BogomolovPop.bracket_one_left line 208
  30. theorem OAI.BogomolovPop.bracket_continuous line 214
  31. def OAI.BogomolovPop.bracketLeftHom line 226
  32. theorem OAI.BogomolovPop.bracket_smul_left line 232
  33. def OAI.BogomolovPop.bracketRightHom line 239
  34. theorem OAI.BogomolovPop.bracket_smul_right line 245
  35. def OAI.BogomolovPop.unitScalarEquiv line 252
  36. theorem OAI.BogomolovPop.unitScalarEquiv_apply line 263
  37. def OAI.BogomolovPop.scalarIsomC line 268
  38. theorem OAI.BogomolovPop.scalarStep_equivalence line 281
  39. theorem OAI.BogomolovPop.scalarEqvGen_iff line 297
  40. theorem OAI.BogomolovPop.quotient_comap_map_injective line 307
  41. theorem OAI.BogomolovPop.proEllKernel_map_le line 318
  42. theorem OAI.BogomolovPop.continuous_quotientMap line 335
  43. theorem OAI.BogomolovPop.closedCommutator_map_le line 342
  44. theorem OAI.BogomolovPop.closedGammaThree_map_le line 356
  45. def OAI.BogomolovPop.quotientContinuousEquiv line 370
  46. def OAI.BogomolovPop.proEllContinuousEquiv line 389
  47. def OAI.BogomolovPop.abelianContinuousEquiv line 395
  48. def OAI.BogomolovPop.centralContinuousEquiv line 402
  49. theorem OAI.BogomolovPop.isAlgClosure_perfectClosure line 415
  50. def OAI.BogomolovPop.extendPerfectEquiv line 421
  51. theorem OAI.BogomolovPop.extendPerfectEquiv_spec line 428
  52. theorem OAI.BogomolovPop.perfectClosure_fixed line 435
  53. def OAI.BogomolovPop.absoluteConjugate line 442
  54. theorem OAI.BogomolovPop.absoluteConjugate_apply line 458
  55. theorem OAI.BogomolovPop.perfectExtension_symm line 465
  56. def OAI.BogomolovPop.absoluteConjugateEquiv line 474
  57. theorem OAI.BogomolovPop.absoluteConjugate_continuous line 486
  58. def OAI.BogomolovPop.absoluteConjugateContinuousEquiv line 519
  59. theorem OAI.BogomolovPop.centralProjection_natural line 534
  60. def OAI.BogomolovPop.deltaContinuousEquiv line 540
  61. theorem OAI.BogomolovPop.induced_bracketCompatible line 558
  62. def OAI.BogomolovPop.isomCOfExtension line 575
  63. theorem OAI.BogomolovPop.pullbackGraph_of_extension line 583
  64. theorem OAI.BogomolovPop.exists_pullbackGraph line 594
  65. theorem OAI.BogomolovPop.absoluteToPiA_surjective line 604
  66. def OAI.BogomolovPop.extensionDifference line 608
  67. theorem OAI.BogomolovPop.absoluteConjugate_extensionDifference line 622
  68. theorem OAI.BogomolovPop.isomCOfExtension_eq line 635
  69. theorem OAI.BogomolovPop.pullbackGraph_eq_extension line 651
  70. theorem OAI.BogomolovPop.existsUnique_pullbackGraph line 672
  71. def OAI.BogomolovPop.canonicalPullback line 684
  72. theorem OAI.BogomolovPop.canonicalPullback_spec line 689
  73. theorem OAI.BogomolovPop.canonicalPullback_frobenius line 694
  74. theorem OAI.BogomolovPop.canonicalPullback_eq_of_frobeniusOrbit line 727
  75. def OAI.BogomolovPop.canonicalPhi line 738
  76. theorem OAI.BogomolovPop.canonicalPhi_graph line 745
  77. theorem OAI.BogomolovPop.phiGraph_eq_canonicalPhi line 751
  78. theorem OAI.BogomolovPop.main_wellDefined line 760
  79. theorem OAI.BogomolovPop.main_canonical_wellDefined line 771