NYLL
Module

CurveModel_nonempty_of_perfectField.lean

Nyll.AlgebraicCurves.Models.CurveModel_nonempty_of_perfectField
10 declarations indexed from sourceView source ↗

Module documentation

Curve Model nonempty of perfect Field

Imports5
Imported by6

Declarations

theorem

nonempty_of_separatingGenerator

L36 ↗
AlgebraicCurves.Models.Proofs.CurveModel_nonempty_of_perfectField.P2mModelK.nonempty_of_separatingGenerator
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_nonempty_of_perfectField
universe u v w
noncomputable section
open CategoryTheory AlgebraicGeometry IntermediateField AlgebraicCurve
namespace P2mModelK
Lean source · statement
theorem nonempty_of_separatingGenerator (K : Type u) [Field K] [PerfectField K] [Infinite K]
    {L : Type u} [Field L] [Algebra K L] (t : L) [Fact (t ≠ 0)] (ht : Transcendental K t)
    [FiniteDimensional K⟮t⟯ L] [Algebra.IsSeparable K⟮t⟯ L] : Nonempty (CurveModel K L)
theorem

essFiniteType_of_hfg

L56 ↗
AlgebraicCurves.Models.Proofs.CurveModel_nonempty_of_perfectField.P2mModelK.essFiniteType_of_hfg
Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_nonempty_of_perfectField
universe u v w
noncomputable section
open CategoryTheory AlgebraicGeometry IntermediateField AlgebraicCurve
namespace P2mModelK
section Separating
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
theorem essFiniteType_of_hfg
    (hfg : ∃ x : L, Transcendental K x ∧ FiniteDimensional K⟮x⟯ L) : Algebra.EssFiniteType K L
theorem

isTranscendenceBasis_of_hfg

L65 ↗
AlgebraicCurves.Models.Proofs.CurveModel_nonempty_of_perfectField.P2mModelK.isTranscendenceBasis_of_hfg
Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_nonempty_of_perfectField
universe u v w
noncomputable section
open CategoryTheory AlgebraicGeometry IntermediateField AlgebraicCurve
namespace P2mModelK
section Separating
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
open scoped _root_.IntermediateField.algebraAdjoinAdjoin in
Lean source · statement
theorem isTranscendenceBasis_of_hfg {x : L} (hx : Transcendental K x) [FiniteDimensional K⟮x⟯ L] :
    IsTranscendenceBasis K ![x]
theorem

nonempty_same_universe

L77 ↗
AlgebraicCurves.Models.Proofs.CurveModel_nonempty_of_perfectField.P2mModelK.nonempty_same_universe
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_nonempty_of_perfectField
universe u v w
noncomputable section
open CategoryTheory AlgebraicGeometry IntermediateField AlgebraicCurve
namespace P2mModelK
Lean source · statement
theorem nonempty_same_universe (K : Type u) [Field K] [PerfectField K] [Infinite K]
    (L : Type u) [Field L] [Algebra K L]
    (hfg : ∃ x : L, Transcendental K x ∧ FiniteDimensional K⟮x⟯ L) : Nonempty (CurveModel K L)
def

congr

L107 ↗
AlgebraicCurves.Models.Proofs.CurveModel_nonempty_of_perfectField.P2mModelK.congr
Documentation

