Connected.lean`

35 declarations, 0 contain sorry, 0 declared as axioms

Connected-cover homology, degree-zero components, and degree-one generators.

theorem OAI.Kaplansky.relativeHomologyBoundary_eq_zero_of_contractible line 16
Source documentation
A contractible subspace has zero relative connecting boundary in positive degree.
```
theorem relativeHomologyBoundary_eq_zero_of_contractible {A X : TopCat.{0}}
    (i : A ⟶ X) [Mono i] [ContractibleSpace A] (n : ℕ) (hn : n ≠ 0) :
    relativeHomologyBoundary i n = 0 :=
…
```
Mentions: OAI.Kaplansky.relativeHomologyBoundary
theorem OAI.Kaplansky.absoluteToRelative_bijective_of_contractible line 23
Source documentation
Localization to a relative pair is an isomorphism above degree one when its removed subspace is contractible. The map is the actual quotient map.
```
theorem absoluteToRelative_bijective_of_contractible {A X : TopCat.{0}}
    (i : A ⟶ X) [Mono i] [ContractibleSpace A] (n : ℕ) (hn : n ≠ 0) :
    Function.Bijective (absoluteToRelative i (n+1)) := by
…
```
Mentions: OAI.Kaplansky.absoluteToRelative
def OAI.Kaplansky.contractibleSubspaceLocalizationIso line 39
theorem OAI.Kaplansky.contractibleSubspaceLocalizationIso_hom line 45
abbrev OAI.Kaplansky.pointComponentIso line 54
abbrev OAI.Kaplansky.pointAugmentation line 59
def OAI.Kaplansky.pointHomology line 64
Source documentation
The actual integral H₀ class of a point, expressed as a map out of ℤ.
```
def pointHomology (X : TopCat.{0}) (x : X) :
    ModuleCat.of ℤ ℤ ⟶ (integralSingularHomology 0).obj X :=
…
```
Mentions: OAI.Kaplansky.integralSingularHomology
theorem OAI.Kaplansky.pointHomology_component line 71
theorem OAI.Kaplansky.pointHomology_map line 82
theorem OAI.Kaplansky.pointHomology_eq_of_joined line 97
Source documentation
Points in the same path component give equal integral H₀ classes.
```
theorem pointHomology_eq_of_joined (X : TopCat.{0}) {x y : X} (h : Joined x y) :
    pointHomology X x = pointHomology X y := by
…
```
Mentions: OAI.Kaplansky.pointHomology
theorem OAI.Kaplansky.pointHomology_ne_of_not_joined line 105
Source documentation
Distinct path components are separated by the actual integral H₀ class.
```
theorem pointHomology_ne_of_not_joined (X : TopCat.{0}) {x y : X}
    (h : ¬ Joined x y) : pointHomology X x ≠ pointHomology X y := by
…
```
Mentions: OAI.Kaplansky.pointHomology
theorem OAI.Kaplansky.pointHomology_hom_ext line 127
Source documentation
All actual H₀ classes are determined by their values on point classes.
```
theorem pointHomology_hom_ext (X : TopCat.{0}) {T : ModuleCat.{0} ℤ}
    {f g : (integralSingularHomology 0).obj X ⟶ T}
    (h : ∀ x, pointHomology X x ≫ f = pointHomology X x ≫ g) : f = g := by
…
```
Mentions: OAI.Kaplansky.integralSingularHomology, OAI.Kaplansky.pointHomology
def OAI.Kaplansky.componentCoefficient line 143
Source documentation
The integral coefficient of one specified path component.
```
def componentCoefficient (X : TopCat.{0}) (a : X) :
    (integralSingularHomology 0).obj X ⟶ ModuleCat.of ℤ ℤ := by
…
```
Mentions: OAI.Kaplansky.integralSingularHomology
theorem OAI.Kaplansky.pointHomology_coefficient_self line 150
theorem OAI.Kaplansky.pointHomology_coefficient_other line 155
theorem OAI.Kaplansky.pointHomology_augmentation line 165
Source documentation
The augmentation takes each integral point class to one.
```
theorem pointHomology_augmentation (X : TopCat.{0}) (a : X) :
    pointHomology X a ≫ pointAugmentation X = 𝟙 _ := by
…
```
Mentions: OAI.Kaplansky.pointHomology, OAI.Kaplansky.pointAugmentation
theorem OAI.Kaplansky.twoComponent_decomposition line 174
Source documentation
For a space with exactly these two path components, their two point classes span all integral H₀, with canonical integral coefficients.
```
theorem twoComponent_decomposition (X : TopCat.{0}) (a b : X) (hab : ¬ Joined a b)
    (hcover : ∀ x : X, Joined x a ∨ Joined x b) :
    componentCoefficient X a ≫ pointHomology X a +
      componentCoefficient X b ≫ pointHomology X b = 𝟙 _ := by
