← all areas

Namespace Bialgebra 19 theorems

• Algebra maps multiplicative on points are bialgebra maps Bialgebra.exists_bialgHom_coe_eq_of_comp_convMul 0 below · cited by 2 · depth 15
• Base change of bialgebra points, compatibly with convolution Bialgebra.bijective_convMul_comp_includeRight_baseChange 0 below · cited by 1 · depth 17
• Bialgebra with basis of powers of a group-like element is R[ℤ/n] Bialgebra.nonempty_bialgEquiv_monoidAlgebra_of_basis_pow_of_comul_eq_tmul_self 0 below · cited by 1 · depth 17
• Comultiplication-compatible algebra isomorphisms preserve the counit Bialgebra.counit_comp_algEquiv_of_comul_compat 0 below · cited by 2 · depth 20
• Counit equals 1 at exactly one of a complete orthogonal idempotent family Bialgebra.existsUnique_counit_apply_eq_one_of_completeOrthogonalIdempotents 0 below · cited by 2 · depth 22
• Cotangent module at the unit of a bialgebra commutes with base change Bialgebra.exists_linearEquiv_baseChange_cotangent_ker_counit_comp_baseChange_mapCotangent_eq 0 below · cited by 2 · depth 22
• Pushout of two surjections of commutative bialgebras Bialgebra.exists_surjective_bialgHom_ker_eq_map_ker 0 below · cited by 1 · depth 22
• Unique bialgebra lift of maps from a formally étale bialgebra Bialgebra.existsUnique_bialgHom_baseChange_eq_zmodp 4 below · cited by 2 · depth 23
• Tangent vectors at the counit as linear forms on I/I² Bialgebra.exists_equiv_algHom_dualNumber_over_counit_linearMap_cotangent_ker_counitAlgHom 0 below · cited by 1 · depth 23
• Base change of k[ε]-points over the counit Bialgebra.exists_equiv_withConv_algHom_dualNumber_over_counit_baseChange_apply_one_tmul 0 below · cited by 1 · depth 23
• Convolution of two dual-number points over the counit lies over the counit Bialgebra.fst_mul_withConv_algHom_dualNumber_eq_counit 0 below · cited by 1 · depth 23
• Convolution of k[ε]-points over the counit adds ε-components Bialgebra.snd_mul_withConv_algHom_dualNumber_eq_add 0 below · cited by 1 · depth 23
• Triviality of a bialgebra with id=(F∘ a)*(b∘ V) Bialgebra.eq_algebraMap_counit_of_id_eq_convMul_of_pow_eq 0 below · cited by 1 · depth 27
• Bialgebra maps killing an augmentation ideal factor through a quotient Bialgebra.exists_eq_comp_of_comp_eq_counit_of_ker_eq_map 0 below · cited by 1 · depth 27
• Transporting an Fa * bV convolution identity to a bialgebra retract Bialgebra.exists_id_eq_convMul_of_retract 0 below · cited by 1 · depth 27
• Naturality of the splitting C ≅ A ⊗ A given by two bialgebra maps Bialgebra.bialgEquiv_comp_eq_tensorProduct_map_comp_of_productMap 0 below · cited by 1 · depth 29
• Surjectivity and a dimension count split C as A⊗_k A Bialgebra.exists_bialgEquiv_tensorProduct_of_surjective_productMap_of_finrank_eq 0 below · cited by 1 · depth 29
• Cancelling an intermediate base change of a bialgebra Bialgebra.exists_bialgEquiv_cancelBaseChange_tmul 0 below · cited by 1 · depth 30
• Base change of a bialgebra cokernel along R → S Bialgebra.exists_bialgEquiv_comp_eq_tensorProduct_map_of_surjective_of_ker_eq_map_ker_counit 0 below · cited by 2 · depth 30