Module

Place_inertiaDegAlong_comp.lean

Nyll.AlgebraicCurves.Places.Place_inertiaDegAlong_comp

4 declarations indexed from sourceView source ↗

Module documentation

Place inertia Deg Along comp

Imports1

Nyll.AlgebraicCurves.Divisors.Correspondences

Imported by5

def

valuationSubringEquivOfEq

L25 ↗

AlgebraicCurves.Places.Proofs.Place_inertiaDegAlong_comp.valuationSubringEquivOfEq

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_inertiaDegAlong_comp
open IsDedekindDomain AlgebraicCurve

Lean source · statement

def valuationSubringEquivOfEq
    {K F : Type*} [Field K] [Field F] [Algebra K F]
    (v v' : Place K F) (h : v = v') : v.toValuationSubring ≃+* v'.toValuationSubring

theorem

coe_valuationSubringEquivOfEq

L31 ↗

AlgebraicCurves.Places.Proofs.Place_inertiaDegAlong_comp.coe_valuationSubringEquivOfEq

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_inertiaDegAlong_comp
open IsDedekindDomain AlgebraicCurve

Lean source · statement

theorem coe_valuationSubringEquivOfEq
    {K F : Type*} [Field K] [Field F] [Algebra K F]
    (v v' : Place K F) (h : v = v') (a : v.toValuationSubring) :
    ((valuationSubringEquivOfEq v v' h a : v'.toValuationSubring) : F) = (a : F)

def

residueFieldEquivOfEq

L38 ↗

AlgebraicCurves.Places.Proofs.Place_inertiaDegAlong_comp.residueFieldEquivOfEq

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_inertiaDegAlong_comp
open IsDedekindDomain AlgebraicCurve

Lean source · statement

def residueFieldEquivOfEq
    {K F : Type*} [Field K] [Field F] [Algebra K F]
    (v v' : Place K F) (h : v = v') : v.ResidueField ≃+* v'.ResidueField

theorem

inertiaDegAlong_comp

L43 ↗

AlgebraicCurve.Place.inertiaDegAlong_comp

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.Place_inertiaDegAlong_comp
open IsDedekindDomain AlgebraicCurve

Lean source · statement

theorem _root_.AlgebraicCurve.Place.inertiaDegAlong_comp {K F F' F'' : Type*} [Field K] [Field F]
  [Field F'] [Field F''] [Algebra K F] [Algebra K F'] [Algebra K F''] (φ : F →ₐ[K] F') (χ : F'
  →ₐ[K] F'') (hφ : φ.toRingHom.IsIntegral) (hχ : χ.toRingHom.IsIntegral) (hχφ : (χ.comp
  φ).toRingHom.IsIntegral) (W : Place K F'') : W.inertiaDegAlong (χ.comp φ) hχφ = W.inertiaDegAlong
  χ hχ * (W.restrictAlong χ hχ).inertiaDegAlong φ hφ

Module documentation

Place inertia Deg Along comp

Declarations

valuationSubringEquivOfEq

coe_valuationSubringEquivOfEq

residueFieldEquivOfEq

inertiaDegAlong_comp