NYLL
Module

Place_residueField_eq_compositum_of_isConstantFieldExtension.lean

Nyll.AlgebraicCurves.Places.Place_residueField_eq_compositum_of_isConstantFieldExtension
15 declarations indexed from sourceView source ↗

Module documentation

Place residue Field eq compositum of is Constant Field Extension

Imports7
Imported by2

Declarations

theorem

mem_of_isIntegral

L44 ↗
AlgebraicCurves.Places.Proofs.PlaceResidueFieldCompositum.AlgebraicCurve.Place.ResidueCompositumAux.mem_of_isIntegral
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceResidueFieldCompositum
open _root_.AlgebraicCurve
open _root_.IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ResidueCompositumAux
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Constants
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem mem_of_isIntegral (w : Place K F) {y : F} (hy : IsIntegral K y) : y ∈ w.toValuationSubring
theorem

isUnit_of_isIntegral

L51 ↗
AlgebraicCurves.Places.Proofs.PlaceResidueFieldCompositum.AlgebraicCurve.Place.ResidueCompositumAux.isUnit_of_isIntegral
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceResidueFieldCompositum
open _root_.AlgebraicCurve
open _root_.IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ResidueCompositumAux
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Constants
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
Lean source · statement
theorem isUnit_of_isIntegral (w : Place K F) {y : F} (hy : IsIntegral K y) (hy0 : y ≠ 0) :
    IsUnit (⟨y, mem_of_isIntegral w hy⟩ : w.toValuationSubring)
theorem

mem_adjoin_of_isIntegral_valuationSubring

L66 ↗
AlgebraicCurves.Places.Proofs.PlaceResidueFieldCompositum.AlgebraicCurve.Place.ResidueCompositumAux.mem_adjoin_of_isIntegral_valuationSubring
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceResidueFieldCompositum
open _root_.AlgebraicCurve
open _root_.IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ResidueCompositumAux
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Layer
variable {K F F₁ : Type*} [Field K] [Field F] [Field F₁]
  [Algebra K F] [Algebra K F₁] [Algebra F F₁] [IsScalarTower K F F₁]
  [FiniteDimensional F F₁] [Algebra.IsSeparable F F₁]
Lean source · statement
theorem mem_adjoin_of_isIntegral_valuationSubring (v : Place K F) {α : F₁} (hαK : IsIntegral K α)
    (hgen : IntermediateField.adjoin F ({α} : Set F₁) = ⊤) {z : F₁}
    (hz : IsIntegral v.toValuationSubring z) :
    z ∈ Algebra.adjoin v.toValuationSubring ({α} : Set F₁)
theorem

algebraMap_mem_adjoin_of_mem_adjoin

