Obstruction.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

Nonvanishing twisted section classes and the stable retained-bundle obstruction.

theorem OAI.Kaplansky.sectionProductNormalization line 14
def OAI.Kaplansky.twistedRestrictedSection line 35
theorem OAI.Kaplansky.twistedStandardBundleCoordinates_section line 40
def OAI.Kaplansky.twistedLocalSectionHomeomorph line 58
theorem OAI.Kaplansky.twistedLocalSectionHomeomorph_zero line 62
def OAI.Kaplansky.twistedLocalSectionRelativeIso line 69
def OAI.Kaplansky.twistedRestrictedSectionRelativeMap line 79
theorem OAI.Kaplansky.twistedRestrictedSection_normalization line 92
theorem OAI.Kaplansky.twistedGraphBundleChartNormalization_isIso line 107
theorem OAI.Kaplansky.twistedGraphBundleChartToAmbient_mono line 118
theorem OAI.Kaplansky.twistedProjectiveDimensions_sum line 130
def OAI.Kaplansky.twistedOrdinaryRelativeMap line 135
theorem OAI.Kaplansky.twistedOrdinaryRelativeMap_chart line 147
theorem OAI.Kaplansky.twistedOrdinaryRelativeMap_mono line 160
theorem OAI.Kaplansky.twistedOrdinaryRelativeMap_comparison line 185
theorem OAI.Kaplansky.twistedOrdinarySection_fundamental_ne_zero line 196
Source documentation
The actual twisted section carries the existing augmented-base fundamental class to a nonzero ordinary relative class.
```
theorem twistedOrdinarySection_fundamental_ne_zero
    (hp : 0 < ∑ i, twistedProjectiveDimensions K h i) :
    ordinarySectionClassMap (twistedHyperplaneSection K h)
      (continuous_twistedHyperplaneSection K h) (2*∑ i, twistedProjectiveDimensions K h i)
      (projectiveProductFundamentalClass (twistedProjectiveDimensions K h) hp) ≠ 0 := by
…
```
Mentions: OAI.Kaplansky.twistedProjectiveDimensions, OAI.Kaplansky.ordinarySectionClassMap, OAI.Kaplansky.twistedHyperplaneSection, OAI.Kaplansky.continuous_twistedHyperplaneSection, OAI.Kaplansky.projectiveProductFundamentalClass
theorem OAI.Kaplansky.twistedHyperplane_every_section_has_zero line 214
theorem OAI.Kaplansky.twistedSourceStage_no_large_frame line 244
Source documentation
The tensor construction contradicts any frame with more vectors than the displayed trivial rank. The frame need not respect the line summands.
```
theorem twistedSourceStage_no_large_frame {ι : Type} [Fintype ι]
    (K : ι → ℕ) (h d : ℕ) (hp : 0 < h+∑ i, K i) (hd : h < d) :
    IsEmpty (ContinuousOrthonormalStageFrame (twistedSourceStage K h) d) := by
…
```
Mentions: OAI.Kaplansky.ContinuousOrthonormalStageFrame, OAI.Kaplansky.twistedSourceStage
def OAI.Kaplansky.retainedTwistedSlotEquiv line 253

def OAI.Kaplansky.retainedTwistedSourceUnitary line 266

Source documentation

Exact slot regrouping as an actual unitary bundle isomorphism.

def retainedTwistedSourceUnitary (m R : ℕ) :
    UnitaryBundleEquiv
      (twistedSourceStage (testProjectiveDimension m R) (retainedTrivialMultiplicity m R)).Model
      (retainedGroupedStage m R).Model
      (twistedSourceStage (testProjectiveDimension m R) (retainedTrivialMultiplicity m R)).Fiber
      (retainedGroupedStage m R).Fiber :=
…

Mentions: OAI.Kaplansky.UnitaryBundleEquiv, OAI.Kaplansky.twistedSourceStage, OAI.Kaplansky.testProjectiveDimension, OAI.Kaplansky.retainedTrivialMultiplicity, OAI.Kaplansky.retainedGroupedStage

theorem OAI.Kaplansky.retainedGrouped_no_test_frame line 277
theorem OAI.Kaplansky.retainedGrouped_no_independent_test_frame line 287
Source documentation
Normalizing an arbitrary independent continuous frame reduces it to the excluded orthonormal frame; no extra metric premise is required.
```
theorem retainedGrouped_no_independent_test_frame {m R : ℕ} (hm : 0 < m) (hR : 0 < R) :
    IsEmpty (ContinuousIndependentStageFrame (retainedGroupedStage m R) (2*m*testRank m R 0)) := by
…
```
Mentions: OAI.Kaplansky.ContinuousIndependentStageFrame, OAI.Kaplansky.retainedGroupedStage, OAI.Kaplansky.testRank
theorem OAI.Kaplansky.actualAlgebra_matrix_not_properlyInfinite line 292