IncidenceDegree.lean`

17 declarations, 0 contain sorry, 0 declared as axioms

def OAI.KervaireIncidenceCurrent.skewPart line 35
Source documentation
The ambient projection onto the skew-Hermitian tangent at the identity.
```
def skewPart {I : Type*} [Fintype I] [DecidableEq I] :
    Mat I →ₗ[ℝ] skewAdjoint.submodule ℝ (Mat I) where
…
```
Mentions: OAI.KervaireIncidenceCurrent.Mat
lemma OAI.KervaireIncidenceCurrent.skewPart_coe line 53
def OAI.KervaireIncidenceCurrent.tangentVolume line 61
Source documentation
A constant ambient form restricting to the determinant volume on the unitary tangent.
```
def tangentVolume {I J : Type*} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J]
    (b : Basis J ℝ (skewAdjoint.submodule ℝ (Mat I))) : Mat I [⋀^J]→L[ℝ] ℝ where
…
```
Mentions: OAI.KervaireIncidenceCurrent.Mat
lemma OAI.KervaireIncidenceCurrent.tangentVolume_equiv_ne_zero line 76
lemma OAI.KervaireIncidenceCurrent.model_jacobian_ne_zero line 85

lemma OAI.KervaireIncidenceCurrent.model_fiber_blocks line 95

Source documentation

The only incidence fiber over the identity is the connected gauge orbit.

lemma model_fiber_blocks (X A : Mat K) (B : Matrix K R ℂ) (C : Matrix R K ℂ)
    (D T : Mat R) (hQ : fromBlocks A B C D ∈ unitary (Mat (K ⊕ R)))
    (heq : diag X (-1) * fromBlocks A B C D = fromBlocks A B C D * diag 1 T) :
    X = 1 ∧ B = 0 ∧ C = 0 ∧ T = -1 ∧ A ∈ unitary (Mat K) ∧ D ∈ unitary (Mat R) := by
…

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

lemma OAI.KervaireIncidenceCurrent.model_fiber_iff line 126
lemma OAI.KervaireUnitaryExponential.exists_skew_log line 155
Source documentation
A finite-spectrum unitary has a skew logarithm, including the cut point -1.
```
lemma exists_skew_log (u : unitary A) (hfin : (spectrum ℂ (u : A)).Finite) :
    ∃ a : A, star a = -a ∧ exp a = (u : A) := by
…
```

lemma OAI.KervaireUnitaryExponential.exists_smooth_path line 174

Source documentation

A smooth ambient path from the identity to any finite-spectrum unitary.

lemma exists_smooth_path (u : unitary A) (hfin : (spectrum ℂ (u : A)).Finite) :
    ∃ p : ℝ → A, ContDiff ℝ ∞ p ∧ p 0 = 1 ∧ p 1 = (u : A) ∧
      ∀ t, p t ∈ unitary A := by
…

lemma OAI.KervaireUnitaryExponential.matrix_exists_smooth_path line 189
def OAI.KervaireIncidenceCurrent.jacobian line 201
lemma OAI.KervaireIncidenceCurrent.continuous_jacobian line 206
lemma OAI.KervaireIncidenceCurrent.model_fiber_gauge line 217
def OAI.KervaireIncidenceCurrent.modelVolumeBasis line 236
Source documentation
The determinant volume is normalized by the base point's horizontal frame.
```
def modelVolumeBasis (b : Basis J ℝ (Horizontal K R)) :
    Basis J ℝ (skewAdjoint.submodule ℝ (Mat (K ⊕ R))) :=
…
```
Mentions: OAI.KervaireIncidenceCurrent.Horizontal, OAI.KervaireIncidenceCurrent.Mat
lemma OAI.KervaireIncidenceCurrent.model_jacobian_base line 240
lemma OAI.KervaireIncidenceCurrent.model_jacobian_pos_gauge line 249
lemma OAI.KervaireIncidenceCurrent.model_jacobian_pos_fiber line 279