← all areas

Namespace HopfOrder 23 theorems

• Points of a Hopf order agree with generic-fibre points HopfOrder.exists_equiv_algHom_apply_eq_and_toConv_mul 0 below · cited by 1 · depth 13
• Image of an integral Hopf algebra in a generic fibre HopfOrder.finite_and_comul_mem_and_antipode_mem_and_counit_mem_range_comp_includeRight 0 below · cited by 2 · depth 13
• Rank of an R-order equals the K-dimension it spans HopfOrder.finrank_eq_finrank 0 below · cited by 3 · depth 13
• Rank of a Hopf order multiplies along a Hopf quotient HopfOrder.finrank_eq_finrank_comap_hopfKer_mul_finrank_map 21 below · cited by 1 · depth 13
• Hopf order conditions pass to the Hopf kernel HopfOrder.isHopfOrder_comap_hopfKer 0 below · cited by 3 · depth 13
• Image of a Hopf order under a surjective Hopf quotient HopfOrder.isHopfOrder_map 0 below · cited by 6 · depth 13
• A module-finite subalgebra lies in the integral closure HopfOrder.le_integralClosure_of_finite 0 below · cited by 2 · depth 18
• Antipode-stability passes to the join of two subalgebras HopfOrder.antipode_mem_sup 0 below · cited by 2 · depth 20
• Join of two comultiplication-stable R-subalgebras HopfOrder.comul_mem_range_sup 0 below · cited by 2 · depth 20
• Counit integrality is preserved by joins of subalgebras HopfOrder.counit_mem_range_sup 0 below · cited by 2 · depth 20
• Join of two module-finite K-spanning orders HopfOrder.finite_sup_and_span_sup_eq_top 0 below · cited by 2 · depth 20
• A generically surjective bialgebra map yields a Hopf order HopfOrder.isHopfOrder_range_includeRight_comp_of_surjective_baseChange 0 below · cited by 2 · depth 20
• Nested Hopf orders agreeing on a Hopf kernel and its quotient HopfOrder.eq_of_le_of_comap_hopfKer_eq_of_map_eq 6 below · cited by 1 · depth 25
• Existence of a greatest Hopf order HopfOrder.exists_isGreatest 7 below · cited by 2 · depth 26
• Existence of a least Hopf order via Cartier duality HopfOrder.exists_isLeast 19 below · cited by 1 · depth 26
• Bialgebra automorphisms preserve a least Hopf order HopfOrder.map_eq_of_forall_ge 1 below · cited by 1 · depth 26
• The greatest Hopf order is stable under bialgebra automorphisms HopfOrder.map_eq_of_forall_le 1 below · cited by 1 · depth 26
• Integral Hopf kernel is the trace of the generic one HopfOrder.map_hopfKer_eq_inf_hopfKer 0 below · cited by 1 · depth 26
• Dual of a Hopf order is a Hopf order of the Cartier dual HopfOrder.exists_dual_hopfOrder 0 below · cited by 1 · depth 27
• A sup-closed bounded family of subalgebras has a greatest member HopfOrder.exists_greatest_of_sup_closed_of_le_noetherian 0 below · cited by 1 · depth 27
• The predual of a Hopf order of the Cartier dual HopfOrder.exists_predual_hopfOrder 0 below · cited by 1 · depth 27
• Finiteness of the integral closure in an étale algebra HopfOrder.integralClosure_finite_of_etale 0 below · cited by 1 · depth 27
• Integrality against the dual lattice forces membership HopfOrder.mem_of_forall_mem_dual_apply_mem_range 0 below · cited by 1 · depth 27