OAI/GroupTheory/PolycyclicRecognition/Geometry/SmoothRotationalTwistLift.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Smooth subgroup lifts into the rotational graph

  1. theorem OAI.PolycyclicRecognition.contMDiff_rotationalTwistLift line 28
  2. theorem OAI.PolycyclicRecognition.mfderiv_rotationalTwistLift line 35

    Source documentation

    In the pulled-back atlas, lifting changes no tangent coordinates.

    theorem mfderiv_rotationalTwistLift
    (hf : ContMDiff (𝓘(ℝ,V)) (𝓘(ℝ,E)) ∞ f) (a : A) (v : V) :
    mfderiv (𝓘(ℝ,V)) (𝓘(ℝ,E)) (rotationalTwistLift α τ hinv f hfix) a v =
      mfderiv (𝓘(ℝ,V)) (𝓘(ℝ,E)) f a v := by
…

    Mentions: OAI.PolycyclicRecognition.rotationalTwistLift