Commit 2023-04-22 23:19 5b418785

View on Github →

feat: port AlgebraicTopology.DoldKan.NCompGamma (#3576)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/AlgebraicTopology/DoldKan/FunctorN.lean

added theorem AlgebraicTopology.DoldKan.compatibility_N₁_N₂

Created Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean

added theorem AlgebraicTopology.DoldKan.PInfty_comp_map_mono_eq_zero

added def AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂

added theorem AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂_hom_app

added theorem AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂_natTrans

added theorem AlgebraicTopology.DoldKan.identity_N₂

added theorem AlgebraicTopology.DoldKan.identity_N₂_objectwise

added theorem AlgebraicTopology.DoldKan.Γ₀_obj_termwise_mapMono_comp_PInfty

added def AlgebraicTopology.DoldKan.Γ₂N₁.natTrans

added def AlgebraicTopology.DoldKan.Γ₂N₁

added def AlgebraicTopology.DoldKan.Γ₂N₂.natTrans

added theorem AlgebraicTopology.DoldKan.Γ₂N₂.natTrans_app_f_app

added def AlgebraicTopology.DoldKan.Γ₂N₂