Coalgebra

📁 Source: Mathlib/Analysis/InnerProductSpace/Coalgebra.lean

Statistics

Metric	Count
Definitions Coalgebra, Coalgebra, Coalgebra, algebraOfCoalgebra, coalgebraOfAlgebra, mulOfCoalgebra, ringOfCoalgebra	7
Theorems mul_def, comul_eq_adjoint, counit_eq_adjoint	3
Total	10

CategoryTheory.Comonad

Definitions

Name	Category	Theorems
Coalgebra 📖	CompData	83 math math: CategoryTheory.Adjunction.adjToComonadIso_inv_toNatTrans_app, comparison_faithful_of_faithful, CategoryTheory.ComonadicLeftAdjoint.eqv, CategoryTheory.comp_comparison_hasColimit, comparison_obj_a, beckCoalgebraFork_pt, ForgetCreatesColimits'.liftedCocone_pt, ForgetCreatesLimits'.liftedCone_π_app_f, Coalgebra.comp_f, CofreeEqualizer.topMap_f, forget_map, ForgetCreatesLimits'.γ_app, CategoryTheory.coalgebraEquivOver_functor, forget_faithful, CategoryTheory.comp_comparison_forget_hasColimit, ForgetCreatesColimits'.newCocone_ι_app, instIsCoreflexivePairCoalgebraTopMapBottomMap, CategoryTheory.Coreflective.comparison_full, ForgetCreatesLimits'.newCone_pt, cofree_obj_A, ComonadicityInternal.comparisonAdjunction_counit_f, Coalgebra.id_eq_id, coalgebraPreadditive_homGroup_neg_f, Coalgebra.isoMk_hom_f, coalgebra_iso_of_iso, CategoryTheory.instEssSurjCoalgebraToComonadAdjComparison, cofree_map_f, ForgetCreatesColimits'.γ_app, comparisonForget_inv_app, CategoryTheory.Adjunction.adjToComonadIso_hom_toNatTrans_app, CategoryTheory.overToCoalgebra_map_f, adj_counit, comparisonForget_hom_app, ForgetCreatesLimits'.newCone_π, CategoryTheory.coalgebraToOver_obj, left_comparison, CategoryTheory.coalgebraEquivOver_counitIso, coalgebraPreadditive_homGroup_nsmul_f, CategoryTheory.instIsEquivalenceCoalgebraToComonadComonadicAdjunctionComparison, comparison_map_f, CofreeEqualizer.ι_f, CategoryTheory.Over.star_map_left, cofree_obj_a, ForgetCreatesColimits'.coconePoint_a, ComonadicityInternal.comparisonRightAdjointHomEquiv_symm_apply_f, coalgebraPreadditive_homGroup_zsmul_f, CategoryTheory.overToCoalgebra_obj_A, forget_obj, forget_creates_limits_of_comonad_preserves, CategoryTheory.coalgebraToOver_map, ForgetCreatesColimits'.liftedCoconeIsColimit_desc_f, Coalgebra.id_f, ForgetCreatesLimits'.conePoint_A, comparison_obj_A, ForgetCreatesColimits'.coconePoint_A, forget_additive, CategoryTheory.coalgebraEquivOver_inverse, CategoryTheory.overToCoalgebra_obj_a, CofreeEqualizer.condition, ComonadicityInternal.comparisonAdjunction_counit, Coalgebra.comp_eq_comp, Coalgebra.isoMk_inv_f, CategoryTheory.coalgebraEquivOver_unitIso, algebra_epi_of_epi, ForgetCreatesLimits'.commuting, algebra_mono_of_mono, CofreeEqualizer.bottomMap_f, coalgebraPreadditive_homGroup_add_f, coalgebraPreadditive_homGroup_sub_f, ComonadicityInternal.comparisonAdjunction_unit_app, ForgetCreatesLimits'.liftedConeIsLimit_lift_f, ForgetCreatesColimits'.liftedCocone_ι_app_f, ComonadicityInternal.comparisonAdjunction_counit_f_aux, adj_unit, beckCoalgebraFork_π_app, instIsLeftAdjointCoalgebraForget, CategoryTheory.instFullCoalgebraToComonadAdjComparison, ComonadicityInternal.comparisonRightAdjointHomEquiv_apply, coalgebraPreadditive_homGroup_zero_f, forget_reflects_iso, ForgetCreatesLimits'.liftedCone_pt, hasColimit_of_comp_forget_hasColimit, CategoryTheory.Coreflective.comparison_essSurj

