ZeroSign.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

Real signs of complex derivatives and signed regular-zero coordinates.

theorem OAI.Kaplansky.hasFDerivAt_continuous_zero_coordinates line 26
Source documentation
At a zero of a differentiable section, a merely continuous linear change of fiber coordinates has derivative T x ∘ D. No derivative of the transition family is needed. This applies to continuous bundle charts.
```
theorem hasFDerivAt_continuous_zero_coordinates
    {s : E → F} {D : E →L[ℝ] F} {x : E}
    (hs : HasFDerivAt s D x) (hz : s x = 0)
    {T : E → F →L[ℝ] G} (hT : ContinuousAt T x) :
    HasFDerivAt (fun y => T y (s y)) ((T x).comp D) x := by
…
```
theorem OAI.Kaplansky.real_det_complex line 62
Source documentation
The real determinant of a complex endomorphism is the squared modulus of its complex determinant. This includes complex dimension zero.
```
theorem real_det_complex (f : E →ₗ[ℂ] E) :
    (f.restrictScalars ℝ).det = Complex.normSq f.det := by
…
```
theorem OAI.Kaplansky.real_det_complex_equiv_pos line 67
Source documentation
Complex linear coordinate changes preserve real orientation.
```
theorem real_det_complex_equiv_pos (e : E ≃ₗ[ℂ] E) :
    0 < (e.toLinearMap.restrictScalars ℝ).det := by
…
```

theorem OAI.Kaplansky.complex_equiv_preserves_orientation line 76

Source documentation

Every orientation of the correct dimension is fixed by a complex automorphism viewed over the reals.

theorem complex_equiv_preserves_orientation {ι : Type*} [Fintype ι]
    (o : Orientation ℝ E ι) (hι : Fintype.card ι = Module.finrank ℝ E)
    (e : E ≃ₗ[ℂ] E) :
    Orientation.map ι (e.restrictScalars ℝ) o = o := by
…

def OAI.Kaplansky.complexDerivativeSign line 98
Source documentation
Sign of a real derivative between complex vector spaces of equal dimension. A complex identification is used to take the determinant; complexDerivativeSign_independent proves that choice immaterial. This is a local linear sign, not an Euler class or a global degree.
```
def complexDerivativeSign (e : E ≃ₗ[ℂ] F) (D : E →ₗ[ℝ] F) : SignType :=
…
```
theorem OAI.Kaplansky.complexDerivativeSign_independent line 101
theorem OAI.Kaplansky.complexDerivativeSign_complex_equiv line 114
Source documentation
An invertible complex derivative contributes positive sign.
```
theorem complexDerivativeSign_complex_equiv (e d : E ≃ₗ[ℂ] F) :
    complexDerivativeSign e (d.toLinearMap.restrictScalars ℝ) = 1 := by
…
```
Mentions: OAI.Kaplansky.complexDerivativeSign
theorem OAI.Kaplansky.complexDerivativeSign_post line 121
Source documentation
Changing complex coordinates in the codomain does not change the sign, even when the derivative itself is only real linear.
```
theorem complexDerivativeSign_post (e : E ≃ₗ[ℂ] F) (b : F ≃ₗ[ℂ] G)
    (D : E →ₗ[ℝ] F) :
    complexDerivativeSign (e.trans b) ((b.toLinearMap.restrictScalars ℝ).comp D) =
      complexDerivativeSign e D := by
…
```
Mentions: OAI.Kaplansky.complexDerivativeSign
theorem OAI.Kaplansky.complexDerivativeSign_pre line 132
Source documentation
Changing complex coordinates in the domain conjugates the endomorphism used for the real determinant, and consequently preserves its sign.
```
theorem complexDerivativeSign_pre (e : E ≃ₗ[ℂ] F) (a : G ≃ₗ[ℂ] E)
    (D : E →ₗ[ℝ] F) :
    complexDerivativeSign (a.trans e) (D.comp (a.toLinearMap.restrictScalars ℝ)) =
      complexDerivativeSign e D := by
…
```
Mentions: OAI.Kaplansky.complexDerivativeSign

theorem OAI.Kaplansky.regularZeroSign_continuous_fiber_coordinates line 161

Source documentation

The real derivative sign at a zero is invariant under a continuous change of complex fiber coordinates. The derivative may be only real linear; the transition family need not be differentiable.

