← all areas

Namespace FreyPackage 59 theorems

Landmarks here: Fermat's Last Theorem for prime exponents p ≥ 5 · No Frey package exists · Frey package from a counterexample of exponent p ≥ 5 · Irreducibility of the mod-p torsion module of the Frey curve · Modularity of the Frey curve · Level lowering to Γ₀(2) for the Frey curve · Irreducibility of E_P[p] when a ≡ 3 (mod 8) · No Galois-stable cofixed line at p=11 · Mazur at p≥ 17: no cofixed line · No Galois-stable cofixed line for p∈{5,7,13} · Reducible Frey representation yields a Galois-stable cofixed line · Level lowering for the Frey curve down to Γ₀(2) · Conductor-level modularity of the Frey curve's mod-p representation · Frey p-torsion is unramified outside {2,p} · Mazur–Ribet level lowering at p for conductor levels · Ribet level lowering at an odd prime q ≠ p · Eichler–Shimura residual attachment at every level

— 57 · ModMCarrier 2

directly in FreyPackage 57

• landmark Fermat's Last Theorem for prime exponents p ≥ 5 FreyPackage.fermatLastTheoremFor_of_five_le 29,486 below · cited by 1 · depth 2
• landmark No Frey package exists FreyPackage.no_frey_package 29,484 below · cited by 1 · depth 3
• landmark Frey package from a counterexample of exponent p ≥ 5 FreyPackage.of_counterexample 0 below · cited by 1 · depth 3
• landmark Irreducibility of the mod-p torsion module of the Frey curve FreyPackage.Mazur_Frey 5,435 below · cited by 1 · depth 4
• landmark Modularity of the Frey curve FreyPackage.frey_isModular 27,797 below · cited by 1 · depth 4
• landmark Level lowering to Γ₀(2) for the Frey curve FreyPackage.level_lowering_to_two 27,851 below · cited by 1 · depth 4
• landmark Irreducibility of E_P[p] when a ≡ 3 (mod 8) FreyPackage.Mazur_Frey_of_a_mod_eight 104 below · cited by 1 · depth 5
• landmark No Galois-stable cofixed line at p=11 FreyPackage.frey_no_cofixed_eleven 3 below · cited by 1 · depth 5
• landmark Mazur at p≥ 17: no cofixed line FreyPackage.frey_no_cofixed_large 5,377 below · cited by 1 · depth 5
• landmark No Galois-stable cofixed line for p∈{5,7,13} FreyPackage.frey_no_cofixed_small 6 below · cited by 1 · depth 5
• landmark Reducible Frey representation yields a Galois-stable cofixed line FreyPackage.frey_reducible_hasCofixedLine 82 below · cited by 2 · depth 5
• landmark Level lowering for the Frey curve down to Γ₀(2) FreyPackage.level_lowering_to_two_of_conductorLevel 12,980 below · cited by 1 · depth 5
• landmark Conductor-level modularity of the Frey curve's mod-p representation FreyPackage.modularRepOfConductorLevel 27,798 below · cited by 1 · depth 5
• A prime divides the Frey model's discriminant iff it divides abc FreyPackage.dvd_freyCurveInt_discr_iff 0 below · cited by 9 · depth 6
• The integral Frey model has non-zero discriminant FreyPackage.freyCurveInt_discr_ne_zero 0 below · cited by 8 · depth 6
• Base change of the integral Frey model to ℚ FreyPackage.freyCurveInt_map 0 below · cited by 15 · depth 6
• Discriminant of the Frey curve: (abc)²ᵖ/2⁸ FreyPackage.freyCurve_discriminant 0 below · cited by 8 · depth 6
• landmark Frey p-torsion is unramified outside {2,p} FreyPackage.freyGaloisRep_isUnramifiedAt 42 below · cited by 2 · depth 6
• Frey curve with stable line: a p-torsion point with A-integral abscissa FreyPackage.frey_exists_p_torsion_integral_abscissa_of_stable_line 4 below · cited by 2 · depth 6
• Semistability of the integral Frey model FreyPackage.frey_isSemistableModel 0 below · cited by 4 · depth 6
• No cofixed line for Frey curves with a≡ 3(mod 8) FreyPackage.frey_no_cofixed_of_a_mod_eight 56 below · cited by 1 · depth 6
• Fixed-or-cofixed dichotomy for stable submodules of Frey p-torsion FreyPackage.frey_stable_submodule_fixed_or_cofixed 78 below · cited by 1 · depth 6
• Galois-fixed p-torsion of the Frey curve vanishes FreyPackage.frey_torsion_fixed_eq_zero 2 below · cited by 1 · depth 6
• landmark Mazur–Ribet level lowering at p for conductor levels FreyPackage.level_lowering_at_p_of_conductorLevel 6,090 below · cited by 1 · depth 6
• landmark Ribet level lowering at an odd prime q ≠ p FreyPackage.level_lowering_odd_prime_of_conductorLevel 12,496 below · cited by 1 · depth 6
• At primes dividing abc, c₄ of the Frey model is a unit FreyPackage.not_dvd_freyCurveInt_c4 0 below · cited by 5 · depth 6
• Level lowering at p for p-new modular witnesses FreyPackage.atPNewLowering 6,051 below · cited by 1 · depth 7
• Transfer of the Frey congruence to the canonical integral model FreyPackage.canonicalModelCongruence_of_eigenformResidualAttachment_of_congruence_outside 78 below · cited by 1 · depth 7
• landmark Eichler–Shimura residual attachment at every level FreyPackage.eigenformResidualAttachmentAtFamily 1,297 below · cited by 2 · depth 7
• The Frey curve has no rational point of order p FreyPackage.freyCurve_rational_p_torsion_eq_zero 0 below · cited by 1 · depth 7
• Frobenius swaps the branches when a ≡ 3 (mod 8) FreyPackage.frey_exists_decomposition_branch_swap_of_a_mod_eight 23 below · cited by 1 · depth 7
• The Frey curve's p-torsion is ramified at 2 FreyPackage.frey_exists_inertia_not_fixed_at_two 41 below · cited by 1 · depth 7
• Inertia at p acts trivially on a stable submodule of Frey E[p] or on its quotient FreyPackage.frey_inertia_at_p_trivial_on_submodule_or_quotient 34 below · cited by 1 · depth 7
• Inertia at 2 acts trivially on a stable line of Frey E[p] FreyPackage.frey_inertia_at_two_trivial_on_stable_submodule 9 below · cited by 1 · depth 7
• Bad reduction at primes dividing abc for all integral models FreyPackage.not_isGoodPrimeFor_of_isIntegralModelOf_freyCurve 3 below · cited by 2 · depth 7
• At-p level lowering for pinned p-new witnesses FreyPackage.atPNewLoweringAtUniform 6,003 below · cited by 1 · depth 8
• Field-coefficient residual realizations at every level M FreyPackage.eigenformRealizationSupplyFieldAtFamily 1,103 below · cited by 1 · depth 8
• Residual attachment from realisation supply at level M FreyPackage.eigenformResidualAttachmentAt_of_realizationSupplyFieldAt 1 below · cited by 1 · depth 8
• Inertia above p fixes a stable line or its quotient FreyPackage.frey_inertia_at_p_trivial_on_submodule_or_quotient_at 31 below · cited by 1 · depth 8
• Wild inertia at 2 fixes the p-torsion of a Frey curve FreyPackage.frey_wild_inertia_at_two_trivial 4 below · cited by 1 · depth 8
• Re-pinning a q-new modular witness to the canonical Frey model FreyPackage.modularRepOfLevelNewAtPinned_of_newAt 1,394 below · cited by 1 · depth 8
• Frey curve: p ∤ v₂(Δ) at the prime 2 FreyPackage.not_p_dvd_padicValInt_two_freyCurveInt_discr 1 below · cited by 1 · depth 8
• p divides v_ℓ(Δ) for the Frey curve over ℚ FreyPackage.p_dvd_padicValRat_freyCurve_discr 3 below · cited by 1 · depth 8
• Two-adic valuation of the integral Frey discriminant FreyPackage.padicValInt_two_freyCurveInt_discr 0 below · cited by 2 · depth 8
• Every good-at-3 integral model of the Frey curve has a₃=0 FreyPackage.freyCurveApOfModelThreeAgreement 17 below · cited by 1 · depth 9
• Inertia at p∣ abc acts trivially modulo a proper subspace FreyPackage.frey_inertia_at_p_filtration_of_dvd_abc_of_stable_line 26 below · cited by 1 · depth 9
• Frey curve, p ∤ abc: inertia above p modulo a proper subspace FreyPackage.frey_inertia_at_p_filtration_of_not_dvd_abc 6 below · cited by 1 · depth 9
• One-step level lowering at p for the Frey curve FreyPackage.mazurPrincipleAtPStep 6,002 below · cited by 1 · depth 9
• p divides v_ℓ(Δ) of the Frey curve at odd ℓ FreyPackage.p_dvd_padicValInt_freyCurveInt_discr 1 below · cited by 1 · depth 9
• Reverse-pin congruence at primes bad only for the witness model FreyPackage.routeAReversePinBadOnlySeam 1,372 below · cited by 1 · depth 9
• Two divides the discriminant of the integral Frey curve FreyPackage.two_dvd_freyCurveInt_delta 1 below · cited by 1 · depth 9
• Stable line yields p-torsion point with A-integral abscissa FreyPackage.frey_exists_p_torsion_integral_abscissa 4 below · cited by 1 · depth 10
• Frobenius-power density of kerρ∩ H₂ over a Galois base field FreyPackage.frobeniusPowerDense_inf_of_restrictionKer_le 21 below · cited by 3 · depth 10
• q-adic valuation of the integral Frey discriminant at odd q FreyPackage.padicValInt_freyCurveInt_discr 0 below · cited by 1 · depth 10
• Residual congruence at the canonical Frey model at W-bad primes FreyPackage.routeAReversePinBadOnlySeam_of_eigenformResidualAttachment 79 below · cited by 1 · depth 10
• Congruence at all good primes of the canonical Frey model FreyPackage.canonicalModelCongruence_of_eigenformResidualAttachment 78 below · cited by 1 · depth 11
• Inertia at p acts non-trivially on the p-th roots of unity FreyPackage.exists_inertia_cycloPinned_ne_one_v2 46 below · cited by 1 · depth 13

FreyPackage.ModMCarrier 2

• Joint injectivity of the two degeneracy maps in weight 2 FreyPackage.ModMCarrier.levelInclusionLin_add_rescaleLin_eq_zero 4 below · cited by 3 · depth 15
• Rescaling with d=1 equals the level inclusion FreyPackage.ModMCarrier.rescaleLin_eq_levelInclusionLin 0 below · cited by 1 · depth 16