Transport of a curve model along an algebra equivalence of its function field.

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_nonempty_of_perfectField
universe u v w
noncomputable section
open CategoryTheory AlgebraicGeometry IntermediateField AlgebraicCurve
namespace P2mModelK
Lean source · full declaration
def congr {K : Type u} [Field K] {L : Type v} {L' : Type w} [Field L] [Field L'] [Algebra K L]
    [Algebra K L'] (e : L' ≃ₐ[K] L) (M : CurveModel K L') : CurveModel K L where
  C := M.C
  toBase := M.toBase
  ffEquiv := e.symm.toRingEquiv.trans M.ffEquiv
  ffEquiv_algebraMap a := by
    change M.ffEquiv (e.symm (algebraMap K L a)) = _
    rw [e.symm.commutes]
    exact M.ffEquiv_algebraMap a
  placeOfPoint x := Place.congrEquiv e.toRingEquiv (fun a => e.commutes a) (M.placeOfPoint x)
  placeOfPoint_bijective :=
    (Place.congrEquiv e.toRingEquiv (fun a => e.commutes a)).bijective.comp M.placeOfPoint_bijective
  range_stalk_eq x := by
    have hM := M.range_stalk_eq x
    have hcomp : ((e.symm.toRingEquiv.trans M.ffEquiv).symm : M.C.functionField ≃+*
      L).toRingHom.comp
          (algebraMap (M.C.presheaf.stalk x.1) M.C.functionField) =
        (e.toRingEquiv : L' →+* L).comp
          ((M.ffEquiv.symm : M.C.functionField ≃+* L').toRingHom.comp
            (algebraMap (M.C.presheaf.stalk x.1) M.C.functionField)) := by
      ext y
      rfl
    rw [hcomp, ← RingHom.map_range, hM, Subring.map_equiv_eq_comap_symm]
    rfl
  finset_subset_affineOpen := M.finset_subset_affineOpen
theorem

small_of_hfg

L133 ↗
AlgebraicCurves.Models.Proofs.CurveModel_nonempty_of_perfectField.P2mModelK.small_of_hfg
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_nonempty_of_perfectField
universe u v w
noncomputable section
open CategoryTheory AlgebraicGeometry IntermediateField AlgebraicCurve
namespace P2mModelK
Lean source · statement
theorem small_of_hfg {K : Type u} [Field K] {L : Type v} [Field L] [Algebra K L]
    (hfg : ∃ x : L, Transcendental K x ∧ FiniteDimensional K⟮x⟯ L) : Small.{u} L
theorem

transcendental_algEquiv

L141 ↗
AlgebraicCurves.Models.Proofs.CurveModel_nonempty_of_perfectField.P2mModelK.transcendental_algEquiv
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_nonempty_of_perfectField
universe u v w
noncomputable section
open CategoryTheory AlgebraicGeometry IntermediateField AlgebraicCurve
namespace P2mModelK
Lean source · statement
theorem transcendental_algEquiv {K : Type u} [Field K] {L : Type v} {L' : Type w} [Field L] [Field
  L']
    [Algebra K L] [Algebra K L'] (e : L' ≃ₐ[K] L) {x : L} (hx : Transcendental K x) :
    Transcendental K (e.symm x)
theorem

finiteDimensional_algEquiv

L153 ↗
AlgebraicCurves.Models.Proofs.CurveModel_nonempty_of_perfectField.P2mModelK.finiteDimensional_algEquiv
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_nonempty_of_perfectField
universe u v w
noncomputable section
open CategoryTheory AlgebraicGeometry IntermediateField AlgebraicCurve
namespace P2mModelK
Lean source · statement
theorem finiteDimensional_algEquiv {K : Type u} [Field K] {L : Type v} {L' : Type w} [Field L]
  [Field L']
    [Algebra K L] [Algebra K L'] (e : L' ≃ₐ[K] L) (x : L) [FiniteDimensional K⟮x⟯ L] :
    FiniteDimensional K⟮e.symm x⟯ L'
theorem

main

L164 ↗
AlgebraicCurves.Models.Proofs.CurveModel_nonempty_of_perfectField.P2mModelK.main
Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_nonempty_of_perfectField
universe u v w
noncomputable section
open CategoryTheory AlgebraicGeometry IntermediateField AlgebraicCurve
namespace P2mModelK
Lean source · statement
theorem main (K : Type u) (L : Type v) [Field K] [PerfectField K] [Infinite K] [Field L] [Algebra K
  L]
    (hfg : ∃ x : L, Transcendental K x ∧ FiniteDimensional K⟮x⟯ L) :
    Nonempty (CurveModel K L)
theorem

nonempty_of_perfectField

L182 ↗
AlgebraicCurve.CurveModel.nonempty_of_perfectField
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Models.Proofs.CurveModel_nonempty_of_perfectField
universe u v w
open AlgebraicCurve
Lean source · statement
theorem _root_.AlgebraicCurve.CurveModel.nonempty_of_perfectField
    (K : Type u) (L : Type v) [Field K] [PerfectField K] [Infinite K] [Field L] [Algebra K L]
    (hfg : ∃ x : L, Transcendental K x ∧ FiniteDimensional (IntermediateField.adjoin K ({x} : Set
      L)) L) :
    Nonempty (CurveModel K L)

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