Canonical descent of periodic cover fields and deck-equivariant maps to the cylinder, with genuine continuity, inverse and volume properties.

noncomputable def EulerCylinderCoverDescent.sectionPoint (P : ℝ) [Fact (0 < P)] (q : EulerLiftedGradientSpace.LiftDomain P) : EulerLiftedGradientSpace.LiftTangent

Section point, given by (q.1,(AddCircle.equivIoc P 0 q.2 : ℝ)).

Equations

• EulerCylinderCoverDescent.sectionPoint P q = (q.1, ↑((AddCircle.equivIoc P 0) q.2))

theorem EulerCylinderCoverDescent.coveringMap_sectionPoint (P : ℝ) [Fact (0 < P)] (q : EulerLiftedGradientSpace.LiftDomain P) : EulerLiftedGradientSpace.coveringMap P (sectionPoint P q) = q

theorem EulerCylinderCoverDescent.sectionPoint_measurable (P : ℝ) [Fact (0 < P)] : Measurable (sectionPoint P)

noncomputable def EulerCylinderCoverDescent.descend (P : ℝ) [Fact (0 < P)] {V : Type u_1} (f : EulerLiftedGradientSpace.LiftTangent → V) (q : EulerLiftedGradientSpace.LiftDomain P) : V

Descend, given by f (sectionPoint P q).

Equations

• EulerCylinderCoverDescent.descend P f q = f (EulerCylinderCoverDescent.sectionPoint P q)

theorem EulerCylinderCoverDescent.descend_cover (P : ℝ) [Fact (0 < P)] {V : Type u_1} (f : EulerLiftedGradientSpace.LiftTangent → V) (hf : ∀ (a b : EulerLiftedGradientSpace.LiftTangent), EulerLiftedGradientSpace.coveringMap P a = EulerLiftedGradientSpace.coveringMap P b → f a = f b) (z : EulerLiftedGradientSpace.LiftTangent) : descend P f (EulerLiftedGradientSpace.coveringMap P z) = f z

theorem EulerCylinderCoverDescent.descend_measurable (P : ℝ) [Fact (0 < P)] {V : Type u_1} [MeasurableSpace V] (f : EulerLiftedGradientSpace.LiftTangent → V) (hf : Measurable f) : Measurable (descend P f)

theorem EulerCylinderCoverDescent.descend_continuous (P : ℝ) [Fact (0 < P)] {V : Type u_1} [TopologicalSpace V] (f : EulerLiftedGradientSpace.LiftTangent → V) (hf : Continuous f) (he : ∀ (a b : EulerLiftedGradientSpace.LiftTangent), EulerLiftedGradientSpace.coveringMap P a = EulerLiftedGradientSpace.coveringMap P b → f a = f b) : Continuous (descend P f)

theorem EulerCylinderCoverDescent.descend_joint_continuous (P : ℝ) [Fact (0 < P)] {K : Type u_1} {V : Type u_2} [TopologicalSpace K] [TopologicalSpace V] (f : K → EulerLiftedGradientSpace.LiftTangent → V) (hf : Continuous (Function.uncurry f)) (he : ∀ (t : K) (a b : EulerLiftedGradientSpace.LiftTangent), EulerLiftedGradientSpace.coveringMap P a = EulerLiftedGradientSpace.coveringMap P b → f t a = f t b) : Continuous fun (z : K × EulerLiftedGradientSpace.LiftDomain P) => descend P (f z.1) z.2

theorem EulerCylinderCoverDescent.fiber_constant_of_deck (P : ℝ) {V : Type u_1} (f : EulerLiftedGradientSpace.LiftTangent → V) (hf : ∀ (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent), f (z.1, ↑c + z.2) = f z) (a b : EulerLiftedGradientSpace.LiftTangent) (h : EulerLiftedGradientSpace.coveringMap P a = EulerLiftedGradientSpace.coveringMap P b) : f a = f b

noncomputable def EulerCylinderCoverDescent.descendMap (P : ℝ) [Fact (0 < P)] (f : EulerLiftedGradientSpace.LiftTangent → EulerLiftedGradientSpace.LiftTangent) : EulerLiftedGradientSpace.LiftDomain P → EulerLiftedGradientSpace.LiftDomain P

Descend map, given by descend P (coveringMap P ∘ f).

Equations

• EulerCylinderCoverDescent.descendMap P f = EulerCylinderCoverDescent.descend P (EulerLiftedGradientSpace.coveringMap P ∘ f)

theorem EulerCylinderCoverDescent.map_fiber_constant (P : ℝ) (f : EulerLiftedGradientSpace.LiftTangent → EulerLiftedGradientSpace.LiftTangent) (hdeck : ∀ (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent), f (z.1, ↑c + z.2) = ((f z).1, ↑c + (f z).2)) (a b : EulerLiftedGradientSpace.LiftTangent) (h : EulerLiftedGradientSpace.coveringMap P a = EulerLiftedGradientSpace.coveringMap P b) : EulerLiftedGradientSpace.coveringMap P (f a) = EulerLiftedGradientSpace.coveringMap P (f b)

theorem EulerCylinderCoverDescent.descendMap_cover (P : ℝ) [Fact (0 < P)] (f : EulerLiftedGradientSpace.LiftTangent → EulerLiftedGradientSpace.LiftTangent) (hdeck : ∀ (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent), f (z.1, ↑c + z.2) = ((f z).1, ↑c + (f z).2)) (z : EulerLiftedGradientSpace.LiftTangent) : descendMap P f (EulerLiftedGradientSpace.coveringMap P z) = EulerLiftedGradientSpace.coveringMap P (f z)

theorem EulerCylinderCoverDescent.descendMap_continuous (P : ℝ) [Fact (0 < P)] (f : EulerLiftedGradientSpace.LiftTangent → EulerLiftedGradientSpace.LiftTangent) (hdeck : ∀ (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent), f (z.1, ↑c + z.2) = ((f z).1, ↑c + (f z).2)) (hf : Continuous f) : Continuous (descendMap P f)

theorem EulerCylinderCoverDescent.descendMap_measurePreserving (P : ℝ) [Fact (0 < P)] (f : EulerLiftedGradientSpace.LiftTangent → EulerLiftedGradientSpace.LiftTangent) (hdeck : ∀ (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent), f (z.1, ↑c + z.2) = ((f z).1, ↑c + (f z).2)) (hf : MeasureTheory.MeasurePreserving f MeasureTheory.volume MeasureTheory.volume) : MeasureTheory.MeasurePreserving (descendMap P f) (EulerLiftedGradientSpace.liftMeasure P) (EulerLiftedGradientSpace.liftMeasure P)

theorem EulerCylinderCoverDescent.descendMap_leftInverse (P : ℝ) [Fact (0 < P)] (f : EulerLiftedGradientSpace.LiftTangent → EulerLiftedGradientSpace.LiftTangent) (hdeck : ∀ (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent), f (z.1, ↑c + z.2) = ((f z).1, ↑c + (f z).2)) (g : EulerLiftedGradientSpace.LiftTangent → EulerLiftedGradientSpace.LiftTangent) (hg : ∀ (c : ↥(AddSubgroup.zmultiples P)) (z : EulerLiftedGradientSpace.LiftTangent), g (z.1, ↑c + z.2) = ((g z).1, ↑c + (g z).2)) (hgf : Function.LeftInverse g f) : Function.LeftInverse (descendMap P g) (descendMap P f)