Commit 2023-04-14 12:58 6a4ba7f1

View on Github →

feat: port AlgebraicTopology.SplitSimplicialObject (#3432)

Estimated changes

Modified Mathlib.lean

Created Mathlib/AlgebraicTopology/SplitSimplicialObject.lean

added theorem SimplicialObject.Split.Hom.ext

added structure SimplicialObject.Split.Hom

added theorem SimplicialObject.Split.comp_F

added theorem SimplicialObject.Split.comp_f

added theorem SimplicialObject.Split.congr_F

added theorem SimplicialObject.Split.congr_f

added def SimplicialObject.Split.evalN

added def SimplicialObject.Split.forget

added theorem SimplicialObject.Split.id_F

added theorem SimplicialObject.Split.id_f

added def SimplicialObject.Split.mk'

added def SimplicialObject.Split.natTransιSummand

added theorem SimplicialObject.Split.ιSummand_naturality_symm

added structure SimplicialObject.Split

added def SimplicialObject.Splitting.IndexSet.EqId

added def SimplicialObject.Splitting.IndexSet.e

added def SimplicialObject.Splitting.IndexSet.epiComp

added theorem SimplicialObject.Splitting.IndexSet.eqId_iff_eq

added theorem SimplicialObject.Splitting.IndexSet.eqId_iff_len_eq

added theorem SimplicialObject.Splitting.IndexSet.eqId_iff_len_le

added theorem SimplicialObject.Splitting.IndexSet.eqId_iff_mono

added theorem SimplicialObject.Splitting.IndexSet.ext'

added theorem SimplicialObject.Splitting.IndexSet.ext

added theorem SimplicialObject.Splitting.IndexSet.fac_pull

added def SimplicialObject.Splitting.IndexSet.id

added def SimplicialObject.Splitting.IndexSet.mk

added def SimplicialObject.Splitting.IndexSet.pull

added def SimplicialObject.Splitting.IndexSet

added def SimplicialObject.Splitting.coprod

added def SimplicialObject.Splitting.desc

added theorem SimplicialObject.Splitting.hom_ext'

added theorem SimplicialObject.Splitting.hom_ext

added def SimplicialObject.Splitting.iso

added def SimplicialObject.Splitting.map

added def SimplicialObject.Splitting.ofIso

added def SimplicialObject.Splitting.summand

added def SimplicialObject.Splitting.ιCoprod

added def SimplicialObject.Splitting.ιSummand

added theorem SimplicialObject.Splitting.ιSummand_comp_app

added theorem SimplicialObject.Splitting.ιSummand_epi_naturality

added theorem SimplicialObject.Splitting.ιSummand_eq

added theorem SimplicialObject.Splitting.ιSummand_id

added theorem SimplicialObject.Splitting.ι_desc

added def SimplicialObject.Splitting.φ

added structure SimplicialObject.Splitting