HyperplaneProduct.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

Hyperplane product sections and regular zeros.

theorem OAI.Kaplansky.continuous_pullbackLineCore_section line 16

Source documentation

Pullback of a genuine continuous section through the actual line-core pullback construction.

theorem continuous_pullbackLineCore_section {B X J : Type*} [TopologicalSpace B] [TopologicalSpace X]
    (C : VectorBundleCore ℂ B ℂ J) (g : C(X,B)) (s : ∀ b, C.Fiber b)
    (hs : Continuous (fun b => TotalSpace.mk' ℂ b (s b))) :
    Continuous (fun x => TotalSpace.mk' ℂ x (show (pullbackLineCore C g).Fiber x from s (g x))) := by
…

Mentions: OAI.Kaplansky.pullbackLineCore

def OAI.Kaplansky.hyperplaneProductStage line 29
Source documentation
Exactly K_i copies of each actual pulled-back hyperplane line.
```
def hyperplaneProductStage : LineStage K :=
…
```
Mentions: OAI.Kaplansky.LineStage
def OAI.Kaplansky.hyperplaneProductLineSection line 32
theorem OAI.Kaplansky.continuous_hyperplaneProductLineSection line 37
def OAI.Kaplansky.hyperplaneProductSection line 46
theorem OAI.Kaplansky.continuous_hyperplaneProductSection line 49
def OAI.Kaplansky.firstCoordinateProduct line 55
theorem OAI.Kaplansky.hyperplaneProductSection_eq_zero_iff line 61
Source documentation
The canonical section of the actual rank-sum(K_i) hyperplane sum has one zero on the actual projective-product base. No cohomology identification or invariance under changes of section is asserted by this zero-set theorem.
```
theorem hyperplaneProductSection_eq_zero_iff (P : ProjectiveProduct K) :
    hyperplaneProductSection K P=0 ↔ P=firstCoordinateProduct K := by
…
```
Mentions: OAI.Kaplansky.hyperplaneProductSection, OAI.Kaplansky.firstCoordinateProduct
theorem OAI.Kaplansky.hyperplaneProductStage_rank line 80
def OAI.Kaplansky.canonicalProductGraphPoint line 94
theorem OAI.Kaplansky.canonicalProductGraphPoint_zero line 97
def OAI.Kaplansky.canonicalProductSectionCoordinates line 109
Source documentation
The actual global product section expressed componentwise in the constructed graph evaluation trivializations.
```
def canonicalProductSectionCoordinates (A : ProjectiveProductModel K) : (Σ i, Fin (K i)) → ℂ :=
…
```
theorem OAI.Kaplansky.canonicalProductSectionCoordinates_eq line 113
def OAI.Kaplansky.productSlopeEvaluationEquiv line 127
theorem OAI.Kaplansky.canonicalProductSection_regular_zero line 134
Source documentation
The unique zero of the actual product section has an invertible complex linear derivative in the genuine graph bundle coordinates. The Euler-index invariance and Chern-class identification are not assumed or proved here.
```
theorem canonicalProductSection_regular_zero :
    HasFDerivAt (canonicalProductSectionCoordinates K)
      (productSlopeEvaluationEquiv K).toContinuousLinearMap 0 ∧
      Function.Bijective (productSlopeEvaluationEquiv K) := by
…
```
Mentions: OAI.Kaplansky.canonicalProductSectionCoordinates, OAI.Kaplansky.productSlopeEvaluationEquiv
theorem OAI.Kaplansky.canonicalProductSection_regular_zero_real line 144