Module

Surjective_algebraMap_of_injective_restrict_place_of_isAlgClosed.lean

Nyll.AlgebraicCurves.Places.Surjective_algebraMap_of_injective_restrict_place_of_isAlgClosed

12 declarations indexed from sourceView source ↗

Module documentation

Surjective algebra Map of injective restrict place of is Alg Closed

Imports13

Imported by1

Nyll.AlgebraicCurves.Places.All

theorem

ord_pos_of_not_isUnit

L61 ↗

AlgebraicCurves.Places.Proofs.Surjective_algebraMap_of_injective_restrict_place_of_isAlgClosed.P2mKcDegreeOneByInjectivePlaces.ord_pos_of_not_isUnit

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Surjective_algebraMap_of_injective_restrict_place_of_isAlgClosed
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
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
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve IntermediateField
namespace P2mKcDegreeOneByInjectivePlaces
section PlaceFacts
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem ord_pos_of_not_isUnit (v : Place K F) {a : v.toValuationSubring} (ha : a ≠ 0)
    (hu : ¬IsUnit a) : 0 < v.ord (a : F)

theorem

ord_neg_of_not_mem

L74 ↗

AlgebraicCurves.Places.Proofs.Surjective_algebraMap_of_injective_restrict_place_of_isAlgClosed.P2mKcDegreeOneByInjectivePlaces.ord_neg_of_not_mem

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Surjective_algebraMap_of_injective_restrict_place_of_isAlgClosed
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
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
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve IntermediateField
namespace P2mKcDegreeOneByInjectivePlaces
section PlaceFacts
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem ord_neg_of_not_mem (v : Place K F) {f : F} (hf : f ∉ v.toValuationSubring) :
    v.ord f < 0

theorem

mem_of_ord_nonneg

L100 ↗

AlgebraicCurves.Places.Proofs.Surjective_algebraMap_of_injective_restrict_place_of_isAlgClosed.P2mKcDegreeOneByInjectivePlaces.mem_of_ord_nonneg

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Surjective_algebraMap_of_injective_restrict_place_of_isAlgClosed
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
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
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve IntermediateField
namespace P2mKcDegreeOneByInjectivePlaces
section PlaceFacts
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mem_of_ord_nonneg (v : Place K F) {f : F} (h : 0 ≤ v.ord f) :
    f ∈ v.toValuationSubring

theorem

ord_nonneg_of_mem

L105 ↗

AlgebraicCurves.Places.Proofs.Surjective_algebraMap_of_injective_restrict_place_of_isAlgClosed.P2mKcDegreeOneByInjectivePlaces.ord_nonneg_of_mem

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Surjective_algebraMap_of_injective_restrict_place_of_isAlgClosed
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
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
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve IntermediateField
namespace P2mKcDegreeOneByInjectivePlaces
section PlaceFacts
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem ord_nonneg_of_mem (v : Place K F) {f : F} (hf : f ∈ v.toValuationSubring) :
    0 ≤ v.ord f

theorem

mem_maximalIdeal_of_ord_pos

L115 ↗

AlgebraicCurves.Places.Proofs.Surjective_algebraMap_of_injective_restrict_place_of_isAlgClosed.P2mKcDegreeOneByInjectivePlaces.mem_maximalIdeal_of_ord_pos

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Surjective_algebraMap_of_injective_restrict_place_of_isAlgClosed
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
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
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve IntermediateField
namespace P2mKcDegreeOneByInjectivePlaces
section PlaceFacts
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem mem_maximalIdeal_of_ord_pos (v : Place K F) {f : F} (hf : 0 < v.ord f) :
    ∃ h : f ∈ v.toValuationSubring,
      (⟨f, h⟩ : v.toValuationSubring) ∈ IsLocalRing.maximalIdeal v.toValuationSubring

theorem

isUnit_algebraMap

L127 ↗

