OAI/GroupTheory/PolycyclicRecognition/Geometry/AnalyticRepresentationAtlas.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Analytic charts supplied by a local matrix representation

A local coordinate obtained by projecting a representation, with analytic matrix entries in those coordinates, supplies analytic translated charts.

  1. structure OAI.PolycyclicRecognition.RepresentedLocalChart line 22

    Source documentation

    Only the concrete local chart data needed for the analytic atlas.

    structure RepresentedLocalChart (ρ : G →* Aˣ) where
…
  2. def OAI.PolycyclicRecognition.RepresentedLocalChart.translated line 39
  3. theorem OAI.PolycyclicRecognition.RepresentedLocalChart.translated_apply line 42
  4. theorem OAI.PolycyclicRecognition.RepresentedLocalChart.translated_symm_apply line 44
  5. theorem OAI.PolycyclicRecognition.RepresentedLocalChart.translated_target line 49
  6. def OAI.PolycyclicRecognition.RepresentedLocalChart.chartedSpace line 55
  7. theorem OAI.PolycyclicRecognition.RepresentedLocalChart.transition_contDiff line 63
  8. theorem OAI.PolycyclicRecognition.RepresentedLocalChart.isManifold line 86