NYLL
Module

Place_ramificationIndex_forgetConstants_eq_one_of_isConstantFieldExtension.lean

Nyll.AlgebraicCurves.Places.Place_ramificationIndex_forgetConstants_eq_one_of_isConstantFieldExtension
10 declarations indexed from sourceView source ↗

Module documentation

Place ramification Index forget Constants eq one of is Constant Field Extension

Imports4
Imported by6

Declarations

theorem

ord_nonneg_of_mem

L34 ↗
AlgebraicCurves.Places.Proofs.PlaceRamificationIndexForget.S12CF.ord_nonneg_of_mem
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceRamificationIndexForget
noncomputable section
open IntermediateField AlgebraicCurve Polynomial
attribute [local instance 0] AlgebraicCurve.Place.valuationSubringAlgebra
namespace S12CF
Lean source · statement
theorem ord_nonneg_of_mem {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
    {f : F} (hf : f ∈ v.toValuationSubring) : 0 ≤ v.ord f
theorem

mem_of_ord_nonneg

L50 ↗
AlgebraicCurves.Places.Proofs.PlaceRamificationIndexForget.S12CF.mem_of_ord_nonneg
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceRamificationIndexForget
noncomputable section
open IntermediateField AlgebraicCurve Polynomial
attribute [local instance 0] AlgebraicCurve.Place.valuationSubringAlgebra
namespace S12CF
Lean source · statement
theorem mem_of_ord_nonneg {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F)
    {f : F} (hf : f ≠ 0) (h : 0 ≤ v.ord f) : f ∈ v.toValuationSubring
theorem

exists_ord_eq_one

L58 ↗
AlgebraicCurves.Places.Proofs.PlaceRamificationIndexForget.S12CF.exists_ord_eq_one
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceRamificationIndexForget
noncomputable section
open IntermediateField AlgebraicCurve Polynomial
attribute [local instance 0] AlgebraicCurve.Place.valuationSubringAlgebra
namespace S12CF
Lean source · statement
theorem exists_ord_eq_one {K F : Type*} [Field K] [Field F] [Algebra K F] (v : Place K F) :
    ∃ π : F, v.ord π = 1
theorem

minpoly_eq_map_of_constants

L63 ↗
AlgebraicCurves.Places.Proofs.PlaceRamificationIndexForget.S12CF.minpoly_eq_map_of_constants
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceRamificationIndexForget
noncomputable section
open IntermediateField AlgebraicCurve Polynomial
attribute [local instance 0] AlgebraicCurve.Place.valuationSubringAlgebra
namespace S12CF
Lean source · statement
theorem minpoly_eq_map_of_constants {K F L : Type*} [Field K] [Field F] [Field L]
    [Algebra K F] [Algebra F L] [Algebra K L] [IsScalarTower K F L]
    (hconst : ∀ y : F, IsAlgebraic K y → y ∈ (algebraMap K F).range) {α : L} (hα : IsIntegral K α) :
    minpoly F α = (minpoly K α).map (algebraMap K F)
theorem

isScalarTower_valuationSubring

L98 ↗
AlgebraicCurves.Places.Proofs.PlaceRamificationIndexForget.S12CF.isScalarTower_valuationSubring
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceRamificationIndexForget
noncomputable section
open IntermediateField AlgebraicCurve Polynomial
attribute [local instance 0] AlgebraicCurve.Place.valuationSubringAlgebra
namespace S12CF
section FiniteLayer
variable {K F L : Type*} [Field K] [Field F] [Field L]
  [Algebra K F] [Algebra F L] [Algebra K L] [IsScalarTower K F L]
  [FiniteDimensional F L] [Algebra.IsSeparable F L]
omit [FiniteDimensional F L] [Algebra.IsSeparable F L] in
Lean source · statement
theorem isScalarTower_valuationSubring (v : Place K F) :
    IsScalarTower K v.toValuationSubring L
theorem

differentIdeal_integralClosureAt_eq_top

L105 ↗
AlgebraicCurves.Places.Proofs.PlaceRamificationIndexForget.S12CF.differentIdeal_integralClosureAt_eq_top
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceRamificationIndexForget
noncomputable section
open IntermediateField AlgebraicCurve Polynomial
attribute [local instance 0] AlgebraicCurve.Place.valuationSubringAlgebra
namespace S12CF
section FiniteLayer
variable {K F L : Type*} [Field K] [Field F] [Field L]
  [Algebra K F] [Algebra F L] [Algebra K L] [IsScalarTower K F L]
  [FiniteDimensional F L] [Algebra.IsSeparable F L]
Lean source · statement
theorem differentIdeal_integralClosureAt_eq_top
    (hconst : ∀ y : F, IsAlgebraic K y → y ∈ (algebraMap K F).range)
    {α : L} (hα : IsIntegral K α) (hsep : (minpoly K α).Separable)
    (htop : Algebra.adjoin F ({α} : Set L) = ⊤) (v : Place K F) :
    differentIdeal v.toValuationSubring (Place.integralClosureAt L v) = ⊤
theorem

ramificationIndex_eq_one_finiteLayer

L152 ↗
AlgebraicCurves.Places.Proofs.PlaceRamificationIndexForget.S12CF.ramificationIndex_eq_one_finiteLayer
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceRamificationIndexForget
noncomputable section
open IntermediateField AlgebraicCurve Polynomial
attribute [local instance 0] AlgebraicCurve.Place.valuationSubringAlgebra
namespace S12CF
section FiniteLayer
variable {K F L : Type*} [Field K] [Field F] [Field L]
  [Algebra K F] [Algebra F L] [Algebra K L] [IsScalarTower K F L]
  [FiniteDimensional F L] [Algebra.IsSeparable F L]
Lean source · statement
theorem ramificationIndex_eq_one_finiteLayer
    (hconst : ∀ y : F, IsAlgebraic K y → y ∈ (algebraMap K F).range)
    {α : L} (hα : IsIntegral K α) (hsep : (minpoly K α).Separable)
    (htop : Algebra.adjoin F ({α} : Set L) = ⊤) (W : Place K L) :
    W.ramificationIndex F = 1
theorem

exists_finset_mem_adjoin

L189 ↗
AlgebraicCurves.Places.Proofs.PlaceRamificationIndexForget.S12CF.exists_finset_mem_adjoin
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceRamificationIndexForget
noncomputable section
open IntermediateField AlgebraicCurve Polynomial
attribute [local instance 0] AlgebraicCurve.Place.valuationSubringAlgebra
namespace S12CF
section Reduction
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
Lean source · statement
theorem exists_finset_mem_adjoin {t : F'} (ht : t ∈ Algebra.adjoin F (Set.range (algebraMap K'
  F'))) :
    ∃ S : Finset K', t ∈ Algebra.adjoin F ((algebraMap K' F') '' (S : Set K'))
