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