LineNormalization.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Integral line normalization and finite-cover diagonal comparison.

def OAI.Kaplansky.finiteLineEvaluationRelativeIso line 20
Source documentation
Relative pair coordinates on the ACTUAL finite sum of hyperplane lines.
```
def finiteLineEvaluationRelativeIso (n : ℕ) :=
…
```
def OAI.Kaplansky.finiteLineEvaluationNormalization line 28
Source documentation
Fiber normalization defined even when the base is not contractible.
```
def finiteLineEvaluationNormalization (n : ℕ) :=
…
```
theorem OAI.Kaplansky.finiteLineEvaluationNormalization_isIso line 32
theorem OAI.Kaplansky.finiteLineEvaluation_transition line 45
Source documentation
The transition between these actual evaluation charts is diagonal on each fiber, with explicitly invertible complex entries.
```
theorem finiteLineEvaluation_transition (a : A) (z : S → ℂ) :
    finiteLineEvaluationEquiv p w hwm hwn a
      ((finiteLineEvaluationEquiv p v hm hn a).symm z) =
    complexDiagonalMap (fun s => complexLineCoordinateUnit
      (pullbackEvaluationEquiv (p s) (v s) (hm s) (hn s) a)
      (pullbackEvaluationEquiv (p s) (w s) (hwm s) (hwn s) a)) z := by
…
```
Mentions: OAI.Kaplansky.finiteLineEvaluationEquiv, OAI.Kaplansky.complexDiagonalMap, OAI.Kaplansky.complexLineCoordinateUnit, OAI.Kaplansky.pullbackEvaluationEquiv
theorem OAI.Kaplansky.finiteLineEvaluationNormalization_eq line 59
Source documentation
Genuine integral fiber normalizations from ANY two continuous, nonvanishing line frames agree over a contractible base. No orientation, transition degree, or homology compatibility premise is assumed.
```
theorem finiteLineEvaluationNormalization_eq [ContractibleSpace A] (n : ℕ) :
    finiteLineEvaluationNormalization p v hm hn hc n =
      finiteLineEvaluationNormalization p w hwm hwn hwc n := by
…
```
Mentions: OAI.Kaplansky.finiteLineEvaluationNormalization

theorem OAI.Kaplansky.productPairCoordinateMap_eq_projection_of_finite_cover line 104

Source documentation

A finite contractible cover detects the normalization of a varying complex diagonal coordinate change. The whole base need not be contractible or connected; the lower intersection groups are the actual relative groups.

theorem productPairCoordinateMap_eq_projection_of_finite_cover
    (S : Finset J) (U : J → Set B)
    (hopen : ∀ i ∈ S, IsOpen (U i)) (hcover : (⋃ i ∈ S, U i) = Set.univ)
    (hchart : ∀ i ∈ S, (U i).Nonempty → ContractibleSpace (U i))
    (n : ℕ)
    (hinter : ∀ T : Finset J, T.Nonempty → T ⊆ S → ∀ q < n+1,
      IsZero (relativeSingularHomology
        (subspaceInclusion {z : (⋂ i ∈ T, U i) × (ι → ℂ) | z.2 ≠ 0}) q))
    (f : C(B × (ι → ℂ),(ι → ℂ))) (hf : ∀ z, z.2 ≠ 0 → f z ≠ 0)
    (a : B → ι → ℂˣ) (he : ∀ b v, f (b,v) = complexDiagonalMap (a b) v) :
    productPairCoordinateMap f hf (n+1) =
      productPairProjection (B := B) ({0}ᶜ : Set (ι → ℂ)) (n+1) := by
…

Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.complexDiagonalMap, OAI.Kaplansky.productPairCoordinateMap, OAI.Kaplansky.productPairProjection

theorem OAI.Kaplansky.finiteLineEvaluationNormalization_eq_of_finite_cover line 172

Source documentation

Normalization of the actual finite sum of hyperplane lines 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 finiteLineEvaluationNormalization_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)) :
    finiteLineEvaluationNormalization p v hm hn hc (n+1) =
      finiteLineEvaluationNormalization p w hwm hwn hwc (n+1) := by
…

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

theorem OAI.Kaplansky.affineAvoidance_finiteLineEvaluationNormalization_eq line 229

Source documentation

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

theorem affineAvoidance_finiteLineEvaluationNormalization_eq
    (l : J → E →L[ℝ] F) (c : J → F)
    (p : ∀ s, C(affineAvoidanceSet l c,projectionSpace (d s) 1))
    (v : ∀ s, affineAvoidanceSet l c → EuclideanSpace ℂ (Fin (d s)))
    (hm : ∀ s a, v s a ∈ projectionLine (p s a))
    (hn : ∀ s a, v s a ≠ 0) (hc : ∀ s, Continuous (v s))
    (w : ∀ s, affineAvoidanceSet l c → EuclideanSpace ℂ (Fin (d s)))
    (hwm : ∀ s a, w s a ∈ projectionLine (p s a))
    (hwn : ∀ s a, w s a ≠ 0) (hwc : ∀ s, Continuous (w s))
    (hv : 2 ≤ Module.finrank ℝ (S → ℂ)) :
    finiteLineEvaluationNormalization p v hm hn hc (Module.finrank ℝ (S → ℂ)) =
      finiteLineEvaluationNormalization p w hwm hwn hwc (Module.finrank ℝ (S → ℂ)) := by
…

Mentions: OAI.Kaplansky.affineAvoidanceSet, OAI.Kaplansky.projectionSpace, OAI.Kaplansky.projectionLine, OAI.Kaplansky.finiteLineEvaluationNormalization