AffineAvoidance.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Affine-avoidance covers and convex product-pair homology.

def OAI.Kaplansky.affineAvoidanceSet line 20
Source documentation
The complement of finitely many affine zero sets, including dependent or zero affine maps. No general-position or nonempty assumption is made.
```
def affineAvoidanceSet (l : J → E →L[ℝ] F) (c : J → F) : Set E := {x | ∀ j, l j x + c j ≠ 0}
```
def OAI.Kaplansky.affineAvoidanceChart line 23
Source documentation
A finite chart chooses a nonzero signed real coordinate for each image.
```
def affineAvoidanceChart (l : J → E →L[ℝ] F) (c : J → F)
    (s : J → Fin (Module.finrank ℝ F) × Bool) : Set E :=
…
```
theorem OAI.Kaplansky.affineAvoidanceChart_open line 27
theorem OAI.Kaplansky.affineAvoidanceChart_convex line 32
theorem OAI.Kaplansky.affineAvoidanceCharts_cover line 37
theorem OAI.Kaplansky.affineAvoidanceChart_subset line 60
theorem OAI.Kaplansky.affineAvoidanceSet_open line 66
theorem OAI.Kaplansky.convexRestrictedBase_contractible line 81
Source documentation
A nonempty convex subset remains contractible when viewed inside a larger base subset, with its actual iterated subspace topology.
```
theorem convexRestrictedBase_contractible (D C : Set E) (hCD : C ⊆ D)
    (hc : Convex ℝ C) (hne : (Subtype.val ⁻¹' C : Set D).Nonempty) :
    ContractibleSpace (Subtype.val ⁻¹' C : Set D) := by
…
```

theorem OAI.Kaplansky.convexCover_product_intersection_below_isZero line 90

Source documentation

Every nonempty intersection of convex base charts has the required lower relative vanishing. Empty intersections have zero groups as well.

theorem convexCover_product_intersection_below_isZero
    (D : Set E) (S : Finset J) (C : J → Set E)
    (hsub : ∀ i ∈ S, C i ⊆ D) (hconv : ∀ i ∈ S, Convex ℝ (C i))
    (T : Finset J) (ht : T.Nonempty) (hts : T ⊆ S)
    (hv : 2 ≤ Module.finrank ℝ V) (q : ℕ) (hq : q < Module.finrank ℝ V) :
    IsZero (relativeSingularHomology
      (subspaceInclusion {z : (⋂ i ∈ T, (Subtype.val ⁻¹' C i : Set D)) × V |
        z.2 ≠ 0}) q) := by
…

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

theorem OAI.Kaplansky.convexOpenUnion_product_below_isZero line 120

Source documentation

Relative homology below fiber dimension vanishes over any finite union of open convex base sets. Neither connectivity nor contractibility of that union is asserted.

theorem convexOpenUnion_product_below_isZero
    (S : Finset J) (C : J → Set E)
    (hopen : ∀ i ∈ S, IsOpen (C i)) (hconv : ∀ i ∈ S, Convex ℝ (C i))
    (hv : 2 ≤ Module.finrank ℝ V) (q : ℕ) (hq : q < Module.finrank ℝ V) :
    IsZero (relativeSingularHomology (subspaceInclusion
      {z : (⋃ i ∈ S, C i) × V | z.2 ≠ 0}) q) := by
…

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

theorem OAI.Kaplansky.convexOpenCover_product_projection_isIso line 147

Source documentation

Over a path-connected base admitting a finite open convex cover, the actual fiber projection is an isomorphism in fiber degree.

theorem convexOpenCover_product_projection_isIso
    (D : Set E) [PathConnectedSpace D] (S : Finset J) (C : J → Set E)
    (hopen : ∀ i ∈ S, IsOpen (C i)) (hconv : ∀ i ∈ S, Convex ℝ (C i))
    (hcover : (⋃ i ∈ S, C i) = D)
    (hv : 2 ≤ Module.finrank ℝ V) :
    IsIso (productPairProjection (B := D) ({0}ᶜ : Set V) (Module.finrank ℝ V)) := by
…

Mentions: OAI.Kaplansky.productPairProjection

theorem OAI.Kaplansky.affineAvoidance_product_below_isZero line 185
Source documentation
Lower relative vanishing over a finite affine-zero complement, proved by the explicit convex cover. All kernels may intersect.
```
theorem affineAvoidance_product_below_isZero (l : J → E →L[ℝ] F) (c : J → F)
    (hv : 2 ≤ Module.finrank ℝ V) (q : ℕ) (hq : q < Module.finrank ℝ V) :
    IsZero (relativeSingularHomology (subspaceInclusion
      {z : affineAvoidanceSet l c × V | z.2 ≠ 0}) q) := by
…
```
Mentions: OAI.Kaplansky.relativeSingularHomology, OAI.Kaplansky.subspaceInclusion, OAI.Kaplansky.affineAvoidanceSet
theorem OAI.Kaplansky.affineAvoidance_product_projection_isIso line 203
Source documentation
In fiber degree, the actual projection over a path-connected finite affine-zero complement is an isomorphism.
```
theorem affineAvoidance_product_projection_isIso (l : J → E →L[ℝ] F) (c : J → F)
    [PathConnectedSpace (affineAvoidanceSet l c)] (hv : 2 ≤ Module.finrank ℝ V) :
    IsIso (productPairProjection (B := affineAvoidanceSet l c) ({0}ᶜ : Set V)
…
```
Mentions: OAI.Kaplansky.affineAvoidanceSet, OAI.Kaplansky.productPairProjection