Commit 2023-08-06 01:46 7d39ff43

View on Github →

feat: forward port of AlgebraicTopology.DoldKan.EquivalencePseudoabelian (#6293)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicTopology/DoldKan/EquivalencePseudoabelian.lean

added def CategoryTheory.Idempotents.DoldKan.N

added def CategoryTheory.Idempotents.DoldKan.equivalence

added theorem CategoryTheory.Idempotents.DoldKan.equivalence_counitIso

added theorem CategoryTheory.Idempotents.DoldKan.equivalence_functor

added theorem CategoryTheory.Idempotents.DoldKan.equivalence_inverse

added theorem CategoryTheory.Idempotents.DoldKan.equivalence_unitIso

added theorem CategoryTheory.Idempotents.DoldKan.hN₁

added theorem CategoryTheory.Idempotents.DoldKan.hΓ₀

added theorem CategoryTheory.Idempotents.DoldKan.hε

added theorem CategoryTheory.Idempotents.DoldKan.hη

added def CategoryTheory.Idempotents.DoldKan.Γ

added def CategoryTheory.Idempotents.DoldKan.ε

added def CategoryTheory.Idempotents.DoldKan.η

Modified Mathlib/AlgebraicTopology/DoldKan/NCompGamma.lean

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

Modified Mathlib/CategoryTheory/Functor/Category.lean