← all areas

Namespace FrobeniusEndo 22 theorems

• Frobenius satisfies π²-aπ+q=0 on all k-points FrobeniusEndo.frobCharEqOnPoints_of_frobenius 23 below · cited by 2 · depth 7
• Pointwise characteristic equation of Frobenius from the kernel-count line FrobeniusEndo.frobCharEqOnPoints_of_line 10 below · cited by 2 · depth 8
• Kernel-degree line #ker([m]-π)=m²-am+q FrobeniusEndo.kerDeg_frobEnd_line_one 11 below · cited by 4 · depth 8
• Finiteness of ker([m]-π) on W(k) FrobeniusEndo.kerDeg_frobEnd_line_one_ne_zero 10 below · cited by 4 · depth 8
• Characteristic equation of σ on p-torsion at an isotropic prime FrobeniusEndo.charEq_on_torsionBy_of_line_of_isotropic 3 below · cited by 1 · depth 9
• Roots of X²-aX+q modulo arbitrarily large primes FrobeniusEndo.exists_prime_gt_and_quadratic_root 0 below · cited by 1 · depth 9
• Frobenius characteristic relation on all points from large torsion FrobeniusEndo.frobCharEqOnPoints_of_charEq_on_torsion_of_trace_ne_zero 0 below · cited by 1 · depth 9
• Frobenius characteristic equation on points, trace-zero case FrobeniusEndo.frobCharEqOnPoints_of_charEq_on_torsion_of_trace_zero 3 below · cited by 1 · depth 9
• Degree formula for the Frobenius pencil [m]-π FrobeniusEndo.kerDeg_frobEnd_line_one_pos_and_eq 9 below · cited by 2 · depth 9
• Fixed points of the q-power Frobenius are the F-rational points FrobeniusEndo.kerDeg_frobEnd_one_one 0 below · cited by 3 · depth 9
• Pointwise-equal automorphisms give the same torsion operator FrobeniusEndo.galoisRepModuleEnd_eq_of_forall_eq 0 below · cited by 1 · depth 10
• Invariance of p-torsion trace and determinant under field extension FrobeniusEndo.galoisTrace_det_eq_of_isScalarTower 0 below · cited by 1 · depth 10
• Trace and determinant of Frobenius on p-torsion FrobeniusEndo.galoisTrace_det_frob_of_isAlgClosed 27 below · cited by 1 · depth 10
• Kernel count #ker([m]-π)=m²-am+q for the Frobenius pencil FrobeniusEndo.kerDeg_frobEnd_line_one_pos_and_eq_of_torsion 6 below · cited by 1 · depth 10
• Trace and determinant of σ on p-torsion, isotropic case FrobeniusEndo.trace_det_frob_of_line_of_isotropic 2 below · cited by 2 · depth 10
• Vanishing of det(̄ m-̄ nσ) on p-torsion versus p∣#ker FrobeniusEndo.det_frobPencilEnd_eq_zero_iff_dvd_kerDeg 1 below · cited by 1 · depth 11
• Singular pencil on p-torsion forces p ∣ #ker([m]-[n]σ) FrobeniusEndo.dvd_kerDeg_of_det_frobPencilEnd_eq_zero 0 below · cited by 2 · depth 11
• x([m]P-π P) as a rational function of x(P) FrobeniusEndo.exists_x_linePencil_frobEnd_mul_collision_sq 3 below · cited by 2 · depth 11
• Frobenius trace on W[p] as q+1-#W(mathbb F_q) FrobeniusEndo.galoisTrace_frob_eq_of_line_of_charEqOnPoints 6 below · cited by 1 · depth 11
• Trace and determinant of σ on W(K)[p] FrobeniusEndo.trace_det_frob_of_line_of_charEqOnPoints 4 below · cited by 1 · depth 12
• Trace and determinant of σ on W(K)[p], anisotropic case FrobeniusEndo.trace_det_frob_of_charEq_of_anisotropic 0 below · cited by 1 · depth 13
• Kernel count of [m]-π over a finite field FrobeniusEndo.kerDeg_frobEnd_line_one_pos_and_eq_finiteField 7 below · cited by 1 · depth 22