theorem

main

L211 ↗
AlgebraicCurves.Places.Proofs.PlaceRamificationIndexForget.S12CF.main
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceRamificationIndexForget
noncomputable section
open IntermediateField AlgebraicCurve Polynomial
attribute [local instance 0] AlgebraicCurve.Place.valuationSubringAlgebra
namespace S12CF
section Reduction
variable {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
  [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
  [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
Lean source · statement
theorem main [Algebra.IsAlgebraic K K'] [Algebra.IsSeparable K K'] [Algebra.IsIntegral F F']
    (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
    (hconst : ∀ y : F, IsAlgebraic K y → y ∈ (algebraMap K F).range)
    (W : Place K' F') :
    (W.forgetConstants (K := K)).ramificationIndex F = 1
theorem

ramificationIndex_forgetConstants_eq_one_of_isConstantFieldExtension

L322 ↗
AlgebraicCurve.Place.ramificationIndex_forgetConstants_eq_one_of_isConstantFieldExtension
Source context 2 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceRamificationIndexForget
Lean source · statement
theorem
  _root_.AlgebraicCurve.Place.ramificationIndex_forgetConstants_eq_one_of_isConstantFieldExtension
    {K K' F F' : Type*} [Field K] [Field K'] [Field F] [Field F']
    [Algebra K K'] [Algebra K' F'] [Algebra K F'] [IsScalarTower K K' F']
    [Algebra K F] [Algebra F F'] [IsScalarTower K F F']
    [Algebra.IsAlgebraic K K'] [Algebra.IsSeparable K K'] [Algebra.IsIntegral F F']
    (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
    (hconst : ∀ y : F, IsAlgebraic K y → y ∈ (algebraMap K F).range)
    (W : AlgebraicCurve.Place K' F') :
    (W.forgetConstants (K := K)).ramificationIndex F = 1

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.