Commit 2023-04-22 01:34 b53dd023

View on Github →

feat: port AlgebraicTopology.DoldKan.FunctorGamma (#3566)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicTopology/DoldKan/FunctorGamma.lean

added theorem AlgebraicTopology.DoldKan.HigherFacesVanish.on_Γ₀_summand_id

added theorem AlgebraicTopology.DoldKan.Isδ₀.eq_δ₀

added theorem AlgebraicTopology.DoldKan.Isδ₀.iff

added def AlgebraicTopology.DoldKan.Isδ₀

added theorem AlgebraicTopology.DoldKan.PInfty_on_Γ₀_splitting_summand_eq_self

added def AlgebraicTopology.DoldKan.Γ₀'

added def AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono

added theorem AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_comp

added theorem AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_eq_zero

added theorem AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_id

added theorem AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_naturality

added theorem AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_δ₀'

added theorem AlgebraicTopology.DoldKan.Γ₀.Obj.Termwise.mapMono_δ₀

added def AlgebraicTopology.DoldKan.Γ₀.Obj.map

added theorem AlgebraicTopology.DoldKan.Γ₀.Obj.mapMono_on_summand_id

added theorem AlgebraicTopology.DoldKan.Γ₀.Obj.map_epi_on_summand_id

added theorem AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand'

added theorem AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand

added theorem AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀'

added theorem AlgebraicTopology.DoldKan.Γ₀.Obj.map_on_summand₀

added def AlgebraicTopology.DoldKan.Γ₀.Obj.obj₂

added def AlgebraicTopology.DoldKan.Γ₀.Obj.summand

added def AlgebraicTopology.DoldKan.Γ₀.map

added def AlgebraicTopology.DoldKan.Γ₀.obj

added def AlgebraicTopology.DoldKan.Γ₀.splitting

added theorem AlgebraicTopology.DoldKan.Γ₀.splitting_iso_hom_eq_id

added theorem AlgebraicTopology.DoldKan.Γ₀.splitting_map_eq_id

added def AlgebraicTopology.DoldKan.Γ₀

added def AlgebraicTopology.DoldKan.Γ₂

Modified Mathlib/AlgebraicTopology/SplitSimplicialObject.lean

added theorem SimplicialObject.Split.hom_ext