IncidenceTangent.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.KervaireIncidenceCurrent.contDiff_incidence line 34

lemma OAI.KervaireIncidenceCurrent.fderiv_incidence line 51

Source documentation

Its actual ambient Fréchet differential.

lemma fderiv_incidence {f : ℝ × Mat K → Mat (K ⊕ R)} (hf : ContDiff ℝ ∞ f)
    (p v : ℝ × Alg K R) :
    fderiv ℝ (incidence f) p v =
      fderiv ℝ f (p.1,p.2.1) (v.1,v.2.1) * p.2.2.1 * diag 1 (star p.2.2.2) * star p.2.2.1 +
      f (p.1,p.2.1) * v.2.2.1 * diag 1 (star p.2.2.2) * star p.2.2.1 +
      f (p.1,p.2.1) * p.2.2.1 * in22 (star v.2.2.2) * star p.2.2.1 +
      f (p.1,p.2.1) * p.2.2.1 * diag 1 (star p.2.2.2) * star v.2.2.1 := by
…

Mentions: OAI.KervaireIncidenceCurrent.Mat, OAI.KervaireIncidenceCurrent.Alg, OAI.KervaireIncidenceCurrent.incidence, OAI.KervaireIncidenceCurrent.diag, OAI.KervaireIncidenceCurrent.in22

def OAI.KervaireIncidenceCurrent.horizontalInput line 93
def OAI.KervaireIncidenceCurrent.horizontalDifferential line 109

lemma OAI.KervaireIncidenceCurrent.fderiv_frame_diagonal line 114

Source documentation

Diagonal frame directions and compensated fiber directions have identical images.

lemma fderiv_frame_diagonal {f : ℝ × Mat K → Mat (K ⊕ R)} (hf : ContDiff ℝ ∞ f)
    (t : ℝ) (X : Mat K) (Q : Mat (K ⊕ R)) (T : unitary (Mat R))
    (U : skewAdjoint.submodule ℝ (Mat K)) (V : skewAdjoint.submodule ℝ (Mat R)) :
    fderiv ℝ (incidence f) (t,X,Q,(T : Mat R)) (0,0,Q*diag U V,0) =
    fderiv ℝ (incidence f) (t,X,Q,(T : Mat R)) (0,0,0,(T : Mat R)*compensated T V) := by
…

Mentions: OAI.KervaireIncidenceCurrent.Mat, OAI.KervaireIncidenceCurrent.incidence, OAI.KervaireIncidenceCurrent.diag, OAI.KervaireIncidenceCurrent.compensated

lemma OAI.KervaireIncidenceCurrent.direction_bracket line 133

lemma OAI.KervaireIncidenceCurrent.fderiv_direction_bracket line 148

Source documentation

The differential of a bracket is in the span of horizontal directions, with the explicitly computed coefficients.

lemma fderiv_direction_bracket {f : ℝ × Mat K → Mat (K ⊕ R)} (hf : ContDiff ℝ ∞ f)
    (t : ℝ) (p : unitary (Alg K R)) (h g : Horizontal K R) :
    fderiv ℝ (incidence f) (t,(p : Alg K R))
      (0,(p : Alg K R)*((direction h : Alg K R)*(direction g : Alg K R)-
        (direction g : Alg K R)*(direction h : Alg K R))) =
    fderiv ℝ (incidence f) (t,(p : Alg K R))
      (0,(p : Alg K R)*(direction (effectiveBracket ⟨p.val.2.2,(unitary_alg_parts p).2.2⟩ h g) : Alg K R)) := by
…

Mentions: OAI.KervaireIncidenceCurrent.Mat, OAI.KervaireIncidenceCurrent.Alg, OAI.KervaireIncidenceCurrent.Horizontal, OAI.KervaireIncidenceCurrent.incidence, OAI.KervaireIncidenceCurrent.direction, OAI.KervaireIncidenceCurrent.effectiveBracket, OAI.KervaireIncidenceCurrent.unitary_alg_parts

lemma OAI.KervaireIncidenceCurrent.basis_bracket_condition line 187
abbrev OAI.KervaireFixedSpace.Skew line 217
theorem OAI.KervaireFixedSpace.skew_entry line 220
Source documentation
Entrywise skew-Hermitian symmetry.
```
theorem skew_entry (T : Skew K) (i j : K) : star (T.val j i) = -T.val i j := by
…
```
Mentions: OAI.KervaireFixedSpace.Skew
def OAI.KervaireFixedSpace.skewBlock11 line 224
Source documentation
The first diagonal block of a skew-Hermitian matrix.
```
def skewBlock11 (T : Skew (K ⊕ R)) : Skew K :=
…
```
Mentions: OAI.KervaireFixedSpace.Skew
def OAI.KervaireFixedSpace.skewBlock22 line 230
Source documentation
The second diagonal block of a skew-Hermitian matrix.
```
def skewBlock22 (T : Skew (K ⊕ R)) : Skew R :=
…
```
Mentions: OAI.KervaireFixedSpace.Skew
def OAI.KervaireFixedSpace.derivativeMatrix line 236
Source documentation
The block formula for the incidence derivative.
```
def derivativeMatrix (ε : ℝ) (A : Skew K) (B : Skew R) (Z : Matrix R K ℂ) :
    Matrix (K ⊕ R) (K ⊕ R) ℂ :=
…
```
Mentions: OAI.KervaireFixedSpace.Skew
theorem OAI.KervaireFixedSpace.derivativeMatrix_skew line 240
def OAI.KervaireFixedSpace.degreeDerivative line 250
def OAI.KervaireFixedSpace.inverseDerivative line 267
Source documentation
Explicit inverse coordinates of the differential; no finite-dimensional or genericity assumption is needed for this algebraic step.
```
def inverseDerivative (ε : ℝ) (T : Skew (K ⊕ R)) : Skew K × Skew R × Matrix R K ℂ :=
…
```
Mentions: OAI.KervaireFixedSpace.Skew
theorem OAI.KervaireFixedSpace.degreeDerivative_inverse line 270
theorem OAI.KervaireFixedSpace.inverse_degreeDerivative line 284
def OAI.KervaireFixedSpace.degreeDerivativeEquiv line 301
Source documentation
The differential at the regular fiber is a real-linear isomorphism.
```
def degreeDerivativeEquiv (ε : ℝ) (hε : ε ≠ 0) :
    (Skew K × Skew R × Matrix R K ℂ) ≃ₗ[ℝ] Skew (K ⊕ R) :=
…
```
Mentions: OAI.KervaireFixedSpace.Skew
lemma OAI.KervaireIncidenceCurrent.incidence_integral_constant line 320