NYLL
Module

Place_exists_forgetConstants_restrict_eq_of_isConstantFieldExtension.lean

Nyll.AlgebraicCurves.Places.Place_exists_forgetConstants_restrict_eq_of_isConstantFieldExtension
20 declarations indexed from sourceView source ↗

Module documentation

Place exists forget Constants restrict eq of is Constant Field Extension

Imports4
Imported by5

Declarations

theorem

ord_nonneg_of_mem

L34 ↗
AlgebraicCurves.Places.Proofs.PlaceExistsForgetConstants.S12CT.ord_nonneg_of_mem
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsForgetConstants
noncomputable section
open IntermediateField AlgebraicCurve Polynomial
attribute [local instance 0] AlgebraicCurve.Place.valuationSubringAlgebra
namespace S12CT
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.PlaceExistsForgetConstants.S12CT.mem_of_ord_nonneg
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsForgetConstants
noncomputable section
open IntermediateField AlgebraicCurve Polynomial
attribute [local instance 0] AlgebraicCurve.Place.valuationSubringAlgebra
namespace S12CT
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.PlaceExistsForgetConstants.S12CT.exists_ord_eq_one
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsForgetConstants
noncomputable section
open IntermediateField AlgebraicCurve Polynomial
attribute [local instance 0] AlgebraicCurve.Place.valuationSubringAlgebra
namespace S12CT
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
instance

instIsScalarTowerIntermediateFieldBase

