OAI/NumberTheory/CubicMoment/Theta/CubicThetaQuotient.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The actual topological quotient by the principal level-three group. Proper discontinuity supplies Hausdorffness; the open quotient map preserves local compactness.

  1. instance OAI.CubicFirstMoment.cubicThetaPoint_locallyCompact line 12
  2. instance OAI.CubicFirstMoment.cubicThetaPrincipalPointAction_continuous line 15
  3. abbrev OAI.CubicFirstMoment.CubicThetaQuotient line 19
  4. def OAI.CubicFirstMoment.cubicThetaQuotientMap line 22
  5. lemma OAI.CubicFirstMoment.cubicThetaQuotientMap_open line 25
  6. instance OAI.CubicFirstMoment.cubicThetaQuotient_t2 line 28
  7. instance OAI.CubicFirstMoment.cubicThetaQuotient_locallyCompact line 30
  8. instance OAI.CubicFirstMoment.cubicThetaQuotient_secondCountable line 33
  9. lemma OAI.CubicFirstMoment.cubicThetaQuotientMap_surjective line 36