OAI/Topology/CoarseAssembly/CongruenceEdgeOperators.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The concrete one-step congruence-fiber operators

The normalized child map is now instantiated with the proved surjective congruence reduction. Its adjoint and the equal-depth permutations preserve constants and have coefficients supported precisely on the prescribed right-holonomy edge relation.

  1. def OAI.CoarseAssembly.Congruence.childIsometry line 18
  2. theorem OAI.CoarseAssembly.Congruence.childIsometry_constant line 24
  3. theorem OAI.CoarseAssembly.Congruence.childAdjoint_constant line 30
  4. theorem OAI.CoarseAssembly.Congruence.childIsometry_support line 36
  5. theorem OAI.CoarseAssembly.Congruence.childAdjoint_support line 53
  6. def OAI.CoarseAssembly.Congruence.sameLevelIsometry line 64
  7. theorem OAI.CoarseAssembly.Congruence.sameLevelIsometry_constant line 68
  8. theorem OAI.CoarseAssembly.Congruence.sameLevelIsometry_support line 72