AlgebraicCurve.CurveModel.one_lt_finrankAlong_of_nontrivial_deck
A nonidentity actual deck transformation supplies the strict degree inequality needed by the geometric H¹ cardinality argument.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open CategoryTheory AlgebraicGeometry AlgebraicCurve
open CategoryTheory.PreGaloisCategory EtaleFundamentalGroups
namespace AlgebraicCurve.CurveModelLean source · statement
theorem one_lt_finrankAlong_of_nontrivial_deck
{K F E : Type} [Field K] [IsAlgClosed K]
[Field F] [Field E] [Algebra K F] [Algebra K E]
(M : CurveModel K F) (N : CurveModel K E) [IsNormalIntegral M.C]
(d : N.C ⟶ M.C) (hd : d ≫ M.toBase = N.toBase) [IsFiniteEtale d]
(σ : Aut (FiniteEtale.mk d)) (hne : σ ≠ 1) :
1 < finrankAlong K (M.finiteEtaleFieldMap N d hd)