…
```
Mentions: OAI.Kaplansky.componentCoefficient, OAI.Kaplansky.pointHomology
theorem OAI.Kaplansky.twoComponent_decomposition_apply line 187
theorem OAI.Kaplansky.additiveFunctor_biprod_detect_zero line 201

theorem OAI.Kaplansky.homology_biprod_detect_zero line 215

Source documentation

Homology of a biproduct is jointly detected by its two projections.

theorem homology_biprod_detect_zero {C D : ChainComplex (ModuleCat.{0} ℤ) ℕ}
    {T : ModuleCat.{0} ℤ} (n : ℕ) (f : T ⟶ (C ⊞ D).homology n)
    (h₁ : f ≫ homologyMap biprod.fst n = 0)
    (h₂ : f ≫ homologyMap biprod.snd n = 0) : f = 0 := by
…

theorem OAI.Kaplansky.pointDifference_mayerVietoris_zero line 226
Source documentation
A difference of two point classes in the intersection is killed by both inclusion maps when both cover members are path connected.
```
theorem pointDifference_mayerVietoris_zero [PathConnectedSpace U] [PathConnectedSpace V]
    (a b : ↥(U ∩ V)) :
    (pointHomology (TopCat.of ↥(U ∩ V)) a - pointHomology (TopCat.of ↥(U ∩ V)) b) ≫
      homologyMap (smallMayerVietorisSequence U V).f 0 = 0 := by
…
```
Mentions: OAI.Kaplansky.pointHomology, OAI.Kaplansky.smallMayerVietorisSequence

theorem OAI.Kaplansky.openCover_homologyOne_nonzero line 252

Source documentation

Two distinct path components in the intersection of a path-connected open cover produce a genuinely nonzero integral H₁ class.

theorem openCover_homologyOne_nonzero [PathConnectedSpace U] [PathConnectedSpace V]
    (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ)
    (a b : ↥(U ∩ V)) (hab : ¬ Joined a b) :
    ∃ z : (integralSingularHomology 1).obj (TopCat.of X), z ≠ 0 := by
…

Mentions: OAI.Kaplansky.integralSingularHomology

theorem OAI.Kaplansky.twoComponent_inclusion_augmentation line 285

Source documentation

The two intersection coefficients sum to the augmentation after inclusion.

theorem twoComponent_inclusion_augmentation (a b : ↥(U ∩ V)) (hab : ¬ Joined a b)
    (hcover : ∀ x : ↥(U ∩ V), Joined x a ∨ Joined x b) :
    componentCoefficient (TopCat.of ↥(U ∩ V)) a + componentCoefficient (TopCat.of ↥(U ∩ V)) b =
      (integralSingularHomology 0).map
        (subspaceInclusionOfLE (Set.inter_subset_left : U ∩ V ⊆ U)) ≫
        pointAugmentation (TopCat.of U) := by
…

Mentions: OAI.Kaplansky.componentCoefficient, OAI.Kaplansky.integralSingularHomology, OAI.Kaplansky.subspaceInclusionOfLE, OAI.Kaplansky.pointAugmentation

theorem OAI.Kaplansky.twoComponent_mayerVietoris_kernel line 301

Source documentation

Elements killed by the intersection-to-sum map have opposite coefficients.

theorem twoComponent_mayerVietoris_kernel (a b : ↥(U ∩ V)) (hab : ¬ Joined a b)
    (hcover : ∀ x : ↥(U ∩ V), Joined x a ∨ Joined x b)
    (z : (integralSingularHomology 0).obj (TopCat.of ↥(U ∩ V)))
    (hz : homologyMap (smallMayerVietorisSequence U V).f 0 z = 0) :
    componentCoefficient (TopCat.of ↥(U ∩ V)) a z +
      componentCoefficient (TopCat.of ↥(U ∩ V)) b z = 0 := by
…

Mentions: OAI.Kaplansky.integralSingularHomology, OAI.Kaplansky.smallMayerVietorisSequence, OAI.Kaplansky.componentCoefficient

def OAI.Kaplansky.smallMayerVietorisOneCoordinate line 329
Source documentation
The coefficient of the first intersection component after the actual Mayer–Vietoris boundary. This fixes an integral sign convention.
```
def smallMayerVietorisOneCoordinate (a : ↥(U ∩ V)) :
    (smallSingularChains U V).homology 1 ⟶ ModuleCat.of ℤ ℤ :=
