OAI/Topology/CoarseAssembly/FiniteFiberMaps.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Permutations and normalized quotient-copying maps

These are the two types of edge operator in the graph construction: permutations at equal depth, and normalized copying along a surjective finite-group quotient. Their norm and constant-vector properties are proved on the actual finite-fiber Hilbert spaces.

  1. def OAI.CoarseAssembly.reindexFiberVector line 20
  2. theorem OAI.CoarseAssembly.reindexFiber_norm line 24
  3. def OAI.CoarseAssembly.reindexFiber line 31
  4. theorem OAI.CoarseAssembly.reindexFiber_apply line 40
  5. theorem OAI.CoarseAssembly.reindexFiber_constant line 43
  6. def OAI.CoarseAssembly.quotientSection line 53
  7. theorem OAI.CoarseAssembly.quotientSection_spec line 56
  8. def OAI.CoarseAssembly.quotientFiberEquiv line 59
  9. def OAI.CoarseAssembly.quotientCopy line 71
  10. theorem OAI.CoarseAssembly.quotientCopy_apply line 77
  11. theorem OAI.CoarseAssembly.quotientCopy_constant line 81
  12. theorem OAI.CoarseAssembly.quotientCopy_adjoint_constant line 94
  13. def OAI.CoarseAssembly.twistedQuotientCopy line 101

    Source documentation

    The shallow-to-deep edge operator, including its right holonomy twist.

    def twistedQuotientCopy (f : G →* K) [Fintype f.ker] (hf : Function.Surjective f) (a : K) :
    lp (fun _ : K => ℂ) 2 →ₗᵢ[ℂ] lp (fun _ : G => ℂ) 2 :=
…
  14. theorem OAI.CoarseAssembly.twistedQuotientCopy_constant line 105
  15. theorem OAI.CoarseAssembly.twistedQuotientCopy_adjoint_constant line 111
  16. theorem OAI.CoarseAssembly.twistedQuotientCopy_apply line 117