OAI/GroupTheory/Kervaire/UnitaryHomotopy.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.KervaireUnitaryHomotopy.UMap line 35

   Source documentation

   A smooth ambient representative of a smooth unitary-valued map.

   structure UMap where
   …

2. instance OAI.KervaireUnitaryHomotopy.(instance at line 40) line 40
3. def OAI.KervaireUnitaryHomotopy.Elementary line 45

   Source documentation

   Elementary smooth homotopy; equalities only concern the unitary domain.

   def Elementary (F G : UMap B C) : Prop :=
   …

   Mentions: OAI.KervaireUnitaryHomotopy.UMap

4. def OAI.KervaireUnitaryHomotopy.Homotopic line 52

   Source documentation

   Finite chains suffice, so no smooth concatenation theorem is assumed.

   def Homotopic (F G : UMap B C) : Prop := Relation.EqvGen Elementary F G

   Mentions: OAI.KervaireUnitaryHomotopy.UMap, OAI.KervaireUnitaryHomotopy.Elementary

5. lemma OAI.KervaireUnitaryHomotopy.homotopic_of_elementary line 54
6. lemma OAI.KervaireUnitaryHomotopy.homotopic_refl line 57
7. lemma OAI.KervaireUnitaryHomotopy.homotopic_symm line 58
8. lemma OAI.KervaireUnitaryHomotopy.homotopic_trans line 60
9. lemma OAI.KervaireUnitaryHomotopy.fderiv_horizontal_congr line 71

   Source documentation

   Horizontal derivatives depend only on the restriction to the unitary group. This is essential: homotopies cancel X X* only on that group, not on all matrices.

   lemma fderiv_horizontal_congr {f g : ℝ × E → D}
       (hf : ContDiff ℝ ∞ f) (hg : ContDiff ℝ ∞ g) (t s : ℝ)
       (heq : ∀ x : unitary E, f (t,(x : E)) = g (s,(x : E)))
       (x : unitary E) (a : skewAdjoint.submodule ℝ E) :
       fderiv ℝ f (t,(x : E)) (0,(x : E)*(a : E)) =
         fderiv ℝ g (s,(x : E)) (0,(x : E)*(a : E)) := by
   …

10. lemma OAI.KervaireUnitaryHomotopy.invariant_of_elementary line 101
11. lemma OAI.KervaireIncidenceCurrent.incidence_restrict_congr line 125
12. lemma OAI.KervaireIncidenceCurrent.incidence_endpoint_integral line 133
13. def OAI.KervaireIncidenceCurrent.timeless line 152

    Source documentation

    An ambient representative independent of the time coordinate.

    def timeless (F : UMap (Mat K) (Mat (K ⊕ R))) : ℝ × Mat K → Mat (K ⊕ R) :=
    …

    Mentions: OAI.KervaireIncidenceCurrent.Mat

14. lemma OAI.KervaireIncidenceCurrent.contDiff_timeless line 156
15. def OAI.KervaireIncidenceCurrent.current line 160

    Source documentation

    The compact horizontal current evaluated on a smooth unitary map.

    def current {n : ℕ} (b : Fin n → Horizontal K R)
        (form : Mat (K ⊕ R) → Mat (K ⊕ R) [⋀^Fin n]→L[ℝ] ℝ)
        (F : UMap (Mat K) (Mat (K ⊕ R))) : ℝ :=
    …

    Mentions: OAI.KervaireIncidenceCurrent.Horizontal, OAI.KervaireIncidenceCurrent.Mat

16. lemma OAI.KervaireIncidenceCurrent.current_eq_of_elementary line 168
17. lemma OAI.KervaireIncidenceCurrent.current_eq_of_homotopic line 183
18. def OAI.KervaireIncidenceCurrent.model line 198
19. lemma OAI.KervaireIncidenceCurrent.contDiff_model line 200
20. lemma OAI.KervaireIncidenceCurrent.fderiv_model line 205
21. def OAI.KervaireIncidenceCurrent.skewConj line 218

    Source documentation

    Conjugation is a real linear automorphism of the skew-Hermitian space.

    def skewConj (U : unitary (Mat K)) :
        skewAdjoint.submodule ℝ (Mat K) ≃ₗ[ℝ] skewAdjoint.submodule ℝ (Mat K) where
    …

    Mentions: OAI.KervaireIncidenceCurrent.Mat

22. def OAI.KervaireIncidenceCurrent.gaugeFrame line 241
23. def OAI.KervaireIncidenceCurrent.gaugePoint line 244
24. lemma OAI.KervaireIncidenceCurrent.model_incidence_gauge line 252
25. def OAI.KervaireIncidenceCurrent.modelHorizontalEquiv line 259
26. lemma OAI.KervaireIncidenceCurrent.fderiv_model_gauge line 265