OAI/Algebra/BogomolovPop/Foundations.lean

GitHub source file

77 declarations, 0 contain sorry, 0 declared as axioms

Literal Galois objects, quotient topology and continuous ell-adic actions.

  1. def OAI.BogomolovPop.proEllKernel line 13

    Also declared: ComparatorChallenges/BogomolovPopInjectivity.lean:8 (same declaration text).

  2. instance OAI.BogomolovPop.proEllKernel_normal line 16

    Also declared: ComparatorChallenges/BogomolovPopInjectivity.lean:11 (same declaration text).

  3. abbrev OAI.BogomolovPop.ProEll line 22

    Also declared: ComparatorChallenges/BogomolovPopInjectivity.lean:17 (same declaration text).

  4. def OAI.BogomolovPop.closedGammaThree line 25

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

  5. instance OAI.BogomolovPop.closedGammaThree_normal line 29

    Also declared: ComparatorChallenges/BogomolovPopInjectivity.lean:24 (same declaration text).

  6. abbrev OAI.BogomolovPop.PiA line 34

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

  7. abbrev OAI.BogomolovPop.PiC line 36

    Also declared: ComparatorChallenges/BogomolovPopInjectivity.lean:31 (same declaration text).

  8. theorem OAI.BogomolovPop.closedGammaThree_le line 38

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

  9. def OAI.BogomolovPop.centralProjection line 43

    Also declared: ComparatorChallenges/BogomolovPopInjectivity.lean:38 (same declaration text).

  10. abbrev OAI.BogomolovPop.Delta line 46

    Also declared: ComparatorChallenges/BogomolovPopInjectivity.lean:41 (same declaration text).

  11. def OAI.BogomolovPop.sourceCommutator line 48

    Also declared: ComparatorChallenges/BogomolovPopInjectivity.lean:43 (same declaration text).

  12. def OAI.BogomolovPop.abelianLift line 50

    Also declared: ComparatorChallenges/BogomolovPopInjectivity.lean:45 (same declaration text).

  13. theorem OAI.BogomolovPop.abelianLift_spec line 53

    Also declared: ComparatorChallenges/BogomolovPopInjectivity.lean:48 (same declaration text).

  14. def OAI.BogomolovPop.bracket line 56

    Also declared: ComparatorChallenges/BogomolovPopInjectivity.lean:51 (same declaration text).

  15. def OAI.BogomolovPop.BracketCompatible line 62

    Also declared: ComparatorChallenges/BogomolovPopInjectivity.lean:57 (same declaration text).

  16. abbrev OAI.BogomolovPop.PerfectFieldClosure line 67

    Also declared: ComparatorChallenges/BogomolovPopInjectivity.lean:62 (same declaration text).

  17. def OAI.BogomolovPop.PerfectIsom line 69

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

  18. def OAI.BogomolovPop.FrobeniusStep line 75

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

  19. abbrev OAI.BogomolovPop.IsomF line 80

    Also declared: ComparatorChallenges/BogomolovPopInjectivity.lean:75 (same declaration text).

  20. abbrev OAI.BogomolovPop.IsomC line 84

    Also declared: ComparatorChallenges/BogomolovPopInjectivity.lean:79 (same declaration text).

  21. def OAI.BogomolovPop.ScalarStep line 87

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

  22. abbrev OAI.BogomolovPop.IsomCUnits line 93

    Also declared: ComparatorChallenges/BogomolovPopInjectivity.lean:88 (same declaration text).

  23. def OAI.BogomolovPop.absoluteToPiA line 96

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

  24. def OAI.BogomolovPop.absoluteAction line 100

    Also declared: ComparatorChallenges/BogomolovPopInjectivity.lean:95 (same declaration text).

  25. def OAI.BogomolovPop.PullbackGraph line 105

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

  26. def OAI.BogomolovPop.PhiGraph line 116

    Also declared: ComparatorChallenges/BogomolovPopInjectivity.lean:111 (same declaration text).

  27. def OAI.BogomolovPop.MainStatement line 122
  28. theorem OAI.BogomolovPop.closedCommutator_image_commute line 136
  29. theorem OAI.BogomolovPop.quotient_commutator_independent line 147
  30. theorem OAI.BogomolovPop.sourceCommutator_independent line 178
  31. theorem OAI.BogomolovPop.bracket_eq_of_lifts line 195
  32. theorem OAI.BogomolovPop.quotient_nonarchimedean line 203
  33. theorem OAI.BogomolovPop.proEllKernel_isClosed line 219
  34. theorem OAI.BogomolovPop.restrictScalarsHom_continuous line 224
  35. theorem OAI.BogomolovPop.restrictScalarsHom_surjective_of_purelyInseparable line 254
  36. theorem OAI.BogomolovPop.absoluteGaloisGroup_compact line 265
  37. theorem OAI.BogomolovPop.absoluteGaloisGroup_nonarchimedean line 278
  38. instance OAI.BogomolovPop.(instance at line 286) line 286
  39. instance OAI.BogomolovPop.(instance at line 289) line 289
  40. instance OAI.BogomolovPop.(instance at line 292) line 292
  41. instance OAI.BogomolovPop.ProEll.t2Space line 296
  42. instance OAI.BogomolovPop.ProEll.totallyDisconnectedSpace line 300
  43. instance OAI.BogomolovPop.PiA.t2Space line 305
  44. instance OAI.BogomolovPop.PiA.totallyDisconnectedSpace line 309
  45. instance OAI.BogomolovPop.PiC.t2Space line 314
  46. instance OAI.BogomolovPop.PiC.totallyDisconnectedSpace line 319
  47. def OAI.BogomolovPop.EllQuotients line 326
  48. instance OAI.BogomolovPop.ellQuotient_normal line 329
  49. theorem OAI.BogomolovPop.proEllKernel_le line 332
  50. def OAI.BogomolovPop.proEllEval line 336
  51. theorem OAI.BogomolovPop.proEllEval_injective line 340
  52. theorem OAI.BogomolovPop.proEllEval_continuous line 352
  53. theorem OAI.BogomolovPop.proEllEval_isClosedEmbedding line 359
  54. theorem OAI.BogomolovPop.proEll_pow_tendsto_one line 366
  55. theorem OAI.BogomolovPop.isPGroup_of_proEll_image line 382
  56. theorem OAI.BogomolovPop.continuous_padic_toZModPow line 398
  57. theorem OAI.BogomolovPop.finite_abelian_ell_exponent line 412
  58. abbrev OAI.BogomolovPop.finiteEllModule line 417
  59. theorem OAI.BogomolovPop.finiteEllModule_continuous line 423
  60. abbrev OAI.BogomolovPop.AllLevels line 437
  61. instance OAI.BogomolovPop.levelDiscrete line 440
  62. instance OAI.BogomolovPop.levelFinite line 443
  63. def OAI.BogomolovPop.levelEval line 446
  64. theorem OAI.BogomolovPop.levelEval_injective line 450
  65. theorem OAI.BogomolovPop.levelEval_continuous line 462
  66. theorem OAI.BogomolovPop.levelEval_closedEmbedding line 465
  67. def OAI.BogomolovPop.AllLevelsEll line 469
  68. instance OAI.BogomolovPop.levelsModule line 474
  69. theorem OAI.BogomolovPop.levels_continuous line 479
  70. def OAI.BogomolovPop.levelImage line 484
  71. def OAI.BogomolovPop.levelImageEquiv line 496
  72. abbrev OAI.BogomolovPop.abelianEllModule line 505
  73. theorem OAI.BogomolovPop.levelEval_smul line 508
  74. theorem OAI.BogomolovPop.abelianEllModule_continuous line 515
  75. theorem OAI.BogomolovPop.padic_appr_tendsto line 528
  76. theorem OAI.BogomolovPop.continuous_addHom_padic_linear line 541
  77. theorem OAI.BogomolovPop.padic_appr_smul_tendsto line 553