L63 ↗
AlgebraicCurves.Places.Proofs.PlaceExistsForgetConstants.S12CT.instIsScalarTowerIntermediateFieldBase
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsForgetConstants
noncomputable section
open IntermediateField AlgebraicCurve Polynomial
attribute [local instance 0] AlgebraicCurve.Place.valuationSubringAlgebra
namespace S12CT
Lean source · statement
instance instIsScalarTowerIntermediateFieldBase {K F F' : Type*} [Field K] [Field F] [Field
  F']
    [Algebra K F] [Algebra F F'] [Algebra K F'] [IsScalarTower K F F'] (L : IntermediateField F
      F') :
    IsScalarTower K L F'
theorem

minpoly_eq_map_of_constants

L70 ↗
AlgebraicCurves.Places.Proofs.PlaceExistsForgetConstants.S12CT.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.PlaceExistsForgetConstants
noncomputable section
open IntermediateField AlgebraicCurve Polynomial
attribute [local instance 0] AlgebraicCurve.Place.valuationSubringAlgebra
namespace S12CT
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)
instance

instIsScalarTowerValuationSubringLayer

L104 ↗
AlgebraicCurves.Places.Proofs.PlaceExistsForgetConstants.S12CT.instIsScalarTowerValuationSubringLayer
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsForgetConstants
noncomputable section
open IntermediateField AlgebraicCurve Polynomial
attribute [local instance 0] AlgebraicCurve.Place.valuationSubringAlgebra
namespace S12CT
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
instance instIsScalarTowerValuationSubringLayer (v : Place K F) :
    IsScalarTower K v.toValuationSubring L
theorem

isUnit_aeval_derivative_minpoly

L112 ↗
AlgebraicCurves.Places.Proofs.PlaceExistsForgetConstants.S12CT.isUnit_aeval_derivative_minpoly
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsForgetConstants
noncomputable section
open IntermediateField AlgebraicCurve Polynomial
attribute [local instance 0] AlgebraicCurve.Place.valuationSubringAlgebra
namespace S12CT
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 isUnit_aeval_derivative_minpoly
    (hconst : ∀ y : F, IsAlgebraic K y → y ∈ (algebraMap K F).range)
    {α : L} (hα : IsIntegral K α) (hsep : (minpoly K α).Separable) (v : Place K F) :
    IsUnit (Polynomial.aeval (⟨α, hα.tower_top⟩ : Place.integralClosureAt L v)
      (Polynomial.derivative (minpoly v.toValuationSubring (⟨α, hα.tower_top⟩ :
        Place.integralClosureAt L v))))
theorem

differentIdeal_integralClosureAt_eq_top

L156 ↗
AlgebraicCurves.Places.Proofs.PlaceExistsForgetConstants.S12CT.differentIdeal_integralClosureAt_eq_top
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsForgetConstants
noncomputable section
open IntermediateField AlgebraicCurve Polynomial
attribute [local instance 0] AlgebraicCurve.Place.valuationSubringAlgebra
namespace S12CT
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

L167 ↗
AlgebraicCurves.Places.Proofs.PlaceExistsForgetConstants.S12CT.ramificationIndex_eq_one_finiteLayer
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsForgetConstants
noncomputable section
open IntermediateField AlgebraicCurve Polynomial
attribute [local instance 0] AlgebraicCurve.Place.valuationSubringAlgebra
namespace S12CT
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

L205 ↗
AlgebraicCurves.Places.Proofs.PlaceExistsForgetConstants.S12CT.exists_finset_mem_adjoin
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsForgetConstants
noncomputable section
open IntermediateField AlgebraicCurve Polynomial
attribute [local instance 0] AlgebraicCurve.Place.valuationSubringAlgebra
namespace S12CT
section Square
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']
  [Algebra.IsAlgebraic K K']
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

isIntegral_gen

L237 ↗
AlgebraicCurves.Places.Proofs.PlaceExistsForgetConstants.S12CT.isIntegral_gen
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsForgetConstants
noncomputable section
open IntermediateField AlgebraicCurve Polynomial
attribute [local instance 0] AlgebraicCurve.Place.valuationSubringAlgebra
namespace S12CT
section LayerInSquare
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']
  [Algebra.IsAlgebraic K K'] [Algebra.IsIntegral F F']
omit [Algebra.IsIntegral F F'] in
Lean source · statement
theorem isIntegral_gen {b : F'} (hbint : IsIntegral K b) :
    IsIntegral K (IntermediateField.AdjoinSimple.gen F b)
theorem

minpoly_gen

L245 ↗
AlgebraicCurves.Places.Proofs.PlaceExistsForgetConstants.S12CT.minpoly_gen
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsForgetConstants
noncomputable section
open IntermediateField AlgebraicCurve Polynomial
attribute [local instance 0] AlgebraicCurve.Place.valuationSubringAlgebra
namespace S12CT
section LayerInSquare
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']
  [Algebra.IsAlgebraic K K'] [Algebra.IsIntegral F F']
omit [Algebra.IsIntegral F F'] in
Lean source · statement
theorem minpoly_gen {b : F'} :
    minpoly K (IntermediateField.AdjoinSimple.gen F b) = minpoly K b
theorem

adjoin_gen_eq_top

L253 ↗
AlgebraicCurves.Places.Proofs.PlaceExistsForgetConstants.S12CT.adjoin_gen_eq_top
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsForgetConstants
noncomputable section
open IntermediateField AlgebraicCurve Polynomial
attribute [local instance 0] AlgebraicCurve.Place.valuationSubringAlgebra
namespace S12CT
section LayerInSquare
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']
  [Algebra.IsAlgebraic K K'] [Algebra.IsIntegral F F']
omit [Algebra.IsIntegral F F'] in
Lean source · statement
theorem adjoin_gen_eq_top {b : F'} (hbint : IsIntegral K b) :
    Algebra.adjoin F ({IntermediateField.AdjoinSimple.gen F b} : Set F⟮b⟯) = ⊤
theorem

adjoin_finset_eq_adjoin_simple

L269 ↗
AlgebraicCurves.Places.Proofs.PlaceExistsForgetConstants.S12CT.adjoin_finset_eq_adjoin_simple
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsForgetConstants
noncomputable section
open IntermediateField AlgebraicCurve Polynomial
attribute [local instance 0] AlgebraicCurve.Place.valuationSubringAlgebra
namespace S12CT
section Main
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']
  [Algebra.IsAlgebraic K K'] [Algebra.IsSeparable K K'] [Algebra.IsIntegral F F']
omit [Algebra.IsAlgebraic K K'] [Algebra.IsSeparable K K'] in
Lean source · statement
theorem adjoin_finset_eq_adjoin_simple {S : Finset K'}
    {β : IntermediateField.adjoin K (S : Set K')} (hβ : K⟮β⟯ = ⊤) :
    IntermediateField.adjoin K (S : Set K') = K⟮(β : K')⟯
theorem

image_subset_adjoin

L290 ↗
AlgebraicCurves.Places.Proofs.PlaceExistsForgetConstants.S12CT.image_subset_adjoin
Source context 18 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsForgetConstants
noncomputable section
open IntermediateField AlgebraicCurve Polynomial
attribute [local instance 0] AlgebraicCurve.Place.valuationSubringAlgebra
namespace S12CT
section Main
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']
  [Algebra.IsAlgebraic K K'] [Algebra.IsSeparable K K'] [Algebra.IsIntegral F F']
omit [Algebra.IsIntegral F F'] [Algebra.IsSeparable K K'] in
omit [Algebra.IsSeparable K K'] in
omit [Algebra.IsIntegral F F'] in
omit [Algebra.IsSeparable K K'] in
omit [Algebra.IsIntegral F F'] in
omit [Algebra.IsSeparable K K'] in
omit [Algebra.IsIntegral F F'] in
omit [Algebra.IsSeparable K K'] in
omit [Algebra.IsIntegral F F'] in
omit [Algebra.IsSeparable K K'] in
Lean source · statement
theorem image_subset_adjoin {S : Finset K'}
    {β : IntermediateField.adjoin K (S : Set K')} (hβ : K⟮β⟯ = ⊤) :
    (algebraMap K' F') '' (S : Set K') ⊆ (F⟮algebraMap K' F' (β : K')⟯ : Set F')
theorem

adjoin_image_le

L314 ↗
AlgebraicCurves.Places.Proofs.PlaceExistsForgetConstants.S12CT.adjoin_image_le
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsForgetConstants
noncomputable section
open IntermediateField AlgebraicCurve Polynomial
attribute [local instance 0] AlgebraicCurve.Place.valuationSubringAlgebra
namespace S12CT
section Main
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']
  [Algebra.IsAlgebraic K K'] [Algebra.IsSeparable K K'] [Algebra.IsIntegral F F']
omit [Algebra.IsIntegral F F'] [Algebra.IsSeparable K K'] in
omit [Algebra.IsIntegral F F'] in
Lean source · statement
theorem adjoin_image_le {S : Finset K'}
    {β : IntermediateField.adjoin K (S : Set K')} (hβ : K⟮β⟯ = ⊤) :
    Algebra.adjoin F ((algebraMap K' F') '' (S : Set K'))
      ≤ F⟮algebraMap K' F' (β : K')⟯.toSubalgebra
theorem

mem_valuationSubring_of_monic

L329 ↗
AlgebraicCurves.Places.Proofs.PlaceExistsForgetConstants.S12CT.mem_valuationSubring_of_monic
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsForgetConstants
noncomputable section
open IntermediateField AlgebraicCurve Polynomial
attribute [local instance 0] AlgebraicCurve.Place.valuationSubringAlgebra
namespace S12CT
section Extension
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']
  [Algebra.IsAlgebraic K K'] [Algebra.IsSeparable K K'] [Algebra.IsIntegral F F']
Lean source · statement
theorem mem_valuationSubring_of_monic {R L : Type*} [CommRing R] [Field L] (O : ValuationSubring L)
    (φ : R →+* L) (hφ : ∀ r, φ r ∈ O) {x : L}
    (hx : ∃ p : Polynomial R, p.Monic ∧ p.eval₂ φ x = 0) : x ∈ O
theorem

inv_mem_of_isUnit

L340 ↗
AlgebraicCurves.Places.Proofs.PlaceExistsForgetConstants.S12CT.inv_mem_of_isUnit
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsForgetConstants
noncomputable section
open IntermediateField AlgebraicCurve Polynomial
attribute [local instance 0] AlgebraicCurve.Place.valuationSubringAlgebra
namespace S12CT
section Extension
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']
  [Algebra.IsAlgebraic K K'] [Algebra.IsSeparable K K'] [Algebra.IsIntegral F F']
Lean source · statement
theorem inv_mem_of_isUnit {L : Type*} [Field L] (O : ValuationSubring L) {z : L} (hz : z ∈ O)
    (h : IsUnit (⟨z, hz⟩ : O)) : z⁻¹ ∈ O
theorem

exists_forgetConstants_restrict_eq

L349 ↗
AlgebraicCurves.Places.Proofs.PlaceExistsForgetConstants.S12CT.exists_forgetConstants_restrict_eq
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsForgetConstants
noncomputable section
open IntermediateField AlgebraicCurve Polynomial
attribute [local instance 0] AlgebraicCurve.Place.valuationSubringAlgebra
namespace S12CT
section Extension
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']
  [Algebra.IsAlgebraic K K'] [Algebra.IsSeparable K K'] [Algebra.IsIntegral F F']
Lean source · statement
theorem exists_forgetConstants_restrict_eq
    (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
    (hconst : ∀ y : F, IsAlgebraic K y → y ∈ (algebraMap K F).range)
    {M : Type*} [Field M] [Algebra F M] [Algebra M F'] [IsScalarTower F M F']
    [Algebra K M] [IsScalarTower K M F'] [Algebra.IsIntegral M F']
    (V : Place K M) :
    ∃ W : Place K' F', (W.forgetConstants (K := K)).restrict M = V
theorem

exists_forgetConstants_restrict_eq_of_isConstantFieldExtension

L570 ↗
AlgebraicCurve.Place.exists_forgetConstants_restrict_eq_of_isConstantFieldExtension
Source context 2 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceExistsForgetConstants
Lean source · statement
theorem _root_.AlgebraicCurve.Place.exists_forgetConstants_restrict_eq_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)
    {M : Type*} [Field M] [Algebra F M] [Algebra M F'] [IsScalarTower F M F']
    [Algebra K M] [IsScalarTower K M F'] [Algebra.IsIntegral M F']
    (V : AlgebraicCurve.Place K M) :
    ∃ W : AlgebraicCurve.Place K' F', (W.forgetConstants (K := K)).restrict M = V

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