CategoryTheory.Endofunctor

Definitions

Name	Category	Theorems
Coalgebra 📖	CompData	54 math math: Coalgebra.id_f, Coalgebra.functorOfNatTransComp_inv_app_f, Adjunction.algebraCoalgebraEquiv_unitIso_hom_app_f, Adjunction.algebraCoalgebraEquiv_inverse_obj_str, Coalgebra.equivOfNatIso_inverse, Coalgebra.forget_faithful, Coalgebra.comp_eq_comp, Coalgebra.functorOfNatTrans_obj_str, coalgebraPreadditive_homGroup_sub_f, coalgebraPreadditive_homGroup_zero_f, coalgebraPreadditive_homGroup_neg_f, Coalgebra.id_eq_id, Adjunction.algebraCoalgebraEquiv_inverse_obj_a, Adjunction.AlgCoalgEquiv.counitIso_inv_app_f, Coalgebra.forget_map, Coalgebra.functorOfNatTransId_inv_app_f, Coalgebra.equivOfNatIso_counitIso, Coalgebra.isoMk_hom_f, Adjunction.algebraCoalgebraEquiv_functor_map_f, Adjunction.AlgCoalgEquiv.unitIso_inv_app_f, Adjunction.algebraCoalgebraEquiv_counitIso_inv_app_f, Coalgebra.iso_of_iso, Coalgebra.isoMk_inv_f, Adjunction.algebraCoalgebraEquiv_unitIso_inv_app_f, coalgebraPreadditive_homGroup_zsmul_f, Adjunction.AlgCoalgEquiv.counitIso_hom_app_f, Coalgebra.equivOfNatIso_unitIso, Coalgebra.functorOfNatTransEq_hom_app_f, Adjunction.algebraCoalgebraEquiv_functor_obj_V, Adjunction.Coalgebra.toAlgebraOf_obj_a, Adjunction.algebraCoalgebraEquiv_counitIso_hom_app_f, Coalgebra.equivOfNatIso_functor, Coalgebra.forget_obj, Coalgebra.functorOfNatTrans_obj_V, Adjunction.Algebra.toCoalgebraOf_obj_V, CategoryTheory.Coalgebra.forget_additive, Coalgebra.epi_of_epi, Adjunction.Algebra.toCoalgebraOf_map_f, Adjunction.algebraCoalgebraEquiv_functor_obj_str, Adjunction.Algebra.toCoalgebraOf_obj_str, Coalgebra.functorOfNatTransId_hom_app_f, Coalgebra.mono_of_mono, Adjunction.Coalgebra.toAlgebraOf_obj_str, coalgebraPreadditive_homGroup_add_f, Adjunction.AlgCoalgEquiv.unitIso_hom_app_f, Coalgebra.functorOfNatTransEq_inv_app_f, Coalgebra.Terminal.right_inv', coalgebraPreadditive_homGroup_nsmul_f, Adjunction.algebraCoalgebraEquiv_inverse_map_f, Coalgebra.functorOfNatTrans_map_f, Coalgebra.functorOfNatTransComp_hom_app_f, Coalgebra.comp_f, Adjunction.Coalgebra.toAlgebraOf_map_f, Coalgebra.forget_reflects_iso

InnerProductSpace

Definitions

Name	Category	Theorems
algebraOfCoalgebra 📖	CompOp	—
coalgebraOfAlgebra 📖	CompOp	—
mulOfCoalgebra 📖	CompOp	1 math math: AlgebraOfCoalgebra.mul_def
ringOfCoalgebra 📖	CompOp	—

InnerProductSpace.AlgebraOfCoalgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mul_def 📖	mathematical	—	InnerProductSpace.mulOfCoalgebra DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring TensorProduct Semifield.toCommSemiring ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace TensorProduct.instNormedAddCommGroup TensorProduct.instInnerProductSpace LinearMap.instFunLike LinearEquiv CommSemiring.toSemiring starRingEnd RCLike.toStarRing RingHomInvPair.instStarRingEnd LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.adjoint Module.Finite.tensorProduct CoalgebraStruct.comul Coalgebra.toCoalgebraStruct TensorProduct.tmul	—	—

