Commit 2023-04-22 16:39 0b676a27

View on Github →

feat: port AlgebraicTopology.DoldKan.GammaCompN (#3568)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicTopology/DoldKan/GammaCompN.lean

added def AlgebraicTopology.DoldKan.N₁Γ₀

added theorem AlgebraicTopology.DoldKan.N₁Γ₀_app

added theorem AlgebraicTopology.DoldKan.N₁Γ₀_hom_app

added theorem AlgebraicTopology.DoldKan.N₁Γ₀_hom_app_f_f

added theorem AlgebraicTopology.DoldKan.N₁Γ₀_inv_app

added theorem AlgebraicTopology.DoldKan.N₁Γ₀_inv_app_f_f

added def AlgebraicTopology.DoldKan.N₂Γ₂

added def AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso

added theorem AlgebraicTopology.DoldKan.N₂Γ₂_compatible_with_N₁Γ₀

added theorem AlgebraicTopology.DoldKan.N₂Γ₂_inv_app_f_f

added theorem AlgebraicTopology.DoldKan.N₂Γ₂_toKaroubi

added theorem AlgebraicTopology.DoldKan.whiskerLeft_toKaroubi_N₂Γ₂_hom

added def AlgebraicTopology.DoldKan.Γ₀'CompNondegComplexFunctor

added def AlgebraicTopology.DoldKan.Γ₀NondegComplexIso

Modified Mathlib/AlgebraicTopology/DoldKan/SplitSimplicialObject.lean

Modified Mathlib/AlgebraicTopology/SplitSimplicialObject.lean