theorem regularZeroSign_continuous_fiber_coordinates
    {s : E → F} {D : E →L[ℝ] F} {x : E}
    (hs : HasFDerivAt s D x) (hz : s x = 0)
    {T : E → F →L[ℝ] G} (hT : ContinuousAt T x)
    (b : F ≃L[ℂ] G) (hb : T x = b.toContinuousLinearMap.restrictScalars ℝ)
    (e : E ≃ₗ[ℂ] F) (e' : E ≃ₗ[ℂ] G) :
    complexDerivativeSign e' (fderiv ℝ (fun y => T y (s y)) x).toLinearMap =
      complexDerivativeSign e D.toLinearMap := by
…

Mentions: OAI.Kaplansky.complexDerivativeSign

theorem OAI.Kaplansky.regularZeroSign_base_coordinates line 175

Source documentation

Invariance under a differentiable change of base coordinates whose derivative at the zero is a complex linear equivalence.

theorem regularZeroSign_base_coordinates [FiniteDimensional ℂ G]
    {s : E → F} {D : E →L[ℝ] F} {g : G → E} {x : G}
    (hs : HasFDerivAt s D (g x)) (a : G ≃L[ℂ] E)
    (hg : HasFDerivAt g (a.toContinuousLinearMap.restrictScalars ℝ) x)
    (e : E ≃ₗ[ℂ] F) (e' : G ≃ₗ[ℂ] F) :
    complexDerivativeSign e' (fderiv ℝ (s ∘ g) x).toLinearMap =
      complexDerivativeSign e D.toLinearMap := by
…

Mentions: OAI.Kaplansky.complexDerivativeSign

theorem OAI.Kaplansky.complex_regular_zero_sign_in_continuous_coordinates line 188

Source documentation

A complex regular zero retains positive local sign after an arbitrary continuous change of complex fiber coordinates.

theorem complex_regular_zero_sign_in_continuous_coordinates
    {s : E → F} {x : E} (d : E ≃L[ℂ] F)
    (hs : HasFDerivAt s (d.toContinuousLinearMap.restrictScalars ℝ) x)
    (hz : s x = 0) {T : E → F →L[ℝ] G} (hT : ContinuousAt T x)
    (b : F ≃L[ℂ] G) (hb : T x = b.toContinuousLinearMap.restrictScalars ℝ)
    (e' : E ≃ₗ[ℂ] G) :
    complexDerivativeSign e' (fderiv ℝ (fun y => T y (s y)) x).toLinearMap = 1 := by
…

Mentions: OAI.Kaplansky.complexDerivativeSign

def OAI.Kaplansky.canonicalProductGraphChart line 206
Source documentation
The genuine product graph chart used for the canonical zero.
```
def canonicalProductGraphChart :
    OpenPartialHomeomorph (ProjectiveProduct K) (ProjectiveProductModel K) :=
…
```
theorem OAI.Kaplansky.canonicalProductGraphChart_symm line 210
theorem OAI.Kaplansky.canonicalProduct_zero_in_chart line 213
theorem OAI.Kaplansky.canonicalProductGraphChart_zero line 219
theorem OAI.Kaplansky.canonicalProductSectionCoordinates_hasFDerivAt line 225
def OAI.Kaplansky.canonicalProductLocalSign line 233
theorem OAI.Kaplansky.canonicalProductLocalSign_eq_one line 237
def OAI.Kaplansky.canonicalProductZeroSet line 246
Source documentation
The finite set here is proved to be the zero set of the actual global section, and to lie inside the chart where the local sign is computed.
```
def canonicalProductZeroSet : Finset (ProjectiveProduct K) :=
…
```
theorem OAI.Kaplansky.mem_canonicalProductZeroSet_iff line 249
theorem OAI.Kaplansky.canonicalProductZeroSet_in_chart line 255
def OAI.Kaplansky.canonicalProductSignedZeroCount line 265
Source documentation
The signed zero count of this specific section is one. Invariance under changing the section, and identification with an Euler/Chern invariant, remain separate obligations; neither is asserted by this definition.
```
def canonicalProductSignedZeroCount : ℤ :=
…
```
theorem OAI.Kaplansky.canonicalProductSignedZeroCount_eq_one line 268