← all areas

Namespace HopfAlgebra 333 theorems

— 326 · FVect 4 · FVectStructure 1 · Raynaud 2

directly in HopfAlgebra 326

• Finite free Hopf quotient of a finite Hopf algebra over a PID HopfAlgebra.exists_finite_free_quotient_bialgHom 0 below · cited by 2 · depth 9
• Points of a tensor product of Hopf algebras HopfAlgebra.exists_withConv_tensorProduct_equiv_prod 0 below · cited by 2 · depth 11
• Flat finite-type ℤ-Hopf algebra with one ℚ̄-point is ℤ HopfAlgebra.nonempty_algEquiv_int_of_subsingleton_ringHom_algebraicClosure_rat 7 below · cited by 2 · depth 11
• Reduction is injective on ℓ-power points when ℓ is a uniformiser HopfAlgebra.point_eq_one_of_pow_prime_pow_eq_one_of_sub_counit_mem_maximalIdeal 0 below · cited by 6 · depth 11
• Constant and multiplicative rank-q Hopf algebra models HopfAlgebra.exists_constant_and_rootsOfUnity_models_of_rank 0 below · cited by 9 · depth 12
• Finite flat Hopf models multiply over a finite index set HopfAlgebra.exists_finiteFlat_pi 1 below · cited by 4 · depth 12
• Integral model of an inertia-stable step HopfAlgebra.exists_model_points_genericFibre_of_finite_flat_of_inertiaStable_step 35 below · cited by 2 · depth 12
• Flat Hopf quotients cutting out a Galois-stable chain of points HopfAlgebra.exists_quotientFlag_of_galoisStableChain 0 below · cited by 5 · depth 12
• Bialgebra maps induce morphisms of fppf point sheaves HopfAlgebra.exists_sheafHom_sectionsEquiv_algHom_comp_of_bialgHom 0 below · cited by 2 · depth 12
• Points of a ℤ-Hopf algebra as an fppf sheaf HopfAlgebra.exists_sheaf_smallFppfTopology_specInt_sectionsEquiv_algHom 0 below · cited by 3 · depth 12
• Cocommutativity from an abelian convolution group of Ω-points HopfAlgebra.isCocomm_of_isReduced_baseChange_of_withConv_equiv 1 below · cited by 2 · depth 12
• Cartier's theorem: Hopf algebras of finite type in characteristic zero are reduced HopfAlgebra.isReduced_of_finiteType_of_charZero 6 below · cited by 28 · depth 12
• Points of a commutative Hopf algebra form a group HopfAlgebra.isUnit_withConv_algHom 0 below · cited by 10 · depth 12
• Rigidity for bialgebras with étale Cartier dual HopfAlgebra.bialgHom_apply_eq_algebraMap_counit_of_etale_cartierDual_of_sub_mem_map_maximalIdeal 0 below · cited by 4 · depth 13
• Galois descent for a D-stable monoid of points HopfAlgebra.evalQuot_bijective_of_forall_exists_comp_eq 0 below · cited by 3 · depth 13
• Hopf ideals admit Hopf quotients over a field HopfAlgebra.exists_hopfAlgebra_bialgHom_surjective_ker_eq_of_hopfIdeal 0 below · cited by 3 · depth 13
• Inertia-cyclotomic point submonoids are cut out by O[(ℤ/q)ᵃ] HopfAlgebra.exists_surjective_bialgHom_monoidAlgebra_of_inertiaCyclotomic_submonoid 18 below · cited by 4 · depth 13
• Tensor product of finite flat Hopf algebras is finite flat HopfAlgebra.finiteFlat_tensorProduct 0 below · cited by 1 · depth 13
• Killing a group scheme on all points versus on the universal point HopfAlgebra.forall_withConv_pow_eq_one_iff_toConv_id_pow_eq_one 0 below · cited by 5 · depth 13
• Cartier's theorem over an algebraically closed base field HopfAlgebra.isReduced_of_finiteType_of_isAlgClosed_of_charZero 5 below · cited by 1 · depth 13
• Vanishing ideal of a point submonoid is a Hopf ideal HopfAlgebra.map_mk_comul_eq_zero_and_counit_eq_zero_and_antipode_mem_of_mem_vanishingIdealOfPoints_ptSet 0 below · cited by 3 · depth 13
• K-points of a finite free Hopf algebra count its rank HopfAlgebra.natCard_algHom_eq_finrank_of_charZero 9 below · cited by 47 · depth 13
• No μₚ-type point when the Cartier dual is local HopfAlgebra.point_eq_one_of_forall_mem_inertiaSubgroupIn_eq_pow_of_isLocalRing_cartierDual 28 below · cited by 1 · depth 13
• Inertia-fixed points of a connected finite flat Hopf algebra over ℤ₍ₚ₎ HopfAlgebra.point_eq_one_of_forall_mem_inertiaSubgroupIn_of_isLocalRing 21 below · cited by 1 · depth 13
• Restriction of points to a Hopf kernel: monoid map with H(L)-fibres HopfAlgebra.toConv_comp_hopfKer_val_mul_and_eq_iff_existsUnique 4 below · cited by 11 · depth 13
• Points agreeing on the Hopf kernel: unique translating B-point HopfAlgebra.algHom_comp_hopfKer_val_eq_iff 0 below · cited by 4 · depth 14
• Finite Hopf algebras in characteristic zero are étale HopfAlgebra.algebra_etale_of_module_finite_of_charZero 7 below · cited by 15 · depth 14
• Λ-torsor grading of a Hopf algebra block HopfAlgebra.blockPieces_torsor_core 10 below · cited by 1 · depth 14
• L-points of a commutative Hopf algebra are convolution-invertible HopfAlgebra.exists_comp_antipode_convMul_eq_one 0 below · cited by 7 · depth 14
• Finite flat Hopf algebra over an abstract DVR with fraction field ℚ HopfAlgebra.exists_finiteFlat_dvr_of_padicInt_of_withConv_equiv_along 35 below · cited by 1 · depth 14
• Inertia eigenvector with tame character of p-adic digits 0,1 HopfAlgebra.exists_inertia_eigenvector_tameCharacter_pow_of_finite_flat 137 below · cited by 1 · depth 14
• Multiplicative-type point subgroup yields a group-algebra quotient HopfAlgebra.exists_surjective_bialgHom_monoidAlgebra_of_multiplicativeType_sub 17 below · cited by 1 · depth 14
• Cyclic torsor gradings: Q-torsion degrees give unit Q-th powers HopfAlgebra.exists_unit_pow_of_torsor_grading_nsmul 0 below · cited by 2 · depth 14
• Rank multiplicativity for Hopf kernels of surjective bialgebra maps HopfAlgebra.finrank_hopfKer_mul_finrank_of_surjective 17 below · cited by 4 · depth 14
• Localization at any K-point kernel of a Hopf algebra is a domain HopfAlgebra.isDomain_localization_atPrime_ker_algHom_of_finiteType_of_charZero 4 below · cited by 1 · depth 14
• Surjections onto finite free Hopf algebras are Hopf–Galois HopfAlgebra.isHopfGalois_of_surjective 2 below · cited by 13 · depth 14
• Local-local criterion from Ft=F² and Vt=V² HopfAlgebra.isLocalRing_and_isLocalRing_cartierDual_of_pow_eq_counit_of_frobenius_congr 0 below · cited by 1 · depth 14
• Finite-order points congruent to the counit are trivial HopfAlgebra.point_eq_one_of_pow_eq_one_of_sub_counit_mem_maximalIdeal 1 below · cited by 6 · depth 14
• Surjectivity of the canonical map for a surjective Hopf map HopfAlgebra.canMap_surjective_of_surjective 0 below · cited by 2 · depth 15
• Generic-fibre character algebra: annihilator description and Hopf stability HopfAlgebra.characterGenericFibre_eq_and_isComulStable_and_isAntipodeStable 2 below · cited by 5 · depth 15
• Unique lifting of bialgebra maps to R[M] over henselian local rings HopfAlgebra.existsUnique_bialgHom_addMonoidAlgebra_lift_residueField_of_henselianLocalRing 12 below · cited by 1 · depth 15
• Every K-point kernel is a translate of the augmentation ideal HopfAlgebra.exists_algEquiv_comap_ker_counitAlgHom_eq_ker_algHom 0 below · cited by 1 · depth 15
• Points of the character closure are L-valued characters of S HopfAlgebra.exists_characterClosure_points_equiv 3 below · cited by 2 · depth 15
• Finite flat Hopf model over a DVR with fraction field ℚ HopfAlgebra.exists_finiteFlat_dvr_of_ratLocalizedAt_of_irreducible 4 below · cited by 1 · depth 15
• Galois-simple finite flat factor for nonzero inertia-equivariant maps HopfAlgebra.exists_finiteFlat_galoisSimple_factor_of_nonzero_equivariant_map 13 below · cited by 1 · depth 15
• Tensor product model for a product of Galois modules HopfAlgebra.exists_finiteFlat_model_prod 0 below · cited by 2 · depth 15
• Equivariant quotients of points of finite flat ℤₚ-Hopf algebras HopfAlgebra.exists_finiteFlat_padicInt_quotient_of_equivariant_surjection 0 below · cited by 6 · depth 15
• Finite flat Hopf quotient by a Galois-stable point subgroup HopfAlgebra.exists_finiteFlat_quotient_of_forall_fixing_smul_mem 3 below · cited by 5 · depth 15
• Hopf-order descent from ℤₚ to ℤ₍ₚ₎ HopfAlgebra.exists_finiteFlat_ratLocalizedAt_of_padicInt_of_withConv_equiv 30 below · cited by 3 · depth 15
• Raynaud digit bound, Galois-simple case: inertia eigenvector for a tame character power HopfAlgebra.exists_inertia_eigenvector_tameCharacter_pow_of_finite_flat_of_galoisSimple 134 below · cited by 1 · depth 15
• Left integrals representing the counit on a finite free Hopf algebra HopfAlgebra.exists_leftIntegral_sum_apply_mul_eq_counit 0 below · cited by 2 · depth 15
• Transporting ℚ̄ₚ-points along a base-change bialgebra isomorphism HopfAlgebra.exists_withConv_equiv_padicInt_of_algEquiv_baseChange_padic 1 below · cited by 1 · depth 15
• Hopf kernel is finite free over a PID HopfAlgebra.finite_free_hopfKer_of_isPrincipalIdealRing 0 below · cited by 2 · depth 15
• Localization at the augmentation ideal is a domain HopfAlgebra.isDomain_localization_atPrime_ker_counitAlgHom_of_finiteType_of_charZero 2 below · cited by 1 · depth 15
• Hopf–Galois property, faithful flatness and finite type of Hopf kernels HopfAlgebra.isHopfGalois_and_faithfullyFlat_and_finiteType_hopfKer_of_surjective 35 below · cited by 2 · depth 15
• Point counts multiply along a surjection of Hopf algebras HopfAlgebra.natCard_algHom_eq_mul_of_surjective 5 below · cited by 1 · depth 15
• Bialgebra maps to a group algebra are determined modulo 𝔪 HopfAlgebra.bialgHom_addMonoidAlgebra_eq_of_mapAlgHom_residueField_comp_eq 2 below · cited by 1 · depth 16
• Index-two triviality criterion for points of the character closure HopfAlgebra.characterClosure_point_eq_trivial_of_restrict_of_congr_two 25 below · cited by 1 · depth 16
• Matching ℚ̄ₚ-point groups give isomorphic base-changed Hopf algebras HopfAlgebra.exists_algEquiv_baseChange_padic_comul_of_withConv_equiv 13 below · cited by 1 · depth 16
• Uniqueness of finite Hopf algebras over ℚₚ with given Galois module of points HopfAlgebra.exists_algEquiv_comul_of_withConv_equiv_algClosure_padic 12 below · cited by 1 · depth 16
• Existence of bialgebra lifts to R[M] over henselian local rings HopfAlgebra.exists_bialgHom_addMonoidAlgebra_lift_residueField_of_henselianLocalRing 8 below · cited by 1 · depth 16
• Odd-order flat Hopf ℤ-models: constant or extension by zero HopfAlgebra.exists_completeOrthogonalIdempotents_zmod_of_natCard_algHom_eq_of_ne_two 17 below · cited by 1 · depth 16
• Finite basis of I/I² at the augmentation ideal HopfAlgebra.exists_fin_lift_basis_ker_counitAlgHom_sq_of_finiteType 0 below · cited by 1 · depth 16
• Finite flat Hopf quotient by a finite set of L-points HopfAlgebra.exists_finiteFlat_bialgHom_surjective_comp_of_avg_descent 2 below · cited by 1 · depth 16
• Transport of a finite flat Hopf model along R ≅ ℤ₍ₚ₎ HopfAlgebra.exists_finiteFlat_of_ratLocalizedAt_of_algebraMap_range_eq 2 below · cited by 1 · depth 16
• Finite flat model for the induced module along an étale algebra HopfAlgebra.exists_finiteFlat_padicInt_model_pi_algHom_of_etale 14 below · cited by 1 · depth 16
• Finite flat ℤₚ-Hopf realisation of a unit-Kummer extension HopfAlgebra.exists_finiteFlat_padicInt_withConv_equiv_of_multiplicative_by_unramified_of_unitKummer 35 below · cited by 1 · depth 16
• Hopf-order descent from ℤₚ to ℤ₍ₚ₎ HopfAlgebra.exists_finiteFlat_ratLocalizedAt_of_algEquiv_baseChange_padic 16 below · cited by 1 · depth 16
• Finite Galois modules as points of finite commutative Hopf algebras HopfAlgebra.exists_hopfAlgebra_withConv_equiv_of_isOpen_stabilizer 0 below · cited by 1 · depth 16
• Inertia eigenvector from a reduction-kernel point with F≠ 0 HopfAlgebra.exists_inertia_eigenvector_tameCharacter_pow_of_finite_flat_of_galoisSimple_of_exists_reductionKernel_map_ne_zero 131 below · cited by 1 · depth 16
• Inertia-fixed eigenvector when F kills the reduction kernel HopfAlgebra.exists_inertia_eigenvector_tameCharacter_pow_of_finite_flat_of_galoisSimple_of_forall_reductionKernel_map_eq_zero 1 below · cited by 1 · depth 16
• Galois module of ℚ̄-points transfers to ℚ̄ₚ-points HopfAlgebra.exists_withConv_equiv_padic_of_withConv_equiv_algebraicClosure 1 below · cited by 1 · depth 16
• Faithful flatness of a Hopf algebra over a Hopf kernel HopfAlgebra.faithfullyFlat_hopfKer_of_surjective_of_isPrincipalIdealRing 29 below · cited by 1 · depth 16
• Hopf–Galois criterion via the kernel of π HopfAlgebra.isHopfGalois_iff_ker_le_span_of_surjective 0 below · cited by 6 · depth 16
• Hopf–Galois property of surjections from cocommutative Hopf algebras HopfAlgebra.isHopfGalois_of_isCocomm_of_finiteType_of_surjective 1 below · cited by 2 · depth 16
• Multiplicativity of the augmentation filtration in characteristic zero HopfAlgebra.mul_not_mem_ker_counitAlgHom_pow_succ_of_lift_basis_charZero 0 below · cited by 1 · depth 16
• Multiplicativity of point counts along a Hopf–Galois quotient HopfAlgebra.natCard_algHom_eq_mul_of_isHopfGalois 1 below · cited by 2 · depth 16
• Oort–Tate over ℤ: cyclotomic points give ℤ[ℤ/q] HopfAlgebra.nonempty_bialgEquiv_monoidAlgebra_of_natCard_algHom_eq_of_convPow_of_ne_two 38 below · cited by 1 · depth 16
• Non-finite μ_q-type Hopf algebras over ℤ: punctured models HopfAlgebra.prime_and_exists_bialgHom_monoidAlgebra_of_natCard_algHom_eq_of_convPow_of_not_finite_of_ne_two 40 below · cited by 1 · depth 16
• Post-composition by ι is bijective and convolution-multiplicative HopfAlgebra.bijective_withConv_algHomComp_of_finite_of_isAlgClosed 0 below · cited by 2 · depth 17
• Finite flat group schemes over ℤ are killed by their order HopfAlgebra.convPow_natCard_algHom_algebraicClosure_eq_one 7 below · cited by 2 · depth 17
• Finite flat Hopf algebra killed by an invertible integer is étale HopfAlgebra.etale_of_pow_eq_one_of_isUnit_of_finite 2 below · cited by 2 · depth 17
• Galois descent: étale Hopf algebras from their Ω-points HopfAlgebra.exists_algEquiv_comul_of_etale_of_withConv_equiv_algClosure 3 below · cited by 2 · depth 17
• Natural torsion point inclusion comes from a bialgebra quotient HopfAlgebra.exists_bialgHom_surjective_forall_comp_eq_of_natural_injective_of_range_eq_torsion 0 below · cited by 2 · depth 17
• Connected–étale sequence over ℤₚ in Hopf-algebraic form HopfAlgebra.exists_connected_etale_sequence_padicInt 30 below · cited by 3 · depth 17
• ℚ̄ₚ-points of a Weil restriction as induced Galois module HopfAlgebra.exists_distribMulAction_withConv_equiv_of_weilRestriction_points_padic 1 below · cited by 1 · depth 17
• Transport of finite flat cocommutative Hopf models along ring isomorphisms HopfAlgebra.exists_finiteFlat_cocomm_withConvEquiv_of_ringEquiv 1 below · cited by 1 · depth 17
• Hopf order over ℤ₍ₚ₎ from a p-adic identification HopfAlgebra.exists_finiteFlat_hopfOrder_ratLocalizedAt_of_algEquiv_baseChange_padic 13 below · cited by 1 · depth 17
• Galois-stable subquotients of points of finite flat ℤₚ-Hopf algebras HopfAlgebra.exists_finiteFlat_padicInt_withConv_equiv_subquotient 12 below · cited by 1 · depth 17
• A k-action on a finite flat p-group over ℤₚ HopfAlgebra.exists_forall_apply_comp_eq_smul_of_finrank_eq_prime_pow_of_ne_two 94 below · cited by 1 · depth 17
• Hopf points realise a multiplicative-by-unramified module étale-locally HopfAlgebra.exists_hopf_points_subquotient_of_unitKummer_over_etale_level 10 below · cited by 1 · depth 17
• Inertia-simple step carrying a nonzero additive functional HopfAlgebra.exists_inertiaStable_simple_step_of_map_ne_zero 12 below · cited by 1 · depth 17
• Raynaud digit bound for one inertia-simple step HopfAlgebra.exists_inertia_eigenvector_tameCharacter_pow_of_finite_flat_of_inertiaSimple_step 128 below · cited by 1 · depth 17
• Sign-twisted form of a finite flat ℤₚ-Hopf algebra HopfAlgebra.exists_signTwist_withConv_equiv_padicInt_of_odd_of_not_isSquare 13 below · cited by 1 · depth 17
• Kummer-type splitting of inertia for p-torsion Hopf algebras over ℤₚ HopfAlgebra.exists_units_forall_inertia_apply_eq_of_inertiaCyclotomic_submonoid_padicInt 48 below · cited by 1 · depth 17
• Weil restriction along a finite étale extension is finite flat HopfAlgebra.exists_weilRestriction_of_etale 9 below · cited by 2 · depth 17
• Transport of ℚ̄-points along a base-change isomorphism HopfAlgebra.exists_withConv_equiv_ratLocalizedAt_of_algEquiv_baseChange_rat 1 below · cited by 1 · depth 17
• Takeuchi's theorem: faithful flatness over a Hopf subalgebra HopfAlgebra.faithfullyFlat_subalgebra_of_comul_mem_span_of_antipode_mem 26 below · cited by 9 · depth 17
• Group-like elements reduce to 1; dual has no nontrivial idempotents HopfAlgebra.groupLike_characterClosure_mem_and_sub_one_mem_of_reduction 3 below · cited by 1 · depth 17
• Cocommutative Hopf algebras: the antipode is a coalgebra map HopfAlgebra.map_antipode_comul_of_isCocomm 1 below · cited by 8 · depth 17
• Point counts of G and G^∨ multiply to dim B HopfAlgebra.natCard_algHom_mul_natCard_algHom_cartierDual_eq_finrank_of_map_eq_conv_frobenius 6 below · cited by 2 · depth 17
• Hopf algebras of rank 2 over a base where 2 is irreducible HopfAlgebra.nonempty_algEquiv_pi_or_bialgEquiv_monoidAlgebra_of_finrank_eq_two_of_irreducible 1 below · cited by 2 · depth 17
• Connected rank-two Hopf algebra is R[ℤ/2] HopfAlgebra.nonempty_bialgEquiv_monoidAlgebra_of_finrank_eq_two_of_forall_isIdempotentElem 2 below · cited by 1 · depth 17
• Finite Hopf ℚ-algebra with cyclotomic q-point action is ℚ[ℤ/q] HopfAlgebra.nonempty_bialgEquiv_monoidAlgebra_of_natCard_algHom_eq_of_convPow_rat 7 below · cited by 1 · depth 17
• Finite flat Hopf algebra of order q with cyclotomic points is ℤ_{(q)}[ℤ/q] HopfAlgebra.nonempty_bialgEquiv_monoidAlgebra_of_natCard_algHom_ratLocalizedAt_eq_of_convPow_of_ne_two 26 below · cited by 2 · depth 17
• Galois-fixed ℚ̄-points of a flat Hopf ℤ-algebra HopfAlgebra.rational_separating_dense_algHom_algebraicClosure_of_forall_ringEquiv_apply_eq 10 below · cited by 2 · depth 17
• Congruent mathbf Z_{(ℓ)}-points of an odd-order Hopf ℤ-model agree HopfAlgebra.ringHom_ratLocalizedAt_eq_of_forall_sub_mem_span_of_natCard_algHom_eq_of_ne_two 14 below · cited by 1 · depth 17
• Convolution relation id^m = 1 base-changes along R → R' HopfAlgebra.toConv_id_pow_eq_one_baseChange 0 below · cited by 3 · depth 17
• The antipode is a coalgebra anti-morphism HopfAlgebra.comul_antipode 0 below · cited by 1 · depth 18
• Full faithfulness of the generic fibre over ℤₚ, p odd HopfAlgebra.existsUnique_bialgHom_forall_apply_comp_eq_of_finrank_eq_prime_pow_of_ne_two 93 below · cited by 6 · depth 18
• Raynaud digit bound for one inertia-simple step, functional form HopfAlgebra.exists_additive_eigenfunctional_tameCharacter_pow_of_finite_flat_of_inertiaSimple_step 124 below · cited by 1 · depth 18
• Tate–Oort normal form for rank two Hopf algebras HopfAlgebra.exists_basis_tateOort_two 0 below · cited by 2 · depth 18
• Finitely generated Hopf subalgebras exhaust a Hopf subalgebra HopfAlgebra.exists_fg_subalgebra_comul_mem_antipode_mem_of_finset_subset 2 below · cited by 1 · depth 18
• Hopf order over mathbb Z₍ₚ₎ from a matching basis HopfAlgebra.exists_finiteFlat_hopfOrder_ratLocalizedAt_of_basis_match 9 below · cited by 1 · depth 18
• Quotient Hopf algebra by a Hopf ideal over a commutative ring HopfAlgebra.exists_hopfAlgebra_bialgHom_surjective_ker_eq_of_hopfIdeal_of_commRing 0 below · cited by 4 · depth 18
• Factorisation of a bialgebra map through a finite flat Hopf algebra HopfAlgebra.exists_hopfAlgebra_surjective_injective_comp_eq 0 below · cited by 4 · depth 18
• Weil restriction of a cocommutative Hopf algebra along a finite free extension HopfAlgebra.exists_hopfAlgebra_weilRestriction_points_equiv 3 below · cited by 1 · depth 18
• Inertia eigenvector from a tame eigenfunctional on a simple step HopfAlgebra.exists_inertia_eigenvector_of_additive_eigenfunctional_of_inertiaSimple_step 3 below · cited by 1 · depth 18
• Kummer carrier Hopf algebra of a Kummer cocycle datum HopfAlgebra.exists_kummerCarrier_withConv_equiv_of_kummerCocycle 0 below · cited by 1 · depth 18
• Galois-stable chains of L-points and flat Hopf quotient flags HopfAlgebra.exists_quotientFlag_of_galoisStableChain_of_fixedPoints 0 below · cited by 6 · depth 18
• Hopf kernel of a surjection: retraction, projectivity and rank HopfAlgebra.exists_retraction_hopfKer_and_rankAtStalk_mul_finrank_of_surjective 4 below · cited by 26 · depth 18
• Quadratic twist of a finite flat cocommutative ℤₚ-Hopf algebra HopfAlgebra.exists_signTwist_withConv_mulEquiv_padicInt_of_odd_of_not_isSquare 12 below · cited by 1 · depth 18
• Unramified level for a unit-Kummer presentation of M HopfAlgebra.exists_unramified_unitKummer_surjection_of_multiplicative_by_unramified_of_unitKummer 5 below · cited by 1 · depth 18
• Takeuchi faithful flatness: reduced case implies the general case HopfAlgebra.faithfullyFlat_subalgebra_of_forall_isReduced_of_perfectField 6 below · cited by 1 · depth 18
• Faithful flatness over a reduced finitely generated Hopf subalgebra HopfAlgebra.faithfullyFlat_subalgebra_of_isReduced_of_fg_of_isAlgClosed 7 below · cited by 1 · depth 18
• Finite flat Hopf algebra killed by m on geometric points HopfAlgebra.forall_withConv_pow_eq_one_of_forall_algHom_pow_eq_one_of_isAlgClosed 10 below · cited by 2 · depth 18
• Idempotent augmentation ideal forces formal unramifiedness HopfAlgebra.formallyUnramified_of_ker_counit_eq_sq 0 below · cited by 3 · depth 18
• Finite flat Hopf algebra over ℤₚ with pᵃ points is free of rank pᵃ HopfAlgebra.free_and_finrank_eq_prime_pow_of_withConv_equiv_of_natCard_eq 10 below · cited by 1 · depth 18
• Inertia acts cyclotomically on inertia displacements (p odd) HopfAlgebra.inertia_displacement_eq_nsmul_of_inertiaTrivialOrCyclotomicChain_padicInt 51 below · cited by 1 · depth 18
• Locality of the Cartier dual passes to bialgebra quotients HopfAlgebra.isLocalRing_cartierDual_of_surjective 0 below · cited by 12 · depth 18
• Augmentation ideal is idempotent when n kills all points HopfAlgebra.ker_counit_eq_sq_of_pow_eq_one_of_isUnit 0 below · cited by 2 · depth 18
• Cyclotomic filtration forces inertia to act by ω (p odd) HopfAlgebra.act_eq_nsmul_of_inertiaCyclotomicChain_padicInt 50 below · cited by 1 · depth 19
• Reduction mod p is injective on points: unipotent case HopfAlgebra.algHom_eq_of_forall_sub_mem_span_of_isLocalRing_cartierDual 1 below · cited by 9 · depth 19
• The antipode of a commutative Hopf algebra is an involution HopfAlgebra.antipode_antipode 0 below · cited by 11 · depth 19
• Integrality of structure constants from a basis-matched p-adic model HopfAlgebra.basis_structureConstants_mem_ratLocalizedAt_range_of_basis_match_padic 5 below · cited by 1 · depth 19
• Translations by points: bijectivity, stability of subalgebras, transitivity HopfAlgebra.bijective_translate_and_map_mem_and_exists_comp_translate_eq 0 below · cited by 2 · depth 19
• Deligne's theorem: a point is killed by the rank HopfAlgebra.convPow_finrank_eq_one_of_isCocomm 0 below · cited by 6 · depth 19
• ℚ̄-points separate a finite flat Hopf algebra HopfAlgebra.eq_of_forall_algHom_algebraicClosure_apply_eq_of_flat_ratLocalizedAt 8 below · cited by 6 · depth 19
• Unique extension of generic-fibre Hopf morphisms over a uniformising p HopfAlgebra.existsUnique_bialgHom_baseChange_eq_of_pow_eq_one 86 below · cited by 3 · depth 19
• Full faithfulness of ̄ K-points of finite Hopf algebras HopfAlgebra.existsUnique_bialgHom_forall_apply_comp_eq_of_charZero 11 below · cited by 4 · depth 19
• Raynaud prolongation over ℤ₍ₚ₎: points form, p ≠ 2 HopfAlgebra.existsUnique_bialgHom_ratLocalizedAt_forall_apply_comp_eq_and_bijective_of_addEquiv_of_ne_two 94 below · cited by 5 · depth 19
• Identity-reducing points form a Galois-stable subgroup containing inertia displacements HopfAlgebra.exists_addSubgroup_forall_nnnorm_sub_counit_lt_one_padicInt 1 below · cited by 2 · depth 19
• Raynaud normal-form model of an inertia-simple step HopfAlgebra.exists_fVectStructure_normalForm_model_of_finite_flat_of_inertiaSimple_step 122 below · cited by 1 · depth 19
• Finite flat quotient Hopf algebra with prescribed Galois-stable points HopfAlgebra.exists_finiteFlat_padicInt_surjective_points_eq_of_galoisStable_addSubgroup 1 below · cited by 1 · depth 19
• Schematic closure of a Galois-stable monoid of ℚ̄-points HopfAlgebra.exists_finiteFlat_pointClosure_of_isGaloisInvariant_rat_algebraicClosure 12 below · cited by 3 · depth 19
• Naturally group-valued functor of points yields a Hopf algebra HopfAlgebra.exists_hopfAlgebra_algEquiv_of_natural_mul 0 below · cited by 1 · depth 19
• Hopf quotient by a Hopf subalgebra's augmentation ideal HopfAlgebra.exists_hopfAlgebra_surjective_ker_eq_span_of_comul_mem_span_of_antipode_mem 1 below · cited by 1 · depth 19
• Hopf order from a basis with R-integral structure constants HopfAlgebra.exists_hopfOrder_of_basis_structureConstants_mem_range 1 below · cited by 1 · depth 19
• Non-zero primitive element in a finite unipotent bialgebra HopfAlgebra.exists_ne_zero_comul_eq_tmul_one_add_one_tmul_of_isLocalRing_cartierDual 0 below · cited by 4 · depth 19
• Quadratic twist of a finite flat ℤₚ-Hopf algebra by a unit HopfAlgebra.exists_signTwist_linearEquiv_padicInt_of_odd 7 below · cited by 1 · depth 19
• Sign-twisted point bijection for a d₀-twisted p-adic Hopf algebra HopfAlgebra.exists_signTwist_withConv_mulEquiv_of_linearEquiv_padicInt 6 below · cited by 1 · depth 19
• Frobenius image of a finitely generated Hopf subalgebra is reduced HopfAlgebra.exists_subalgebra_pow_char_pow_isReduced 0 below · cited by 1 · depth 19
• Inertia-cyclotomic point submonoids cut out by a bialgebra surjection HopfAlgebra.exists_surjective_bialgHom_monoidAlgebra_of_inertiaCyclotomic_submonoid_of_isAlgClosed 17 below · cited by 3 · depth 19
• Finite Hopf algebra with twisted μₙ-points HopfAlgebra.exists_withConv_algHom_equiv_rootsOfUnity_quadraticTwist 19 below · cited by 1 · depth 19
• Faithful flatness of K⊗_{K'}H→ H⊗_{K'}H HopfAlgebra.faithfullyFlat_map_toAlgHom_tensor_of_free_map_of_ker_eq_span 0 below · cited by 1 · depth 19
• Flat Hopf algebra extensions over ̄ k are faithfully flat HopfAlgebra.faithfullyFlat_of_flat_of_injective_of_isAlgClosed 3 below · cited by 1 · depth 19
• Kreimer–Takeuchi: A finite projective over the Hopf kernel HopfAlgebra.finite_projective_hopfKer_of_surjective 2 below · cited by 7 · depth 19
• dim_k A = p^{dim_k P(A)} for Hopf algebras with trivial Verschiebung HopfAlgebra.finrank_eq_pow_finrank_primitives_of_forall_convPow_prime_eq_zero 1 below · cited by 3 · depth 19
• Freeness over a Hopf subalgebra with nilpotent augmentation ideal HopfAlgebra.free_subalgebra_of_isNilpotent_ker_counit 1 below · cited by 1 · depth 19
• Hopf kernel of a surjection stays local and local-dual HopfAlgebra.isLocalRing_hopfKer_and_isLocalRing_cartierDual_hopfKer_of_surjective 5 below · cited by 1 · depth 19
• Identity-reducing points lie in the inertia-displacement subgroup HopfAlgebra.mem_of_forall_nnnorm_sub_counit_lt_one_of_forall_inertia_displacement_mem_padicInt 43 below · cited by 2 · depth 19
• Non-finite order-two Hopf algebras over ℤ HopfAlgebra.prime_and_exists_isLocalizationAway_of_not_module_finite_of_natCard_algHom_eq_two 13 below · cited by 1 · depth 19
• Pairs of ℚ̄-points separate H⊗ H HopfAlgebra.tensorProduct_eq_of_forall_lift_apply_eq_of_flat_ratLocalizedAt 9 below · cited by 1 · depth 19
• Restriction of length-n Witt homomorphisms is surjective HopfAlgebra.wittHomMap_surjective_of_surjective_of_forall_convPow_eq_zero 46 below · cited by 8 · depth 19
• Inertia acts trivially on a finite flat ℤₚ-group with unramified chain (p odd) HopfAlgebra.act_eq_self_of_inertiaTrivialChain_padicInt 46 below · cited by 1 · depth 20
• Comultiplication-compatible algebra isomorphisms intertwine antipodes HopfAlgebra.antipode_comp_algEquiv_of_comul_compat 1 below · cited by 1 · depth 20
• Structure constants lie in mathbb Z₍ₚ₎ for basis-matched mathbb Zₚ-models HopfAlgebra.basis_structureConstants_mem_ratLocalizedAt_range_of_bialgHom_basis_match 2 below · cited by 1 · depth 20
• Rank-one torsor grading on a Hopf algebra block HopfAlgebra.blockPieces_torsor_core_of_isAlgClosed 10 below · cited by 1 · depth 20
• Inertia-fixed identity-reducing ℚ̄ₚ-points are trivial HopfAlgebra.eq_counit_of_forall_nnnorm_sub_counit_lt_one_of_forall_mem_inertiaSubgroupIn_apply_eq_padicInt 26 below · cited by 1 · depth 20
• Bialgebra maps into a flat algebra are determined generically HopfAlgebra.eq_of_baseChange_eq 0 below · cited by 1 · depth 20
• Raynaud full faithfulness in morphism form, p≠ 2 HopfAlgebra.existsUnique_bialgHom_forall_apply_comp_eq_of_finrank_eq_prime_pow_of_irreducible 93 below · cited by 3 · depth 20
• Full ℓ-power torsion points force a constant group scheme HopfAlgebra.exists_algEquiv_pi_of_injective_points_of_finrank_eq 1 below · cited by 1 · depth 20
• Torsor isomorphism H⊗_K H≅ H⊗_k(H/K⁺H) HopfAlgebra.exists_algEquiv_subalgebraTensor_tensorQuotient_of_comul_mem_span 0 below · cited by 2 · depth 20
• Finite flat models of a short exact Galois sequence, p odd HopfAlgebra.exists_bialgHom_surjective_range_eq_hopfKer_of_exact_of_ne_two 97 below · cited by 1 · depth 20
• Coefficient action of k on a finite flat ℤₚ-model HopfAlgebra.exists_coeffAction_forall_apply_comp_eq_smul_of_ne_two 94 below · cited by 1 · depth 20
• Descent of an F-vector space structure to a finite flat model HopfAlgebra.exists_fVectStructure_baseChange_eq_of_pow_eq_one 87 below · cited by 1 · depth 20
• Equivariant F-action on points gives an F-vector space structure HopfAlgebra.exists_fVectStructure_forall_comp_eq_of_equivariant_of_bijective_evalPoints 4 below · cited by 1 · depth 20
• Transport of an F-vector space structure along a bialgebra isomorphism HopfAlgebra.exists_fVectStructure_isFCompatible_of_bialgEquiv 0 below · cited by 1 · depth 20
• A finite field acting on an inertia-simple step of points HopfAlgebra.exists_field_lineAction_of_finite_flat_of_inertiaSimple_step 18 below · cited by 1 · depth 20
• Finite cocommutative Hopf algebra for norm-one torus n-torsion HopfAlgebra.exists_finite_cocomm_generated_normOneTorusNTorsion 17 below · cited by 1 · depth 20
• Functions primitive against pⁿ-th convolution powers descend HopfAlgebra.exists_mem_primitives_forall_apply_pow_eq_convPow_apply 0 below · cited by 1 · depth 20
• Lifting primitives along surjections of Hopf algebras killed by V HopfAlgebra.exists_mem_primitives_map_eq_of_surjective_of_forall_convPow_prime_eq_zero 30 below · cited by 1 · depth 20
• Sign-twist point bijection for a quadratic-twist Hopf algebra HopfAlgebra.exists_signTwist_withConv_equiv_formula_of_linearEquiv_padicInt 1 below · cited by 1 · depth 20
• Points of a norm-one torus Hopf algebra as μₙ HopfAlgebra.exists_withConv_equiv_rootsOfUnity_of_comul_gens_quadraticTwist 0 below · cited by 1 · depth 20
• Cartier's dimension formula for height-one bialgebras HopfAlgebra.finrank_eq_pow_finrank_cotangent_of_forall_pow_prime_eq_zero 0 below · cited by 4 · depth 20
• Primitives of the Cartier dual compute the cotangent rank HopfAlgebra.finrank_primitives_cartierDual_eq_finrank_cotangentSpace 0 below · cited by 2 · depth 20
• Order of the Frobenius kernel over 𝔽ₚ HopfAlgebra.finrank_quotient_span_pow_prime_ker_counit_eq_pow_finrank_cotangent 34 below · cited by 2 · depth 20
• Image of a Hopf kernel under a surjective bialgebra map HopfAlgebra.map_hopfKer_eq_hopfKer_of_surjective_of_ker_eq_map_ker 31 below · cited by 4 · depth 20
• Antipode axiom for the sign-twisted ℤₚ-Hopf structure HopfAlgebra.signTwist_antipode_mul_comul_padicInt 1 below · cited by 1 · depth 20
• Coassociativity of the sign-twisted comultiplication over ℤₚ HopfAlgebra.signTwist_comul_coassoc_padicInt 4 below · cited by 1 · depth 20
• Bialgebra compatibility of the sign-twisted ℤₚ-Hopf structure HopfAlgebra.signTwist_comul_mul_padicInt 3 below · cited by 1 · depth 20
• Sign-twisted Galois equivariance of the twist bijection HopfAlgebra.signTwist_galois_of_formula_of_linearEquiv_padicInt 1 below · cited by 1 · depth 20
• Injective bialgebra maps of p-power-order Hopf algebras, surjective generically HopfAlgebra.surjective_of_injective_of_surjective_baseChange_of_pow_eq_one 82 below · cited by 2 · depth 20
• Sign twist on points is convolution-multiplicative HopfAlgebra.withConv_mul_signTwist_of_formula_of_linearEquiv_padicInt 3 below · cited by 1 · depth 20
• Surjectivity of Hom(-,Wₙ) at a saturating level HopfAlgebra.wittHomMap_surjective_of_surjective_of_wittHomShift_surjective 55 below · cited by 1 · depth 20
• Points separate algebra endomorphisms of a split étale algebra HopfAlgebra.algHom_eq_of_forall_comp_eq_of_bijective_evalPoints 0 below · cited by 1 · depth 21
• Fontaine's fifth step: isomorphism detected on the special fibre HopfAlgebra.bijective_and_exists_bialgHom_eq_of_baseChange_eq_of_isLocalRing_cartierDual 2 below · cited by 1 · depth 21
• Generic-fibre bijectivity descends for p-power-torsion Hopf algebras HopfAlgebra.bijective_of_bijective_baseChange_of_pow_eq_one 81 below · cited by 1 · depth 21
• Convolution pⁿ-th power kills coordinates of Witt homomorphisms HopfAlgebra.convPow_apply_eq_zero_of_mem_adjoin_coeff_wittHom 1 below · cited by 1 · depth 21
• Infinitesimal Hopf algebras over a perfect field are truncated polynomial algebras HopfAlgebra.exists_algEquiv_mvPolynomial_quotient_X_pow_of_isNilpotent 31 below · cited by 2 · depth 21
• Equivariant endomorphism of points descends to a bialgebra endomorphism HopfAlgebra.exists_bialgHom_forall_comp_eq_of_equivariant_of_bijective_evalPoints 2 below · cited by 1 · depth 21
• Explicit cocommutative Hopf algebra of the norm-one torus HopfAlgebra.exists_cocomm_normOneTorus_generators_and_points 0 below · cited by 1 · depth 21
• Finite cocommutative n-torsion quotient of a norm-one torus HopfAlgebra.exists_finite_nTorsion_quotient_of_normOneTorus_generators 15 below · cited by 1 · depth 21
• Connected–étale splitting in Hopf form over p-adically complete 𝒪 HopfAlgebra.exists_formallyEtale_bialgHom_faithfullyFlat_ker_eq_map_ker_counit_zmodp 23 below · cited by 1 · depth 21
• Hopf quotient of B by the ideal generated by φ(kerε_A) HopfAlgebra.exists_hopfAlgebra_bialgHom_surjective_ker_eq_map_ker_counit 1 below · cited by 6 · depth 21
• Tangent–cotangent duality with operators for finite Hopf algebras HopfAlgebra.finrank_primitives_quot_iSup_map_eq_finrank_iInf_ker_mapCotangent_cartierDual 0 below · cited by 1 · depth 21
• Injectivity of cotangent maps for height-one Hopf algebras HopfAlgebra.mem_ker_counit_sq_of_map_mem_sq_of_injective_of_forall_pow_prime_eq_zero 28 below · cited by 1 · depth 21
• No cyclotomic p-torsion point with unipotent special fibre HopfAlgebra.point_eq_one_of_forall_mem_inertiaSubgroupIn_eq_pow_of_isLocalRing_cartierDual_padicInt 45 below · cited by 1 · depth 21
• Linear term in coassociativity of the sign-twisted comultiplication HopfAlgebra.signTwist_coassoc_linearTerm_padicInt 3 below · cited by 1 · depth 21
• Witt coordinates on a closed subgroup come from the ambient group HopfAlgebra.wittHom_coeff_mem_map_adjoin_of_surjective_of_wittHomShift_surjective 53 below · cited by 1 · depth 21
• Counit idempotent cuts out a Hopf quotient over a local ring HopfAlgebra.exists_bialgHom_surjective_ker_eq_span_one_sub_of_counit_eq_one_of_isLocalRing_quotient 1 below · cited by 2 · depth 22
• n-torsion quotient of the norm-one torus, generated form HopfAlgebra.exists_cocomm_adjoin_nTorsion_quotient_of_normOneTorus_generators 6 below · cited by 1 · depth 22
• Connected components of a finite flat group scheme as G⁰-torsors HopfAlgebra.exists_comul_quotient_bijective_of_completeOrthogonalIdempotents_of_counit_apply_eq_one 4 below · cited by 1 · depth 22
• Splitting symmetric normalised 2-cocycles on a finite Hopf algebra HopfAlgebra.exists_forall_apply_mul_eq_of_symm_cocycle_of_forall_apply_pow_pred_eq_pow 29 below · cited by 1 · depth 22
• Étale part of a finite flat commutative group scheme over ℤₚ HopfAlgebra.exists_formallyEtale_bialgHom_injective_bijective_baseChange_zmodp 12 below · cited by 1 · depth 22
• Factorisation of a bialgebra map through a finite flat Hopf quotient HopfAlgebra.exists_hopfAlgebra_surjective_injective_comp_eq_and_comul_mem_and_antipode_mem 0 below · cited by 7 · depth 22
• Witt-orthogonal and unipotent parts of a finite commutative Hopf algebra HopfAlgebra.exists_wittOrthogonal_unipotent_splitting_of_perfectField 1 below · cited by 1 · depth 22
• Finiteness of a two-generated Hopf algebra with torsion norm-one points HopfAlgebra.finite_of_normOneTorus_nTorsion_generators_and_points 7 below · cited by 1 · depth 22
• Dimension multiplicativity for Hopf subalgebras of nil Hopf algebras HopfAlgebra.finrank_eq_finrank_subalgebra_mul_finrank_quotient_of_isNilpotent 27 below · cited by 1 · depth 22
• Frobenius kernel has order p^{dim_k ω} HopfAlgebra.finrank_quotient_span_pow_prime_eq_pow_finrank_cotangent 1 below · cited by 7 · depth 22
• Hopf kernel of the quotient by a Hopf subalgebra's augmentation ideal HopfAlgebra.hopfKer_eq_of_surjective_of_ker_eq_span 27 below · cited by 2 · depth 22
• j(kerε_H)L=(1-j(f)) for a unit-component idempotent HopfAlgebra.map_ker_counit_eq_span_one_sub_of_isIdempotentElem_of_isLocalRing_zmodp 4 below · cited by 1 · depth 22
• Lagrange for K-points of a Hopf algebra quotient HopfAlgebra.natCard_algHom_dvd_natCard_algHom_of_surjective 1 below · cited by 2 · depth 22
• Surjectivity half of the short five lemma for Hopf algebras HopfAlgebra.surjective_of_bijective_of_bijOn_hopfKer 4 below · cited by 1 · depth 22
• Surjectivity of a dominating finite flat model over an unramified DVR HopfAlgebra.surjective_of_injective_of_surjective_baseChange_of_pow_eq_one_of_simple 79 below · cited by 1 · depth 22
• Pairs of ℚ̄-points separate A ⊗_{F'} A HopfAlgebra.tensorProduct_eq_zero_of_forall_lift_points_eq_zero 1 below · cited by 1 · depth 22
• Points through a local quotient vanish in Galois-invariant p-quotients HopfAlgebra.apply_eq_zero_of_bialgHom_of_isLocalRing_of_finrank_eq_prime_pow_of_irreducible 94 below · cited by 1 · depth 23
• Bijectivity of R₂⊗φ from an F-vector dévissage HopfAlgebra.bijective_baseChange_of_hasFVectDevissage 43 below · cited by 1 · depth 23
• Faithfully flat descent of bijectivity for a bialgebra map HopfAlgebra.bijective_of_faithfullyFlat_baseChange_bijective 0 below · cited by 1 · depth 23
• n-torsion quotient of a norm-one torus Hopf algebra HopfAlgebra.exists_cocomm_adjoin_nTorsion_quotient_of_adjoin_normOneTorus 4 below · cited by 1 · depth 23
• Cocommutative generated norm-one torus Hopf algebra inside an ambient one HopfAlgebra.exists_cocomm_adjoin_normOneTorus_of_generators_and_points 0 below · cited by 1 · depth 23
• F-vector dévissage of the generic fibre after faithfully flat base change HopfAlgebra.exists_faithfullyFlat_hasFVectDevissage_baseChange_of_pow_eq_one 45 below · cited by 1 · depth 23
• Lifting reduced finite commutative Hopf mathbb Fₚ-algebras to 𝒪 HopfAlgebra.exists_formallyEtale_bialgEquiv_baseChange_zmodp 5 below · cited by 2 · depth 23
• Frobenius realises the reduced quotient of a finite mathbb Fₚ-Hopf algebra HopfAlgebra.exists_isReduced_bialgHom_injective_comp_eq_pow_zmodp 1 below · cited by 2 · depth 23
• Étale Hopf algebras with matching Galois modules of Ω-points HopfAlgebra.exists_algEquiv_comul_counit_withConv_comp_of_etale_of_withConv_equiv_algClosure 0 below · cited by 1 · depth 24
• Lifting a bialgebra map along a unipotent finite flat Hopf algebra HopfAlgebra.exists_bialgHom_eq_of_baseChange_eq_of_isLocalRing_cartierDual 2 below · cited by 1 · depth 24
• The n-torsion quotient of a norm-one torus Hopf algebra HopfAlgebra.exists_cocomm_adjoin_nTorsion_quotient_of_powerPair 2 below · cited by 1 · depth 24
• Connected component of a unipotent finite flat Hopf algebra over ℤₚ HopfAlgebra.exists_connectedComponent_of_isLocalRing_cartierDual_zmodp 8 below · cited by 1 · depth 24
• Faithfully flat base change making Galois abelian-by-p HopfAlgebra.exists_faithfullyFlat_isGalois_isPGroup_commutator_le_baseChange_of_pow_eq_one 25 below · cited by 1 · depth 24
• Common finite flat model of two generically isomorphic Hopf algebras HopfAlgebra.exists_finiteFlat_model_bialgHom_surjective_baseChange_of_algEquiv_baseChange 0 below · cited by 1 · depth 24
• The n-th power pair on a norm-one torus Hopf algebra HopfAlgebra.exists_normOneTorus_nthPowerPair_of_generators 0 below · cited by 1 · depth 24
• Raynaud dévissage for split étale p-torsion Hopf algebras HopfAlgebra.hasFVectDevissage_of_bijective_evalPoints_of_isPGroup_of_commutator_le_of_perfectField 18 below · cited by 1 · depth 24
• Surjectivity of Hopf algebra maps surjective on the generic fibre HopfAlgebra.surjective_of_surjective_baseChange_of_pow_eq_one 84 below · cited by 1 · depth 24
• Bijectivity of the evaluation map passes to a Hopf kernel HopfAlgebra.bijective_evalPoints_hopfKer_of_bijective_evalPoints 0 below · cited by 1 · depth 25
• Galois-stable subgroups of points cut out by Hopf quotients HopfAlgebra.exists_bialgHom_surjective_points_eq_of_submonoid_of_bijective_evalPoints_of_perfectField 10 below · cited by 1 · depth 25
• Galois-equivariant F-action on points descends to an F-vector space structure HopfAlgebra.exists_fVectStructure_of_pointAction_of_bijective_evalPoints 3 below · cited by 1 · depth 25
• Schematic closure of a closed subgroup of the generic fibre HopfAlgebra.exists_free_hopf_quotient_algHom_injective_points_iff_of_baseChange_surjective 0 below · cited by 1 · depth 25
• Quotient of a norm-one torus Hopf algebra by a power pair HopfAlgebra.exists_normOneTorus_hopfIdeal_quotient_of_powerPair 0 below · cited by 1 · depth 25
• Order of a finite Hopf algebra map: kernel times image HopfAlgebra.finrank_eq_finrank_quotient_map_ker_counit_mul_finrank_range 36 below · cited by 8 · depth 25
• Idempotent augmentation ideal implies formally unramified HopfAlgebra.formallyUnramified_of_isIdempotentElem_ker_counit 0 below · cited by 1 · depth 25
• ̄ K-points of the n-torsion of the norm-one torus HopfAlgebra.normOneTorus_quotient_nTorsion_points_of_powerPair 0 below · cited by 1 · depth 25
• Algebra maps from the Hopf kernel extend over Ω HopfAlgebra.exists_algHom_comp_hopfKer_val_eq_of_surjective_of_isAlgClosed 0 below · cited by 3 · depth 26
• Galois descent: equivariant point endomorphisms come from bialgebra maps HopfAlgebra.exists_bialgHom_forall_comp_eq_of_equivariant_of_forall_fixed_mem_range 1 below · cited by 1 · depth 26
• Maximal multiplicative-type quotient of a finite flat Hopf algebra HopfAlgebra.exists_bialgHom_surjective_etale_cartierDual_forall_existsUnique_comp_eq_of_henselianLocalRing 17 below · cited by 2 · depth 26
• Restriction of Ω-points to a Hopf kernel HopfAlgebra.exists_restriction_points_hopfKer_mul_and_eq_one_iff_and_surjective_of_isAlgClosed 7 below · cited by 1 · depth 26
• Idempotents in the ideal (F,V) have ordinary image HopfAlgebra.exists_split_idempotent_bijective_tensorProduct_isReduced_cartierDual_of_cartierDualMap_eq_frobenius_conv_verschiebung 7 below · cited by 2 · depth 26
• Evaluation isomorphism for a D-stable subset of split points HopfAlgebra.lift_liftPoint_bijective_of_forall_exists_comp_eq 0 below · cited by 2 · depth 26
• Pairs of points separate the tensor square of `pointQuot` HopfAlgebra.tensorProduct_pointQuot_eq_zero_of_forall_evalPair_eq_zero_of_bijective_evalQuot 0 below · cited by 1 · depth 26
• Trivial Cartier pairing with points factoring through an étale dual HopfAlgebra.apply_ofDual_eq_one_of_eq_comp_of_forall_sub_apply_one_mem_maximalIdeal_of_henselianLocalRing 1 below · cited by 2 · depth 27
• Functoriality of the connected–étale splitting over 𝔽ₚ HopfAlgebra.exists_bialgHom_comp_eq_of_bijective_tensorProduct_comul_zmodp 0 below · cited by 1 · depth 27
• Splitting an idempotent bialgebra endomorphism over a local ring HopfAlgebra.exists_bialgHom_surjective_comp_eq_id_comp_eq_of_comp_eq_self_of_isLocalRing 0 below · cited by 2 · depth 27
• Dualising an étale quotient of the Cartier dual HopfAlgebra.exists_bialgHom_surjective_etale_cartierDual_forall_existsUnique_comp_eq_of_bialgHom_injective_cartierDual 2 below · cited by 1 · depth 27
• Identity-component Hopf quotient over a henselian local base HopfAlgebra.exists_bialgHom_surjective_isLocalRing_tensorProduct_forall_point_comp_eq_of_henselianLocalRing 3 below · cited by 1 · depth 27
• Ordinary normal form descends to the residue field of P HopfAlgebra.exists_bijective_tensorProduct_isReduced_cartierDual_residueField_of_zmodp_valuationSubring_of_isCocomm 1 below · cited by 1 · depth 27
• Formal P-points factor through the multiplicative quotient HopfAlgebra.exists_eq_comp_of_forall_sub_counit_mem_maximalIdeal_of_bijective_tensorProduct_isReduced_valuationSubring 16 below · cited by 1 · depth 27
• Maximal étale quotient of a finite flat commutative Hopf algebra HopfAlgebra.exists_etale_bialgHom_injective_forall_existsUnique_comp_eq_of_henselianLocalRing 13 below · cited by 1 · depth 27
• Connected–étale splitting of a finite Hopf algebra over mathbf Fₚ HopfAlgebra.exists_isLocalRing_isReduced_bijective_tensorProduct_comul_zmodp 2 below · cited by 2 · depth 27
• Hopf kernels commute with flat base change HopfAlgebra.hopfKer_baseChange_toSubmodule_eq_range_baseChange 0 below · cited by 6 · depth 27
• Ordinarity forces the unit component to be of multiplicative type HopfAlgebra.isReduced_cartierDual_of_bijective_tensorProduct_isReduced_cartierDual_of_bijective_tensorProduct_comul_zmodp 1 below · cited by 1 · depth 27
• Connected Hopf quotients of ordinary Hopf algebras over 𝔽ₚ HopfAlgebra.isReduced_cartierDual_of_surjective_of_isLocalRing_of_bijective_tensorProduct_isReduced 0 below · cited by 1 · depth 27
• Kernel of a surjective Hopf quotient is generated by the augmentation ideal of the Hopf kernel HopfAlgebra.ker_eq_map_hopfKer_inf_ker_counit_of_surjective 36 below · cited by 1 · depth 27
• Naturality of the Verschiebung pinned on the Cartier dual HopfAlgebra.comp_eq_comp_of_forall_cartierDual_apply_eq_pow_apply_zmodp 0 below · cited by 2 · depth 28
• Endomorphisms descend uniquely to the connected quotient Hopf algebra HopfAlgebra.existsUnique_bialgHom_comp_eq_comp_of_surjective_of_isLocalRing_of_isReduced_of_ker_eq_map_zmodp 0 below · cited by 1 · depth 28
• Frobenius–Verschiebung factorisation descends to a split unit-root factor HopfAlgebra.exists_cartierDualMap_id_eq_frobenius_conv_verschiebung_of_comp_eq_idempotent_of_cartierDualMap_pow_eq 0 below · cited by 1 · depth 28
• Étale quotient of a finite commutative Hopf algebra over a field HopfAlgebra.exists_etale_bialgHom_injective_forall_existsUnique_comp_eq_of_field 3 below · cited by 1 · depth 28
• Lifting the étale quotient to a henselian local base HopfAlgebra.exists_etale_bialgHom_injective_forall_existsUnique_comp_eq_of_henselianLocalRing_of_residueField 8 below · cited by 1 · depth 28
• Order of a Hopf algebra splits along its Frobenius kernel HopfAlgebra.finrank_quotient_span_pow_mul_finrank_cartierDual_quotient_eq 6 below · cited by 2 · depth 28
• Local ring from reduced Cartier dual of p-power rank HopfAlgebra.isLocalRing_of_isReduced_cartierDual_of_finrank_eq_prime_pow 2 below · cited by 1 · depth 28
• Extensions of 𝔽ₚ-Hopf algebras with reduced Cartier dual HopfAlgebra.isReduced_cartierDual_of_injective_of_surjective_of_ker_eq_map_zmodp 5 below · cited by 1 · depth 28
• Reduced Cartier dual makes Verschiebung a bialgebra automorphism HopfAlgebra.exists_bialgEquiv_forall_cartierDual_map_eq_pow_of_isReduced_cartierDual_zmodp 2 below · cited by 2 · depth 29
• Finite étale Hopf algebras lift over a henselian local ring HopfAlgebra.exists_etale_nonempty_bialgEquiv_baseChange_residueField_of_henselianLocalRing 6 below · cited by 1 · depth 29
• Schematic closure of a Galois-stable subgroup of points HopfAlgebra.exists_finiteFlat_bialgHom_surjective_points_equiv_of_stable_subgroup 9 below · cited by 1 · depth 29
• Frobenius is nilpotent on a finite local 𝔽ₚ-Hopf algebra HopfAlgebra.exists_forall_pow_pow_eq_algebraMap_counit_of_isLocalRing_zmodp 0 below · cited by 1 · depth 29
• Faithful flatness over a reduced Hopf subalgebra HopfAlgebra.faithfullyFlat_of_isReduced_of_isAlgClosed 1 below · cited by 1 · depth 29
• Cartier dual of a base-changed group algebra is reduced HopfAlgebra.isReduced_cartierDual_baseChange_addMonoidAlgebra 0 below · cited by 2 · depth 29
• Reducedness of the Cartier dual descends along field extensions HopfAlgebra.isReduced_cartierDual_of_isReduced_cartierDual_baseChange 0 below · cited by 2 · depth 29
• Geometric points separate bialgebra maps in characteristic zero HopfAlgebra.bialgHom_eq_of_forall_algHom_comp_eq_of_charZero 12 below · cited by 1 · depth 30
• Factorisation of bialgebra maps killed by a Hopf quotient HopfAlgebra.exists_bialgHom_comp_eq_of_injective_baseChange_of_finrank_eq_of_comp_eq_counit 5 below · cited by 1 · depth 30
• Verschiebung, unit reduction, rank and local special fibre HopfAlgebra.exists_verschiebung_bialgEquiv_and_sub_counit_mem_and_finrank_of_baseChange_bialgEquiv_addMonoidAlgebra_and_isLocalRing 5 below · cited by 1 · depth 30
• Hopf–Galois descent for the Hopf kernel over a PID HopfAlgebra.isHopfGalois_and_faithfullyFlat_and_finiteType_hopfKer_of_surjective_of_moduleFinite_baseChange_of_charZero 59 below · cited by 1 · depth 30
• Descent of p^v-torsion kernels along a faithfully flat trivialisation HopfAlgebra.ker_eq_torsionIdeal_of_baseChange_addMonoidAlgebra_of_surjective 0 below · cited by 1 · depth 30
• Hopf kernels commute with base change to the residue field HopfAlgebra.baseChange_toSubmodule_hopfKer_eq_toSubmodule_hopfKer_map_residueField_of_surjective 5 below · cited by 1 · depth 31
• Faithful flatness over a Hopf kernel is local on the base HopfAlgebra.faithfullyFlat_hopfKer_of_forall_isLocalRing_faithfullyFlat_baseChange 2 below · cited by 1 · depth 31
• Group-like elements of a connected smooth Hopf algebra HopfAlgebra.free_and_finite_and_finrank_groupLike_le_of_locally_isStandardSmoothOfRelativeDimension 30 below · cited by 1 · depth 31
• Hopf–Galois descent along a quotient with split finite part HopfAlgebra.isHopfGalois_and_faithfullyFlat_and_finiteType_hopfKer_of_finitePartIdempotent 46 below · cited by 1 · depth 31
• Hopf–Galois property is local on the base along flat local covers HopfAlgebra.isHopfGalois_of_forall_isLocalRing_isHopfGalois_baseChange_of_flat 2 below · cited by 1 · depth 31
• Characters trivial and order prime to char k force φ=ε HopfAlgebra.withConv_algHom_eq_one_of_pow_eq_one_of_forall_isGroupLikeElem 0 below · cited by 1 · depth 31
• Hopf-kernel idempotent dominating the finite-part idempotent HopfAlgebra.exists_isIdempotentElem_mem_hopfKer_mul_eq_of_finitePartIdempotent 12 below · cited by 1 · depth 32
• Faithful flatness of H over its Hopf kernel, local case HopfAlgebra.faithfullyFlat_hopfKer_of_finitePartIdempotent 37 below · cited by 2 · depth 32
• Finite type of the Hopf kernel for a split quasi-finite pair HopfAlgebra.finiteType_hopfKer_of_finitePartIdempotent 0 below · cited by 1 · depth 32
• Hopf–Galois descent for a split quasi-finite pair over a local PID HopfAlgebra.isHopfGalois_of_finitePartIdempotent 41 below · cited by 1 · depth 32
• Lower bound g ≤ dim_K P(H) for H of dimension p^{2g} HopfAlgebra.le_finrank_primitives_of_finrank_eq_pow_of_nsmulAlgHom_eq 8 below · cited by 3 · depth 32
• Finite-part idempotent is group-like: Δ(e)(e⊗ 1)=e⊗ e HopfAlgebra.comul_finitePartIdempotent_mul 0 below · cited by 3 · depth 33
• Counit of a finite-part idempotent equals 1 HopfAlgebra.counit_finitePartIdempotent 0 below · cited by 3 · depth 33
• Primitives of H versus the dual cotangent space of H^∨ HopfAlgebra.exists_primitives_linearEquiv_dual_cotangent_cartierDual 2 below · cited by 2 · depth 33
• Faithful flatness of H over the invariants on the orbit corner HopfAlgebra.faithfullyFlat_quotient_span_one_sub_orbitIdempotent_baseChange_of_finitePartIdempotent 34 below · cited by 1 · depth 33
• Faithful flatness over the generic corner B/(f) HopfAlgebra.faithfullyFlat_quotient_span_orbitIdempotent_baseChange_of_finitePartIdempotent 5 below · cited by 1 · depth 33
• Frobenius image bounds the dimension of a finite Hopf algebra HopfAlgebra.finrank_le_finrank_span_pow_prime_mul_pow_finrank_cotangent 2 below · cited by 1 · depth 33
• Span of p-th powers bounded via Cartier dual quotient HopfAlgebra.finrank_span_pow_prime_le_finrank_cartierDual_quotient_of_nsmulAlgHom_eq 1 below · cited by 1 · depth 33
• Hopf–Galois descends from the generic fibre under flatness HopfAlgebra.isHopfGalois_of_isHopfGalois_baseChange_of_flat 2 below · cited by 1 · depth 33
• Kähler differentials of a Hopf algebra are extended from I/I² HopfAlgebra.nonempty_kaehlerDifferential_linearEquiv_tensorProduct_cotangent 0 below · cited by 2 · depth 33
• Primitives are coboundaries, and coinvariants descend, for a torsor HopfAlgebra.exists_coaction_eq_tmul_one_add_one_tmul_of_comul_eq_of_faithfullyFlat 2 below · cited by 2 · depth 34
• Finite-part quotient Hopf algebra H/(1-e) over a local ring HopfAlgebra.exists_hopfAlgebra_bialgHom_surjective_ker_eq_span_one_sub_of_finitePartIdempotent 4 below · cited by 1 · depth 34
• Finite Hopf algebras: kernels of presentations are locally N-generated HopfAlgebra.exists_ker_map_localization_eq_span_of_surjective_mvPolynomial_of_isMaximal 43 below · cited by 1 · depth 34
• Faithful flatness over the Hopf kernel, finite flat case HopfAlgebra.faithfullyFlat_hopfKer_of_surjective_of_isPrincipalIdealRing_of_moduleFinite 3 below · cited by 2 · depth 34
• Invariants descend onto the invariants of the finite part HopfAlgebra.map_hopfKer_eq_hopfKer_of_finitePartIdempotent 26 below · cited by 1 · depth 34
• Antipode fixes the finite-part idempotent HopfAlgebra.antipode_finitePartIdempotent 0 below · cited by 1 · depth 35
• Finite commutative Hopf algebras over an algebraically closed field HopfAlgebra.exists_algEquiv_pi_mvPolynomial_quotient_span_pow_of_isAlgClosed 34 below · cited by 1 · depth 35
• Restriction of the Hopf kernel to an idempotent sub-part HopfAlgebra.map_hopfKer_eq_hopfKer_of_comul_mul_tmul_eq 19 below · cited by 1 · depth 35
• Hopf kernels are detected on the generic fibre HopfAlgebra.mem_hopfKer_iff_one_tmul_mem_hopfKer_baseChange_fractionRing 0 below · cited by 1 · depth 35
• Inertia-invariant characters kill points reducing to the identity HopfAlgebra.eq_one_of_forall_valuation_sub_counit_lt_one_of_inertiaInvariant 20 below · cited by 1 · depth 36
• Local finite Hopf algebras over a perfect field are truncated polynomial algebras HopfAlgebra.exists_algEquiv_mvPolynomial_quotient_span_pow_of_isLocalRing_of_perfectField 32 below · cited by 1 · depth 36
• Finite Hopf algebra as a power of a local quotient HopfAlgebra.exists_hopfAlgebra_isLocalRing_algEquiv_pi_of_isAlgClosed 0 below · cited by 1 · depth 36
• Cocycles with values in a Hopf-module ideal are coboundaries HopfAlgebra.exists_eq_coaction_sub_tmul_one_of_cocycle 2 below · cited by 1 · depth 40
• Relative fundamental theorem of Hopf modules for ideals HopfAlgebra.le_span_coinvariant_and_exists_coinvariant_sub_mem 1 below · cited by 1 · depth 40
• Fundamental theorem of Hopf modules, commutative case HopfAlgebra.bijective_lift_coinvariants_and_bijective_mkQ_of_isHopfModule 0 below · cited by 2 · depth 41

HopfAlgebra.FVect 4

• Raynaud normal form for rank-q F-vector space schemes HopfAlgebra.FVect.exists_generators_normalForm_of_finrank_eq_card 11 below · cited by 2 · depth 20
• Uniqueness of Hopf orders of rank p^r F-vector space Hopf algebras HopfAlgebra.FVect.hopfOrder_eq_of_le 32 below · cited by 1 · depth 25
• Rigidity of F^×-stable Hopf orders when p is a uniformiser HopfAlgebra.FVect.hopfOrder_eq_of_le_of_forall_act_mem 16 below · cited by 1 · depth 26
• Raynaud profile of an F-equivariant map of Hopf orders HopfAlgebra.FVect.exists_profile_of_isFCompatible 0 below · cited by 1 · depth 27

HopfAlgebra.FVectStructure 1

• Restricting an F-vector space structure to a Hopf order HopfAlgebra.FVectStructure.exists_restrict_hopfOrder 0 below · cited by 1 · depth 27

HopfAlgebra.Raynaud 2

• Nested Hopf orders of a dévissable Hopf algebra coincide HopfAlgebra.Raynaud.hopfOrder_eq_of_le_of_hasFVectDevissage 40 below · cited by 1 · depth 24
• Nonnegative Raynaud profile with n'≤ e<p-1 vanishes HopfAlgebra.Raynaud.valProfile_eq_zero_of_ramification_lt 0 below · cited by 1 · depth 27