OAI/Topology/CoarseAssembly/CongruenceSurjective.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Surjectivity of the successive special-linear reductions

Lift the entries arbitrarily. The lifted determinant is odd, hence a unit; rescaling one row by its inverse corrects the determinant without changing the reduction. Level zero is handled by its singleton group.

  1. theorem OAI.CoarseAssembly.Congruence.residueMap_comp line 14
  2. theorem OAI.CoarseAssembly.Congruence.isUnit_of_residue_one line 20
  3. theorem OAI.CoarseAssembly.Congruence.quotientMap_successor_surjective line 32