OAI/GroupTheory/PolycyclicRecognition/Geometry/ExponentialBasisSection.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A global section for a linear exponential quotient

A product of lifted basis one-parameter subgroups is a continuous global section. Only the individual exponential curves are used; the exponential map need not be globally invertible or even be supplied as a continuous map.

  1. theorem OAI.PolycyclicRecognition.exponentialProduct_linear_quotient line 24
  2. theorem OAI.PolycyclicRecognition.exists_smooth_section_of_exponential_linear_quotient line 41
  3. theorem OAI.PolycyclicRecognition.exists_continuous_section_of_exponential_linear_quotient line 79
  4. theorem OAI.PolycyclicRecognition.isQuotientMap_of_exponential_linear_quotient line 89