GraphCover.lean`

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Projective graph denominators, intersections, and finite graph covers.

theorem OAI.Kaplansky.ComplexGrassmann.horizontalOne_eq_smul line 15
theorem OAI.Kaplansky.ComplexGrassmann.horizontalOne_isUnit_iff line 23
Source documentation
An actual complex endomorphism of a one-dimensional horizontal space is invertible exactly when its scalar coefficient is nonzero.
```
theorem horizontalOne_isUnit_iff (L : GraphHorizontal 1 →L[ℂ] GraphHorizontal 1) :
    IsUnit L ↔ L (fun _ => 1) 0 ≠ 0 := by
…
```
Mentions: OAI.Kaplansky.ComplexGrassmann.GraphHorizontal
def OAI.Kaplansky.ComplexGrassmann.graphDenominatorLinear line 56
Source documentation
The variable part of the graph-overlap denominator.
```
def graphDenominatorLinear (F G : GraphFrame 1 k) : GraphSlope 1 k →L[ℂ] ℂ :=
…
```
Mentions: OAI.Kaplansky.ComplexGrassmann.GraphFrame, OAI.Kaplansky.ComplexGrassmann.GraphSlope
def OAI.Kaplansky.ComplexGrassmann.graphDenominatorConstant line 72
theorem OAI.Kaplansky.ComplexGrassmann.graphDenominator_eq line 75
theorem OAI.Kaplansky.ComplexGrassmann.projective_inGraphChart_iff_denominator line 86
Source documentation
The actual projective overlap is precisely the complement of an affine scalar zero set, for arbitrary complex graph frames.
```
theorem projective_inGraphChart_iff_denominator (F G : GraphFrame 1 k) (A : GraphSlope 1 k) :
    InGraphChart G (slopePoint F A).val ↔
      graphDenominatorLinear F G A + graphDenominatorConstant F G ≠ 0 := by
…
```
Mentions: OAI.Kaplansky.ComplexGrassmann.GraphFrame, OAI.Kaplansky.ComplexGrassmann.GraphSlope, OAI.Kaplansky.ComplexGrassmann.InGraphChart, OAI.Kaplansky.ComplexGrassmann.slopePoint, OAI.Kaplansky.ComplexGrassmann.graphDenominatorLinear, OAI.Kaplansky.ComplexGrassmann.graphDenominatorConstant
def OAI.Kaplansky.ComplexGrassmann.projectiveProductGraphChart line 101
theorem OAI.Kaplansky.ComplexGrassmann.projectiveProductGraphChart_target line 105
def OAI.Kaplansky.ComplexGrassmann.projectiveProductGraphHomeomorph line 110
theorem OAI.Kaplansky.ComplexGrassmann.projectiveProductGraphHomeomorph_symm_apply line 115
def OAI.Kaplansky.ComplexGrassmann.productGraphDenominatorLinear line 119
def OAI.Kaplansky.ComplexGrassmann.productGraphDenominatorConstant line 124
theorem OAI.Kaplansky.ComplexGrassmann.productGraph_multi_overlap_iff line 131
Source documentation
Simultaneous membership in any finite family of actual graph charts is exactly a finite affine nonvanishing condition in a fixed graph chart.
```
theorem productGraph_multi_overlap_iff (F : ∀ i, GraphFrame 1 (K i))
    (G : J → ∀ i, GraphFrame 1 (K i)) (A : ProjectiveProductModel K) :
    (∀ j, ((projectiveProductGraphHomeomorph K F).symm A).val ∈
      (projectiveProductGraphChart K (G j)).source) ↔
    A ∈ affineAvoidanceSet (productGraphDenominatorLinear K F G)
      (productGraphDenominatorConstant K F G) := by
…
```
Mentions: OAI.Kaplansky.ComplexGrassmann.GraphFrame, OAI.Kaplansky.ComplexGrassmann.ProjectiveProductModel, OAI.Kaplansky.ComplexGrassmann.projectiveProductGraphHomeomorph, OAI.Kaplansky.ComplexGrassmann.projectiveProductGraphChart, OAI.Kaplansky.affineAvoidanceSet, OAI.Kaplansky.ComplexGrassmann.productGraphDenominatorLinear, OAI.Kaplansky.ComplexGrassmann.productGraphDenominatorConstant
def OAI.Kaplansky.ComplexGrassmann.projectiveProductGraphIntersection line 144
def OAI.Kaplansky.ComplexGrassmann.projectiveProductGraphIntersectionHomeomorph line 150
Source documentation
Actual iterated graph-chart intersections, with their subspace topology, have the explicit affine-complement coordinates.
```
def projectiveProductGraphIntersectionHomeomorph (F : ∀ i, GraphFrame 1 (K i))
    (G : J → ∀ i, GraphFrame 1 (K i)) :
    projectiveProductGraphIntersection K F G ≃ₜ
      affineAvoidanceSet (productGraphDenominatorLinear K F G)
        (productGraphDenominatorConstant K F G) :=
…
```
Mentions: OAI.Kaplansky.ComplexGrassmann.GraphFrame, OAI.Kaplansky.ComplexGrassmann.projectiveProductGraphIntersection, OAI.Kaplansky.affineAvoidanceSet, OAI.Kaplansky.ComplexGrassmann.productGraphDenominatorLinear, OAI.Kaplansky.ComplexGrassmann.productGraphDenominatorConstant
theorem OAI.Kaplansky.ComplexGrassmann.projectiveProductGraphCharts_cover line 174
theorem OAI.Kaplansky.ComplexGrassmann.projectiveProduct_finiteGraphCover line 183
Source documentation
Compactness supplies a genuine finite cover of the actual projective product by graph charts. Any specified chart can be retained in the cover.
```
theorem projectiveProduct_finiteGraphCover (F₀ : ∀ i, GraphFrame 1 (K i)) :
    ∃ S : Finset (∀ i, GraphFrame 1 (K i)), F₀ ∈ S ∧
      (⋃ F ∈ S, (projectiveProductGraphChart K F).source) = univ := by
…
```
Mentions: OAI.Kaplansky.ComplexGrassmann.GraphFrame, OAI.Kaplansky.ComplexGrassmann.projectiveProductGraphChart