FrameNormalization.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Integral normalization of finite-line frames over affine-avoidance covers.

def OAI.Kaplansky.finiteLineFrameRelativeIso line 20
Source documentation
Relative coordinates of any finite sum with genuine continuous line frames.
```
def finiteLineFrameRelativeIso (n : ℕ) :=
…
```
def OAI.Kaplansky.finiteLineFrameNormalization line 26
theorem OAI.Kaplansky.finiteLineFrame_transition line 33

theorem OAI.Kaplansky.finiteLineFrameNormalization_eq_of_finite_cover line 45

Source documentation

Normalization of the actual finite sum of actual line cores is independent of the chosen continuous nonvanishing line frames on a finite contractible cover with the stated lower intersection vanishing. No global contractibility or connectedness hypothesis is required.

theorem finiteLineFrameNormalization_eq_of_finite_cover
    {J : Type} (T : Finset J) (U : J → Set A)
    (hopen : ∀ i ∈ T, IsOpen (U i)) (hcover : (⋃ i ∈ T, U i) = Set.univ)
    (hchart : ∀ i ∈ T, (U i).Nonempty → ContractibleSpace (U i))
    (n : ℕ)
    (hinter : ∀ I : Finset J, I.Nonempty → I ⊆ T → ∀ q < n+1,
      Limits.IsZero (relativeSingularHomology
        (subspaceInclusion {z : (⋂ i ∈ I, U i) × (S → ℂ) | z.2 ≠ 0}) q)) :
    finiteLineFrameNormalization C v hn hc (n+1) =
      finiteLineFrameNormalization C w hwn hwc (n+1) := by
…

Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.finiteLineFrameNormalization

theorem OAI.Kaplansky.affineAvoidance_finiteLineFrameNormalization_eq line 101

Source documentation

On the complement of any finite family of affine zero sets, the two normalizations of the ACTUAL finite sum of line cores coincide in fiber degree. Contractibility, connectivity, transition degree and homology vanishing are not premises: the finite convex cover supplies the comparison.

theorem affineAvoidance_finiteLineFrameNormalization_eq
    (l : J → E →L[ℝ] F) (c : J → F)
    (C : ∀ s, VectorBundleCore ℂ (affineAvoidanceSet l c) ℂ (I s))
    (v : ∀ s a, (C s).Fiber a) (hn : ∀ s a, v s a ≠ 0)
    (hc : ∀ s, Continuous (fun a => TotalSpace.mk' ℂ a (v s a)))
    (w : ∀ s a, (C s).Fiber a) (hwn : ∀ s a, w s a ≠ 0)
    (hwc : ∀ s, Continuous (fun a => TotalSpace.mk' ℂ a (w s a)))
    (hv : 2 ≤ Module.finrank ℝ (S → ℂ)) :
    finiteLineFrameNormalization C v hn hc (Module.finrank ℝ (S → ℂ)) =
      finiteLineFrameNormalization C w hwn hwc (Module.finrank ℝ (S → ℂ)) := by
…

Mentions: OAI.Kaplansky.affineAvoidanceSet, OAI.Kaplansky.finiteLineFrameNormalization