Mathlib Changelog
v4
Changelog
About
Github
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