OAI/AlgebraicTopology/Integral/Contraction.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FiniteIntegralContraction.rowEval line 17
2. def OAI.FiniteIntegralContraction.rowsMap line 20
3. theorem OAI.FiniteIntegralContraction.rowsMap_apply line 23
4. def OAI.FiniteIntegralContraction.matrixMap line 30
5. theorem OAI.FiniteIntegralContraction.matrixMap_single line 33
6. theorem OAI.FiniteIntegralContraction.map_eq_of_single line 39
7. theorem OAI.FiniteIntegralContraction.exactness line 47

   Source documentation

   A checked integral contraction in degrees 0,1,2 gives both exactness and injectivity of the two-dimensional boundary.

   theorem exactness [Fintype I] [Fintype J] [Fintype K]
       (d₁ : (J → ℤ) →ₗ[ℤ] (I → ℤ)) (d₂ : (K → ℤ) →ₗ[ℤ] (J → ℤ))
       (h₀ : (I → ℤ) →ₗ[ℤ] (J → ℤ)) (h₁ : (J → ℤ) →ₗ[ℤ] (K → ℤ))
       (hleft : ∀ i, h₁ (d₂ (Pi.single i 1)) = Pi.single i 1)
       (hmid : ∀ j, d₂ (h₁ (Pi.single j 1)) + h₀ (d₁ (Pi.single j 1)) = Pi.single j 1) :
       Function.Injective d₂ ∧ ∀ c, d₁ c = 0 → ∃ b, d₂ b = c := by
   …

8. theorem OAI.FiniteIntegralContraction.rows_single_one line 72
9. theorem OAI.FiniteIntegralContraction.rows_single_two line 81
10. theorem OAI.FiniteIntegralContraction.certificate_bottom line 92
11. theorem OAI.FiniteIntegralContraction.certificate_left line 100
12. theorem OAI.FiniteIntegralContraction.certificate_middle line 110
13. def OAI.FiniteIntegralContraction.sumCoordinates line 127
14. theorem OAI.FiniteIntegralContraction.sumCoordinates_single line 132
15. def OAI.FiniteIntegralContraction.rootCoordinates line 135
16. theorem OAI.FiniteIntegralContraction.rootCoordinates_one line 139
17. def OAI.FiniteIntegralContraction.corrected line 142
18. theorem OAI.FiniteIntegralContraction.middle_of_rank line 148

    Source documentation

    A stable rank equality turns a checked split boundary and a checked bottom contraction into the full middle identity. This avoids a large redundant finite matrix certificate; no rational exactness is substituted for integer exactness.

    theorem middle_of_rank
        (card : Fintype.card J + 1 = Fintype.card K + Fintype.card I)
        (root : I) (d₁ : (J → ℤ) →ₗ[ℤ] (I → ℤ)) (d₂ : (K → ℤ) →ₗ[ℤ] (J → ℤ))
        (h₀ : (I → ℤ) →ₗ[ℤ] (J → ℤ)) (h₁ : (J → ℤ) →ₗ[ℤ] (K → ℤ))
        (hd : ∀ t, d₁ (d₂ (Pi.single t 1)) = 0)
        (hb : ∀ i, d₁ (h₀ (Pi.single i 1)) = Pi.single i 1 - Pi.single root 1)
        (hl : ∀ t, h₁ (d₂ (Pi.single t 1)) = Pi.single t 1) :
        (∀ t, corrected d₁ h₀ h₁ (d₂ (Pi.single t 1)) = Pi.single t 1) ∧
        (∀ j, d₂ (corrected d₁ h₀ h₁ (Pi.single j 1)) + h₀ (d₁ (Pi.single j 1)) = Pi.single j 1) := by
    …

    Mentions: OAI.FiniteIntegralContraction.corrected