…
```
Mentions: OAI.Kaplansky.smallSingularChains
theorem OAI.Kaplansky.smallMayerVietorisOneCoordinate_bijective line 335
Source documentation
Exact integral H₁ calculation for two contractible sets whose intersection has exactly two path components. No homology or normalization premise.
```
theorem smallMayerVietorisOneCoordinate_bijective [ContractibleSpace U] [ContractibleSpace V]
    (a b : ↥(U ∩ V)) (hab : ¬ Joined a b)
    (hcover : ∀ x : ↥(U ∩ V), Joined x a ∨ Joined x b) :
    Function.Bijective (smallMayerVietorisOneCoordinate U V a) := by
…
```
Mentions: OAI.Kaplansky.smallMayerVietorisOneCoordinate
def OAI.Kaplansky.smallMayerVietorisOneIso line 372

def OAI.Kaplansky.openCoverMayerVietorisOneIso line 381

Source documentation

Full integral H₁ with the sign fixed by the ordered two intersection components.

def openCoverMayerVietorisOneIso [ContractibleSpace U] [ContractibleSpace V]
    (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ)
    (a b : ↥(U ∩ V)) (hab : ¬ Joined a b)
    (hcover : ∀ x : ↥(U ∩ V), Joined x a ∨ Joined x b) :
    (integralSingularHomology 1).obj (TopCat.of X) ≅ ModuleCat.of ℤ ℤ :=
…

Mentions: OAI.Kaplansky.integralSingularHomology

theorem OAI.Kaplansky.integralHomologyZero_map_injective line 393
Source documentation
An inclusion (indeed any map) from a path-connected space is injective on integral H₀. The augmentation provides an explicit left inverse.
```
theorem integralHomologyZero_map_injective {A X : TopCat.{0}}
    [PathConnectedSpace A] (f : A ⟶ X) :
    Function.Injective ((integralSingularHomology 0).map f) := by
…
```
Mentions: OAI.Kaplansky.integralSingularHomology
theorem OAI.Kaplansky.openCover_homologyOne_isZero line 415
Source documentation
Two contractible open sets with path-connected intersection have zero integral H₁. The connected-intersection hypothesis is essential.
```
theorem openCover_homologyOne_isZero [ContractibleSpace U] [ContractibleSpace V]
    [PathConnectedSpace ↥(U ∩ V)]
    (hU : IsOpen U) (hV : IsOpen V) (hUV : U ∪ V = Set.univ) :
    IsZero ((integralSingularHomology 1).obj (TopCat.of X)) := by
…
```
Mentions: OAI.Kaplansky.integralSingularHomology
theorem OAI.Kaplansky.relativeHomologyBoundary_zero_connected line 450
Source documentation
A connected removed subspace makes the degree-one connecting map zero.
```
theorem relativeHomologyBoundary_zero_connected {A X : TopCat.{0}}
    (i : A ⟶ X) [Mono i] [PathConnectedSpace A] :
    relativeHomologyBoundary i 0 = 0 := by
…
```
Mentions: OAI.Kaplansky.relativeHomologyBoundary
theorem OAI.Kaplansky.relativeHomologyOne_isZero line 461
Source documentation
A connected subspace of a contractible ambient space has zero relative H₁.
```
theorem relativeHomologyOne_isZero {A X : TopCat.{0}} (i : A ⟶ X) [Mono i]
    [PathConnectedSpace A] [ContractibleSpace X] :
    IsZero (relativeSingularHomology i 1) := by
…
```
Mentions: OAI.Kaplansky.relativeSingularHomology
def OAI.Kaplansky.contractibleSubspaceLocalizationOneIso line 476
Source documentation
The contractible-subspace localization theorem also holds in degree one; the low-degree proof uses H₀ injectivity, not a false H₀ vanishing claim.
```
def contractibleSubspaceLocalizationOneIso {A X : TopCat.{0}}
    (i : A ⟶ X) [Mono i] [ContractibleSpace A] :
    (integralSingularHomology 1).obj X ≅ relativeSingularHomology i 1 := by
…
```
Mentions: OAI.Kaplansky.integralSingularHomology, OAI.Kaplansky.relativeSingularHomology
theorem OAI.Kaplansky.contractibleSubspaceLocalizationOneIso_hom line 493
theorem OAI.Kaplansky.relativeHomologyZero_isZero line 499
Source documentation
Relative H₀ vanishes if the ambient space is path connected and the removed subspace is nonempty.
```
theorem relativeHomologyZero_isZero {A X : TopCat.{0}} (i : A ⟶ X)
    [PathConnectedSpace X] [Nonempty A] :
    IsZero (relativeSingularHomology i 0) := by
…
```
Mentions: OAI.Kaplansky.relativeSingularHomology