OAI/Algebra/BogomolovPop/Kummer.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

Tate bases, Kummer characters and scalar conjugation.

  1. instance OAI.BogomolovPop.finiteRootsTopology line 15
  2. instance OAI.BogomolovPop.finiteRootsDiscrete line 17
  3. def OAI.BogomolovPop.rootTransition line 21
  4. def OAI.BogomolovPop.tateModuleGroup line 30
  5. abbrev OAI.BogomolovPop.TateModule line 37
  6. abbrev OAI.BogomolovPop.PrimitiveLevel line 44
  7. lemma OAI.BogomolovPop.primitiveLevel_nonempty line 47
  8. def OAI.BogomolovPop.primitiveDown line 60
  9. lemma OAI.BogomolovPop.primitiveDown_self line 66
  10. lemma OAI.BogomolovPop.primitiveDown_comp line 72
  11. theorem OAI.BogomolovPop.exists_compatible_primitive line 82
  12. def OAI.BogomolovPop.zmodRootEquiv line 112
  13. lemma OAI.BogomolovPop.zmodRootEquiv_nat line 118
  14. lemma OAI.BogomolovPop.zmodRootEquiv_val line 124
  15. lemma OAI.BogomolovPop.zmodRootEquiv_transition line 128
  16. theorem OAI.BogomolovPop.root_continuous_padic_toZModPow line 152
  17. def OAI.BogomolovPop.padicToTate line 170
  18. lemma OAI.BogomolovPop.padicToTate_continuous line 189
  19. lemma OAI.BogomolovPop.padicToTate_injective line 199
  20. lemma OAI.BogomolovPop.padicToTate_surjective line 209
  21. def OAI.BogomolovPop.tateBasisEquiv line 229
  22. lemma OAI.BogomolovPop.root_scalar_exists line 244
  23. theorem OAI.BogomolovPop.closure_root_scalar line 272
  24. theorem OAI.BogomolovPop.torsion_is_constant line 315
  25. theorem OAI.BogomolovPop.fixed_separable_mem_base line 323
  26. theorem OAI.BogomolovPop.galois_fixes_torsion line 340
  27. def OAI.BogomolovPop.kummerRoot line 346
  28. theorem OAI.BogomolovPop.kummerRoot_pow line 355
  29. def OAI.BogomolovPop.kummerRatio line 360
  30. theorem OAI.BogomolovPop.ratio_eq_of_pow_eq line 372
  31. def OAI.BogomolovPop.kummerCharacter line 385
  32. theorem OAI.BogomolovPop.kummerCharacter_apply_of_root line 407
  33. def OAI.BogomolovPop.kummerPairing line 414
  34. theorem OAI.BogomolovPop.kummerRoot_isSeparable line 435
  35. theorem OAI.BogomolovPop.kummerPairing_eq_one_iff line 440
  36. theorem OAI.BogomolovPop.kummerCharacter_eq_one_iff line 464
  37. theorem OAI.BogomolovPop.kummerCharacter_ker_isOpen line 479
  38. theorem OAI.BogomolovPop.kummerCharacter_continuous line 491
  39. theorem OAI.BogomolovPop.kummerCharacter_proEllKernel line 502
  40. def OAI.BogomolovPop.kummerProEll line 518
  41. theorem OAI.BogomolovPop.kummerProEll_continuous line 523
  42. theorem OAI.BogomolovPop.kummerProEll_closedCommutator line 528
  43. def OAI.BogomolovPop.kummerPiA line 535
  44. theorem OAI.BogomolovPop.kummerPiA_continuous line 540
  45. theorem OAI.BogomolovPop.kummerPiA_absolute line 546
  46. theorem OAI.BogomolovPop.kummerPiA_eq_one_iff line 551
  47. lemma OAI.BogomolovPop.torsion_appr_eventually line 571
  48. lemma OAI.BogomolovPop.kummerPiA_scalar_limit line 581
  49. lemma OAI.BogomolovPop.kummerPiA_pairing_mul line 597
  50. def OAI.BogomolovPop.kummerPiAPairing line 604
  51. lemma OAI.BogomolovPop.kummerPiA_class_eq line 614
  52. theorem OAI.BogomolovPop.conjugation_kummer_scalar line 624