AlgebraicCurves.Places.Proofs.Surjective_algebraMap_of_injective_restrict_place_of_isAlgClosed.P2mKcDegreeOneByInjectivePlaces.isUnit_algebraMap

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Surjective_algebraMap_of_injective_restrict_place_of_isAlgClosed
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
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
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve IntermediateField
namespace P2mKcDegreeOneByInjectivePlaces
section PlaceFacts
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem isUnit_algebraMap (v : Place K F) {a : K} (ha : a ≠ 0) :
    IsUnit (⟨algebraMap K F a, v.algebraMap_mem' a⟩ : v.toValuationSubring)

theorem

eq_of_ord_sub_algebraMap_pos

L134 ↗

AlgebraicCurves.Places.Proofs.Surjective_algebraMap_of_injective_restrict_place_of_isAlgClosed.P2mKcDegreeOneByInjectivePlaces.eq_of_ord_sub_algebraMap_pos

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Surjective_algebraMap_of_injective_restrict_place_of_isAlgClosed
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
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
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve IntermediateField
namespace P2mKcDegreeOneByInjectivePlaces
section PlaceFacts
variable {K F : Type*} [Field K] [Field F] [Algebra K F]

Lean source · statement

theorem eq_of_ord_sub_algebraMap_pos (v : Place K F) (t : F) {c c' : K}
    (hc : 0 < v.ord (t - algebraMap K F c)) (hc' : 0 < v.ord (t - algebraMap K F c')) :
    c = c'

theorem

ramificationIndex_eq_finrank

L158 ↗

AlgebraicCurves.Places.Proofs.Surjective_algebraMap_of_injective_restrict_place_of_isAlgClosed.P2mKcDegreeOneByInjectivePlaces.ramificationIndex_eq_finrank

Source context 10 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Surjective_algebraMap_of_injective_restrict_place_of_isAlgClosed
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
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
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve IntermediateField
namespace P2mKcDegreeOneByInjectivePlaces
section TotalRamification
variable {K F F' : Type*} [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F']
  [Algebra F F'] [IsScalarTower K F F']

Lean source · full declaration

theorem ramificationIndex_eq_finrank [IsAlgClosed K] [IsCurveOver K F] [IsCurveOver K F']
    [FiniteDimensional F F'] [Algebra.IsSeparable F F']
    (hinj : Function.Injective (fun w : Place K F' => w.restrict F)) (w : Place K F') :
    w.ramificationIndex F = Module.finrank F F' := by
  have hfib : (w.restrict F).fiber F' = {w} := by
    ext w'
    rw [Place.mem_fiber, Finset.mem_singleton]
    exact ⟨fun h => hinj h, fun h => h ▸ rfl⟩
  have hid := Place.sum_ramificationIndex_mul_inertiaDeg (K := K) (F := F) (F' := F')
    (w.restrict F)
  rw [hfib, Finset.sum_singleton] at hid
  have hdeg : w.inertiaDeg F = 1 := by
    have h := w.deg_restrict_mul_inertiaDeg (F := F)
    rw [IsCurveOver.deg_eq_one_of_isAlgClosed, IsCurveOver.deg_eq_one_of_isAlgClosed,
      one_mul] at h
    exact h
  rw [hdeg, Nat.cast_one, mul_one] at hid
  exact_mod_cast hid

theorem

differentialCoeff_D_regular

L181 ↗

AlgebraicCurves.Places.Proofs.Surjective_algebraMap_of_injective_restrict_place_of_isAlgClosed.P2mKcDegreeOneByInjectivePlaces.differentialCoeff_D_regular

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Surjective_algebraMap_of_injective_restrict_place_of_isAlgClosed
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
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
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve IntermediateField
namespace P2mKcDegreeOneByInjectivePlaces
section Finiteness

Lean source · statement

theorem differentialCoeff_D_regular {K F' : Type*} [Field K] [Field F'] [Algebra K F']
    [PerfectField K] [Algebra.EssFiniteType K F'] [IsCurveOver K F']
    [∀ w : Place K F', w.DCoordGenerates]
    (w : Place K F') (u : F') (_hu : u ≠ 0) (hord : w.ord u = 0) :
    w.differentialCoeff (KaehlerDifferential.D K F' u) = 0 ∨
      0 ≤ w.ord (w.differentialCoeff (KaehlerDifferential.D K F' u))

theorem

finite_place_of_one_lt

L194 ↗

AlgebraicCurves.Places.Proofs.Surjective_algebraMap_of_injective_restrict_place_of_isAlgClosed.P2mKcDegreeOneByInjectivePlaces.finite_place_of_one_lt

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Surjective_algebraMap_of_injective_restrict_place_of_isAlgClosed
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
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
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve IntermediateField
namespace P2mKcDegreeOneByInjectivePlaces
section Finiteness

Lean source · full declaration

theorem finite_place_of_one_lt (K F F' : Type) [Field K] [Field F] [Field F'] [Algebra K F]
    [Algebra K F'] [Algebra F F'] [IsScalarTower K F F']
    [IsAlgClosed K] [CharZero K] [IsCurveOver K F] [Algebra.EssFiniteType K F] [IsCurveOver K F']
    [Algebra.EssFiniteType K F'] [Module.Finite F F']
    (hinj : Function.Injective (fun w : Place K F' => w.restrict F))
    (hn : 1 < Module.finrank F F') : Finite (Place K F') := by
  classical
  have : CharZero F := charZero_of_injective_algebraMap (algebraMap K F).injective
  have : CharZero F' := charZero_of_injective_algebraMap (algebraMap K F').injective
  have hDC : ∀ v : Place K F, v.DCoordGenerates := dCoordGenerates_of_isCurveOver
  have hDC' : ∀ w : Place K F', w.DCoordGenerates := dCoordGenerates_of_isCurveOver
  have : HasCanonicalDivisor (K := K) (F := F) := hasCanonicalDivisor_of_isCurveOver
  have : HasCanonicalDivisor (K := K) (F := F') := hasCanonicalDivisor_of_isCurveOver
  obtain ⟨ω₀, hω₀⟩ := exists_ne (0 : Ω[F⁄K])
  have he : ∀ w : Place K F', w.ramificationIndex F = Module.finrank F F' :=
    ramificationIndex_eq_finrank hinj
  have htame : ∀ w : Place K F', ((w.ramificationIndex F : ℕ) : F') ≠ 0 := fun w => by
    exact_mod_cast (w.ramificationIndex_pos (F := F)).ne'
  have hmap : ∀ w : Place K F', w.ordDifferential (KaehlerDifferential.map K K F F' ω₀)
      = (w.ramificationIndex F : ℤ) * (w.restrict F).ordDifferential ω₀
          + ((w.ramificationIndex F : ℤ) - 1) := fun w =>
    ordDifferential_map_eq (K := K) (F := F) (F' := F')
      (fun w u hu hord => differentialCoeff_D_regular w u hu hord) htame hω₀ w
  obtain ⟨D₀, hD₀⟩ := HasCanonicalDivisor.exists_divisor ω₀ hω₀
  have hD₁ : ∃ D₁ : Divisor K F',
      ∀ w, D₁ w = w.ordDifferential (KaehlerDifferential.map K K F F' ω₀) := by
    by_cases h0 : KaehlerDifferential.map K K F F' ω₀ = 0
    · refine ⟨0, fun w => ?_⟩
      rw [h0, Place.ordDifferential, Place.differentialCoeff_zero, Place.ord_zero]
      rfl
    · exact HasCanonicalDivisor.exists_divisor _ h0
  obtain ⟨D₁, hD₁⟩ := hD₁
  have hcover : (Set.univ : Set (Place K F')) ⊆
      (D₁.support : Set (Place K F')) ∪
        (fun w : Place K F' => w.restrict F) ⁻¹' (D₀.support : Set (Place K F)) := by
    intro w _
    by_contra hw
    simp only [Set.mem_union, Finset.mem_coe, Finsupp.mem_support_iff, Set.mem_preimage,
      not_or, not_not] at hw
    have h := hmap w
    rw [← hD₁, ← hD₀, hw.1, hw.2, he w, mul_zero, zero_add] at h
    have h' : (Module.finrank F F' : ℤ) = 1 := by linarith
    have : Module.finrank F F' = 1 := by exact_mod_cast h'
    omega
  have hfin : (Set.univ : Set (Place K F')).Finite :=
    ((D₁.support.finite_toSet).union
      ((D₀.support.finite_toSet).preimage hinj.injOn)).subset hcover
  exact Set.finite_univ_iff.mp hfin

theorem

infinite_place

L247 ↗

AlgebraicCurves.Places.Proofs.Surjective_algebraMap_of_injective_restrict_place_of_isAlgClosed.P2mKcDegreeOneByInjectivePlaces.infinite_place

Source context 9 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Surjective_algebraMap_of_injective_restrict_place_of_isAlgClosed
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
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
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve IntermediateField
namespace P2mKcDegreeOneByInjectivePlaces
section Infinitude

Lean source · statement

theorem infinite_place (K F' : Type) [Field K] [Field F'] [Algebra K F'] [IsAlgClosed K]
    [CharZero K] [IsCurveOver K F'] [Algebra.EssFiniteType K F'] : Infinite (Place K F')

theorem

surjective_algebraMap_of_injective_restrict_place_of_isAlgClosed

L278 ↗

AlgebraicCurve.surjective_algebraMap_of_injective_restrict_place_of_isAlgClosed

Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs
namespace Surjective_algebraMap_of_injective_restrict_place_of_isAlgClosed
attribute [-instance]
  instIsRankOneDiscreteWithZeroMultiplicativeIntAdicValuation
  instIsTrivialOnWithZeroMultiplicativeIntAdicValuation
  instIsPrimeCenter
  instIsFractionRingIntegralClosureAt
  instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
  instIsDedekindDomainIntegralClosureAt
  instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
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
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
  AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
  AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
open AlgebraicCurve IntermediateField
open P2mKcDegreeOneByInjectivePlaces in

Lean source · full declaration

theorem _root_.AlgebraicCurve.surjective_algebraMap_of_injective_restrict_place_of_isAlgClosed
    (K F F' : Type) [Field K] [Field F] [Field F'] [Algebra K F] [Algebra K F'] [Algebra F F']
      [IsScalarTower K F F']
    [IsAlgClosed K] [CharZero K] [IsCurveOver K F] [Algebra.EssFiniteType K F] [IsCurveOver K F']
      [Algebra.EssFiniteType K F']
    [Module.Finite F F']
    (hinj : Function.Injective (fun w : Place K F' => w.restrict F)) :
    Function.Surjective (algebraMap F F') := by
  by_contra hns
  have hn : 1 < Module.finrank F F' := by
    have hpos : 0 < Module.finrank F F' := Module.finrank_pos
    rcases (Nat.succ_le_of_lt hpos).eq_or_lt with h1 | h1
    · exact absurd ((Algebra.finrank_eq_one_iff_bijective_algebraMap).mp h1.symm).2 hns
    · exact h1
  have := finite_place_of_one_lt K F F' hinj hn
  exact (infinite_place K F').not_finite ‹_›

Module documentation

Surjective algebra Map of injective restrict place of is Alg Closed

Declarations