Pi

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comul_eq_adjoint 📖	mathematical	—	CoalgebraStruct.comul Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Function.module DivisionSemiring.toSemiring Semifield.toDivisionSemiring NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace RCLike.innerProductSpace instCoalgebraStruct Coalgebra.toCoalgebraStruct CommSemiring.toCoalgebra LinearMap.comp TensorProduct EuclideanSpace AddCommGroup.toAddCommMonoid WithLp.instAddCommGroup ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal addCommGroup NormedAddCommGroup.toAddCommGroup WithLp.instModule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing CommSemiring.toSemiring TensorProduct.addCommMonoid TensorProduct.instModule RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids TensorProduct.map LinearEquiv.toLinearMap RingHomInvPair.ids ContinuousLinearEquiv.toLinearEquiv PiLp.topologicalSpace topologicalSpace EuclideanSpace.equiv SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup PiLp.normedAddCommGroup fact_one_le_two_ennreal PiLp.innerProductSpace DFunLike.coe LinearEquiv starRingEnd RCLike.toStarRing RingHomInvPair.instStarRingEnd LinearMap TensorProduct.instNormedAddCommGroup TensorProduct.instInnerProductSpace LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction CommRing.toRing EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.adjoint Module.Finite.tensorProduct WithLp.instModuleFinite FiniteDimensional.finiteDimensional_pi' NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Finite.of_fintype Module.instFiniteDimensionalOfIsReflexive SeminormedAddCommGroup.toAddCommGroup Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.Free.self DivisionRing.toDivisionSemiring module ContinuousLinearEquiv.symm nonUnitalNonAssocSemiring NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing LinearMap.mul' Algebra.to_smulCommClass semiring Function.algebra Algebra.id IsScalarTower.right	—	LinearMap.pi_ext' Finite.of_fintype RingHomCompTriple.ids RingHomInvPair.ids fact_one_le_two_ennreal RingHomInvPair.instStarRingEnd smulCommClass_self Module.Finite.tensorProduct WithLp.instModuleFinite FiniteDimensional.finiteDimensional_pi' Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.Free.self Algebra.to_smulCommClass IsScalarTower.right LinearMap.ext_ring comul_single single_dotProduct one_mul LinearMap.adjoint_inner_right star_mul'
counit_eq_adjoint 📖	mathematical	—	CoalgebraStruct.counit Semifield.toCommSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField addCommMonoid ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing Function.module DivisionSemiring.toSemiring Semifield.toDivisionSemiring NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace RCLike.innerProductSpace instCoalgebraStruct Coalgebra.toCoalgebraStruct CommSemiring.toCoalgebra LinearMap.comp EuclideanSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup PiLp.normedAddCommGroup ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal fact_one_le_two_ennreal PiLp.innerProductSpace RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids DFunLike.coe LinearEquiv CommSemiring.toSemiring starRingEnd RCLike.toStarRing RingHomInvPair.instStarRingEnd LinearMap LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.adjoint Module.instFiniteDimensionalOfIsReflexive SeminormedAddCommGroup.toAddCommGroup Module.instIsReflexiveOfFiniteOfProjective AddCommGroup.toAddCommMonoid FiniteDimensional.finiteDimensional_self NormedDivisionRing.toDivisionRing NormedField.toNormedDivisionRing Module.Projective.of_free Module.Free.self WithLp.instModuleFinite DivisionRing.toDivisionSemiring addCommGroup module FiniteDimensional.finiteDimensional_pi' Finite.of_fintype NormedAddCommGroup.toAddCommGroup NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring WithLp.instAddCommGroup Semiring.toModule WithLp.instModule NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring NormedRing.toRing NormedCommRing.toNormedRing LinearEquiv.toLinearMap RingHomInvPair.ids ContinuousLinearEquiv.toLinearEquiv topologicalSpace PiLp.topologicalSpace ContinuousLinearEquiv.symm EuclideanSpace.equiv Algebra.linearMap semiring Function.algebra Algebra.id	—	LinearMap.pi_ext' Finite.of_fintype fact_one_le_two_ennreal RingHomCompTriple.ids RingHomInvPair.instStarRingEnd smulCommClass_self Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.Free.self WithLp.instModuleFinite FiniteDimensional.finiteDimensional_pi' RingHomInvPair.ids LinearMap.ext_ring counit_comp_single Algebra.to_smulCommClass LinearMap.comp.congr_simp LinearMap.comp_toSpanSingleton LinearMap.adjoint_toSpanSingleton star_one single_dotProduct mul_one

(root)

Definitions

Name	Category	Theorems
Coalgebra 📖	CompData	2 math math: CoalgCat.tensorUnit_instCoalgebra, CoalgCat.tensorObj_instCoalgebra

---

← Back to Index