AlgebraicCurve.Place.card_fiberAlong_le_finrankAlong_and_iff
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_card_fiberAlong_le_finrankAlong_and_iff
attribute [-instance]
AlgebraicCurve.Place.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
AlgebraicCurve.Place.instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
attribute [-simp] AlgebraicCurve.Place.congrEquiv_symm_apply
AlgebraicCurve.RationalFunctionField.heightOneSpectrumOfIrreducible_asIdeal
AlgebraicCurve.Place.congrRingEquiv_toValuationSubring AlgebraicCurve.Place.congrEquiv_apply
AlgebraicCurve.Place.coe_comapSymmRingEquiv_apply
AlgebraicCurve.RationalFunctionField.deg_placeOfPoint
open AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.Place.card_fiberAlong_le_finrankAlong_and_iff
{K F F' : Type*} [Field K] [IsAlgClosed K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
[IsCurveOver K F] [Algebra.EssFiniteType K F] [IsCurveOver K F'] [Algebra.EssFiniteType K F']
(φ : F →ₐ[K] F') (hφ : φ.toRingHom.IsIntegral) (hfin : FiniteAlong K φ) (hsep : SeparableAlong
K φ)
(P : Place K F) :
(Place.fiberAlong φ hφ P).card ≤ finrankAlong K φ ∧
((Place.fiberAlong φ hφ P).card = finrankAlong K φ ↔
∀ W ∈ Place.fiberAlong φ hφ P, W.ramificationIndexAlong φ = 1)