Module

LocalUnramifiedRamification.lean

Nyll.AlgebraicCurves.Places.LocalUnramifiedRamification

4 declarations indexed from sourceView source ↗

Module documentation

Unramified local rings have ramification index one

This local-ring form of the existing curve-model argument applies equally to proper curves and open curves. The local rings are identified with the actual valuation rings, and the map is the actual local homomorphism.

Imports3

Nyll.AlgebraicCurves.Divisors.Correspondences
Nyll.AlgebraicCurves.Places.Place_restrict_eq_of_forall_mem
Mathlib.RingTheory.Unramified.LocalRing

Imported by3

theorem

maximalIdeal_map_equiv

L29 ↗

AlgebraicCurve.Place.maximalIdeal_map_equiv

Source context 2 commands

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

noncomputable section
namespace AlgebraicCurve.Place

Lean source · statement

theorem maximalIdeal_map_equiv
    {A B : Type*} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B]
    (e : A ≃+* B) :
    (IsLocalRing.maximalIdeal A).map e.toRingHom = IsLocalRing.maximalIdeal B

theorem

ramificationIndexAlong_eq_one_of_local_map

L54 ↗

AlgebraicCurve.Place.ramificationIndexAlong_eq_one_of_local_map

Documentation

Formal unramifiedness of the actual local map gives ramification index one, without requiring either curve to be proper.

Source context 2 commands

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

noncomputable section
namespace AlgebraicCurve.Place

Lean source · statement

theorem ramificationIndexAlong_eq_one_of_local_map
    {K F E : Type*} [Field K] [Field F] [Field E] [Algebra K F] [Algebra K E]
    (φ : F →ₐ[K] E) (hφ : φ.toRingHom.IsIntegral)
    (v : Place K F) (w : Place K E)
    {A B : Type*} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B]
    (eA : A ≃+* ↥v.toValuationSubring)
    (eB : B ≃+* ↥w.toValuationSubring)
    [Algebra A B] [IsLocalHom (algebraMap A B)]
    [Algebra.EssFiniteType A B] [Algebra.FormallyUnramified A B]
    (hcompat : ∀ x : A, ((eB (algebraMap A B x) : ↥w.toValuationSubring) : E) =
      φ ((eA x : ↥v.toValuationSubring) : F)) :
    ramificationIndexAlong φ w = 1

theorem

restrictAlong_eq_of_local_map

L107 ↗

AlgebraicCurve.Place.restrictAlong_eq_of_local_map

Documentation

The same actual local-ring square identifies the restricted place.

Source context 2 commands

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

noncomputable section
namespace AlgebraicCurve.Place

Lean source · statement

theorem restrictAlong_eq_of_local_map
    {K F E : Type*} [Field K] [Field F] [Field E] [Algebra K F] [Algebra K E]
    (φ : F →ₐ[K] E) (hφ : φ.toRingHom.IsIntegral)
    (v : Place K F) (w : Place K E)
    {A B : Type*} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B]
    (eA : A ≃+* ↥v.toValuationSubring)
    (eB : B ≃+* ↥w.toValuationSubring)
    [Algebra A B] [IsLocalHom (algebraMap A B)]
    [Algebra.EssFiniteType A B] [Algebra.FormallyUnramified A B]
    (hcompat : ∀ x : A, ((eB (algebraMap A B x) : ↥w.toValuationSubring) : E) =
      φ ((eA x : ↥v.toValuationSubring) : F)) :
    w.restrictAlong φ hφ = v

theorem

ord_dvd_of_local_unramified_root

L133 ↗

AlgebraicCurve.Place.ord_dvd_of_local_unramified_root

Documentation

A root in an unramified extension of the actual local fraction fields forces divisibility of the original valuation order.

Source context 2 commands

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

noncomputable section
namespace AlgebraicCurve.Place

Lean source · statement

theorem ord_dvd_of_local_unramified_root
    {K F E : Type*} [Field K] [Field F] [Field E] [Algebra K F] [Algebra K E]
    (φ : F →ₐ[K] E) (hφ : φ.toRingHom.IsIntegral)
    (v : Place K F) (w : Place K E)
    {A B : Type*} [CommRing A] [CommRing B] [IsLocalRing A] [IsLocalRing B]
    (eA : A ≃+* ↥v.toValuationSubring)
    (eB : B ≃+* ↥w.toValuationSubring)
    [Algebra A B] [IsLocalHom (algebraMap A B)]
    [Algebra.EssFiniteType A B] [Algebra.FormallyUnramified A B]
    (hcompat : ∀ x : A, ((eB (algebraMap A B x) : ↥w.toValuationSubring) : E) =
      φ ((eA x : ↥v.toValuationSubring) : F))
    (a : F) (b : E) (n : ℕ) (hb : b ^ n = φ a) :
    (n : ℤ) ∣ v.ord a

Module documentation

Unramified local rings have ramification index one

Declarations

maximalIdeal_map_equiv

ramificationIndexAlong_eq_one_of_local_map

restrictAlong_eq_of_local_map

ord_dvd_of_local_unramified_root