L139 ↗
AlgebraicCurves.Places.Proofs.PlaceResidueFieldCompositum.AlgebraicCurve.Place.ResidueCompositumAux.algebraMap_mem_adjoin_of_mem_adjoin
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceResidueFieldCompositum
open _root_.AlgebraicCurve
open _root_.IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ResidueCompositumAux
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section LayerThrough
Lean source · statement
theorem algebraMap_mem_adjoin_of_mem_adjoin {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'] {α s : K'}
    (hs : s ∈ Algebra.adjoin K ({α} : Set K')) :
    algebraMap K' F' s ∈ IntermediateField.adjoin F ({algebraMap K' F' α} : Set F')
theorem

isIntegral_algebraMap_of_isIntegral

L156 ↗
AlgebraicCurves.Places.Proofs.PlaceResidueFieldCompositum.AlgebraicCurve.Place.ResidueCompositumAux.isIntegral_algebraMap_of_isIntegral
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceResidueFieldCompositum
open _root_.AlgebraicCurve
open _root_.IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ResidueCompositumAux
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section LayerThrough
Lean source · statement
theorem isIntegral_algebraMap_of_isIntegral {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'] {α : K'} (hα : IsIntegral K α) :
    IsIntegral F (algebraMap K' F' α)
theorem

isSeparable_algebraMap_of_isSeparable

L164 ↗
AlgebraicCurves.Places.Proofs.PlaceResidueFieldCompositum.AlgebraicCurve.Place.ResidueCompositumAux.isSeparable_algebraMap_of_isSeparable
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceResidueFieldCompositum
open _root_.AlgebraicCurve
open _root_.IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ResidueCompositumAux
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section LayerThrough
Lean source · statement
theorem isSeparable_algebraMap_of_isSeparable {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'] {α : K'} (hα : IsSeparable K α) :
    IsSeparable F (algebraMap K' F' α)
theorem

exists_layer

L173 ↗
AlgebraicCurves.Places.Proofs.PlaceResidueFieldCompositum.AlgebraicCurve.Place.ResidueCompositumAux.exists_layer
Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceResidueFieldCompositum
open _root_.AlgebraicCurve
open _root_.IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ResidueCompositumAux
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section LayerThrough
Lean source · statement
theorem exists_layer {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']
    (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤) (x : F') :
    ∃ α : K', x ∈ IntermediateField.adjoin F ({algebraMap K' F' α} : Set F')
theorem

adjoin_gen_eq_top

L221 ↗
AlgebraicCurves.Places.Proofs.PlaceResidueFieldCompositum.AlgebraicCurve.Place.ResidueCompositumAux.adjoin_gen_eq_top
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceResidueFieldCompositum
open _root_.AlgebraicCurve
open _root_.IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ResidueCompositumAux
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Inside
variable {F F' : Type*} [Field F] [Field F'] [Algebra F F']
Lean source · statement
theorem adjoin_gen_eq_top (a : F') :
    IntermediateField.adjoin F
        ({(⟨a, IntermediateField.mem_adjoin_simple_self F a⟩ : IntermediateField.adjoin F ({a} :
          Set F'))} :
          Set (IntermediateField.adjoin F ({a} : Set F'))) = ⊤
theorem

finiteDimensional_adjoin_simple_of_isIntegral

L229 ↗
AlgebraicCurves.Places.Proofs.PlaceResidueFieldCompositum.AlgebraicCurve.Place.ResidueCompositumAux.finiteDimensional_adjoin_simple_of_isIntegral
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceResidueFieldCompositum
open _root_.AlgebraicCurve
open _root_.IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ResidueCompositumAux
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Inside
variable {F F' : Type*} [Field F] [Field F'] [Algebra F F']
Lean source · statement
theorem finiteDimensional_adjoin_simple_of_isIntegral {a : F'} (ha : IsIntegral F a) :
    FiniteDimensional F (IntermediateField.adjoin F ({a} : Set F'))
theorem

isSeparable_adjoin_simple

L233 ↗
AlgebraicCurves.Places.Proofs.PlaceResidueFieldCompositum.AlgebraicCurve.Place.ResidueCompositumAux.isSeparable_adjoin_simple
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceResidueFieldCompositum
open _root_.AlgebraicCurve
open _root_.IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ResidueCompositumAux
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Inside
variable {F F' : Type*} [Field F] [Field F'] [Algebra F F']
Lean source · statement
theorem isSeparable_adjoin_simple {a : F'} (ha : IsSeparable F a) :
    Algebra.IsSeparable F (IntermediateField.adjoin F ({a} : Set F'))
theorem

isIntegral_gen_of_isIntegral

L237 ↗
AlgebraicCurves.Places.Proofs.PlaceResidueFieldCompositum.AlgebraicCurve.Place.ResidueCompositumAux.isIntegral_gen_of_isIntegral
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceResidueFieldCompositum
open _root_.AlgebraicCurve
open _root_.IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ResidueCompositumAux
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Inside
variable {F F' : Type*} [Field F] [Field F'] [Algebra F F']
Lean source · statement
theorem isIntegral_gen_of_isIntegral {K : Type*} [Field K] [Algebra K F] [Algebra K F']
  [IsScalarTower K F F']
    {a : F'} (ha : IsIntegral K a) :
    IsIntegral K (⟨a, IntermediateField.mem_adjoin_simple_self F a⟩ : IntermediateField.adjoin F
      ({a} : Set F'))
theorem

residue_mem_adjoin_of_mem_adjoin

L263 ↗
AlgebraicCurves.Places.Proofs.PlaceResidueFieldCompositum.AlgebraicCurve.Place.ResidueCompositumAux.residue_mem_adjoin_of_mem_adjoin
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceResidueFieldCompositum
open _root_.AlgebraicCurve
open _root_.IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ResidueCompositumAux
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section ResidueChase
open IsLocalRing
Lean source · statement
theorem residue_mem_adjoin_of_mem_adjoin {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.IsIntegral K K']
      [Algebra.IsIntegral F F']
    (W : Place K' F') (F₁ : IntermediateField F F') (α : K') (hα : algebraMap K' F' α ∈ F₁)
    (z : F₁)
    (hz : z ∈ Algebra.adjoin ((W.forgetConstants (K := K)).restrict F).toValuationSubring
      ({⟨algebraMap K' F' α, hα⟩} : Set F₁)) :
    ∃ hzO : ((z : F₁) : F') ∈ W.toValuationSubring,
      IsLocalRing.residue W.toValuationSubring ⟨(z : F'), hzO⟩ ∈
        IntermediateField.adjoin K' (E := W.ResidueField)
          (Set.range ((W.forgetConstants (K := K)).restrictResidueMap (F := F)))
theorem

restrict_restrict

L326 ↗
AlgebraicCurves.Places.Proofs.PlaceResidueFieldCompositum.AlgebraicCurve.Place.ResidueCompositumAux.restrict_restrict
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceResidueFieldCompositum
open _root_.AlgebraicCurve
open _root_.IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ResidueCompositumAux
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
section Tower
variable {K F F₁ F' : Type*} [Field K] [Field F] [Field F₁] [Field F']
  [Algebra K F] [Algebra K F₁] [Algebra K F'] [Algebra F F₁] [Algebra F₁ F'] [Algebra F F']
  [IsScalarTower F F₁ F'] [IsScalarTower K F F'] [IsScalarTower K F₁ F'] [IsScalarTower K F F₁]
  [Algebra.IsIntegral F F'] [Algebra.IsIntegral F₁ F'] [Algebra.IsIntegral F F₁]
Lean source · statement
theorem restrict_restrict (w : Place K F') : (w.restrict F₁).restrict F = w.restrict F
theorem

main

L341 ↗
AlgebraicCurves.Places.Proofs.PlaceResidueFieldCompositum.AlgebraicCurve.Place.ResidueCompositumAux.main
Source context 13 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceResidueFieldCompositum
open _root_.AlgebraicCurve
open _root_.IntermediateField
namespace AlgebraicCurve
open _root_.AlgebraicCurve
namespace Place
open _root_.AlgebraicCurve.Place
namespace ResidueCompositumAux
open _root_.AlgebraicCurve.Place
open _root_.AlgebraicCurve
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']
Lean source · statement
theorem main (hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤) (W : Place K' F') :
    IntermediateField.adjoin K' (E := W.ResidueField)
        (Set.range ((W.forgetConstants (K := K)).restrictResidueMap (F := F))) = ⊤
theorem

residueField_eq_compositum_of_isConstantFieldExtension

L427 ↗
AlgebraicCurve.Place.residueField_eq_compositum_of_isConstantFieldExtension
Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Places.Proofs.PlaceResidueFieldCompositum
open _root_.AlgebraicCurve
open _root_.IntermediateField
open _root_.AlgebraicCurve
  _root_.AlgebraicCurves.Places.Proofs.PlaceResidueFieldCompositum.AlgebraicCurve in
Lean source · statement
theorem _root_.AlgebraicCurve.Place.residueField_eq_compositum_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')) = ⊤)
    (W : Place K' F') :
    IntermediateField.adjoin K' (E := W.ResidueField)
        (Set.range ((W.forgetConstants (K := K)).restrictResidueMap (F := F))) = ⊤

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