Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-05-16 13:10
bb4ae7cd
View on Github →
feat: port CategoryTheory.Endofunctor.Algebra (
#3541
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/CategoryTheory/Endofunctor/Algebra.lean
added
def
CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.counitIso
added
def
CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.unitIso
added
theorem
CategoryTheory.Endofunctor.Adjunction.Algebra.homEquiv_naturality_str
added
def
CategoryTheory.Endofunctor.Adjunction.Algebra.toCoalgebraOf
added
theorem
CategoryTheory.Endofunctor.Adjunction.Coalgebra.homEquiv_naturality_str_symm
added
def
CategoryTheory.Endofunctor.Adjunction.Coalgebra.toAlgebraOf
added
def
CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv
added
def
CategoryTheory.Endofunctor.Algebra.Hom.comp
added
def
CategoryTheory.Endofunctor.Algebra.Hom.id
added
structure
CategoryTheory.Endofunctor.Algebra.Hom
added
theorem
CategoryTheory.Endofunctor.Algebra.Initial.left_inv'
added
theorem
CategoryTheory.Endofunctor.Algebra.Initial.left_inv
added
theorem
CategoryTheory.Endofunctor.Algebra.Initial.right_inv
added
def
CategoryTheory.Endofunctor.Algebra.Initial.strInv
added
theorem
CategoryTheory.Endofunctor.Algebra.Initial.str_isIso
added
theorem
CategoryTheory.Endofunctor.Algebra.comp_eq_comp
added
theorem
CategoryTheory.Endofunctor.Algebra.comp_f
added
theorem
CategoryTheory.Endofunctor.Algebra.epi_of_epi
added
def
CategoryTheory.Endofunctor.Algebra.equivOfNatIso
added
def
CategoryTheory.Endofunctor.Algebra.forget
added
def
CategoryTheory.Endofunctor.Algebra.functorOfNatTrans
added
def
CategoryTheory.Endofunctor.Algebra.functorOfNatTransComp
added
def
CategoryTheory.Endofunctor.Algebra.functorOfNatTransEq
added
def
CategoryTheory.Endofunctor.Algebra.functorOfNatTransId
added
theorem
CategoryTheory.Endofunctor.Algebra.id_eq_id
added
theorem
CategoryTheory.Endofunctor.Algebra.id_f
added
def
CategoryTheory.Endofunctor.Algebra.isoMk
added
theorem
CategoryTheory.Endofunctor.Algebra.iso_of_iso
added
theorem
CategoryTheory.Endofunctor.Algebra.mono_of_mono
added
structure
CategoryTheory.Endofunctor.Algebra
added
def
CategoryTheory.Endofunctor.Coalgebra.Hom.comp
added
def
CategoryTheory.Endofunctor.Coalgebra.Hom.id
added
structure
CategoryTheory.Endofunctor.Coalgebra.Hom
added
theorem
CategoryTheory.Endofunctor.Coalgebra.comp_eq_comp
added
theorem
CategoryTheory.Endofunctor.Coalgebra.comp_f
added
theorem
CategoryTheory.Endofunctor.Coalgebra.epi_of_epi
added
def
CategoryTheory.Endofunctor.Coalgebra.equivOfNatIso
added
def
CategoryTheory.Endofunctor.Coalgebra.forget
added
def
CategoryTheory.Endofunctor.Coalgebra.functorOfNatTrans
added
def
CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransComp
added
def
CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransEq
added
def
CategoryTheory.Endofunctor.Coalgebra.functorOfNatTransId
added
theorem
CategoryTheory.Endofunctor.Coalgebra.id_eq_id
added
theorem
CategoryTheory.Endofunctor.Coalgebra.id_f
added
def
CategoryTheory.Endofunctor.Coalgebra.isoMk
added
theorem
CategoryTheory.Endofunctor.Coalgebra.iso_of_iso
added
theorem
CategoryTheory.Endofunctor.Coalgebra.mono_of_mono
added
structure
CategoryTheory.Endofunctor.Coalgebra