OAI/Geometry/NilpotentCharts/LatticeQuotients.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Discrete projected lattices and compact quotient fibers.

  1. lemma OAI.RawLatticeProjection.commutator_mul_central line 15
  2. theorem OAI.RawLatticeProjection.discrete_map line 26
  3. lemma OAI.RawLatticeFiber.compact_surjecting_set line 80
  4. theorem OAI.RawLatticeFiber.compact_fiber line 101
  5. lemma OAI.RawLatticeFiber.compact_quotient_image line 158
  6. theorem OAI.RawLatticeFiber.discrete_quotient_of_compact_kernel line 184