Module

FunctionField_finite_of_ratFuncAlgHom.lean

Nyll.AlgebraicCurves.FunctionFields.FunctionField_finite_of_ratFuncAlgHom

8 declarations indexed from sourceView source ↗

Module documentation

Function Field finite of rat Func Alg Hom

Imports39

Mathlib.Algebra.Algebra.Basic
Mathlib.Algebra.Algebra.Defs
Mathlib.Algebra.Algebra.Hom
Mathlib.Algebra.Algebra.Subalgebra.Lattice
Mathlib.Algebra.Algebra.Tower
Mathlib.Algebra.GroupWithZero.Units.Lemmas
Mathlib.Algebra.Polynomial.AlgebraMap
Mathlib.Algebra.Ring.Subsemiring.Basic
Mathlib.Basic.Finite.Defs
Mathlib.Combinatorics.Matroid.Basic
Mathlib.Data.Fin.VecNotation
Mathlib.Data.Set.Card
Mathlib.Data.Set.Finite.Basic
Mathlib.Data.Set.Image
Mathlib.Data.Set.Insert
Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Mathlib.FieldTheory.IntermediateField.Basic
Mathlib.FieldTheory.RatFunc.AsPolynomial
Mathlib.FieldTheory.RatFunc.Basic
Mathlib.FieldTheory.RatFunc.Defs
Mathlib.LinearAlgebra.FiniteDimensional.Defs
Mathlib.LinearAlgebra.Span.Defs
Mathlib.RingTheory.Adjoin.Polynomial.Basic
Mathlib.RingTheory.Algebraic.Basic
Mathlib.RingTheory.Algebraic.Defs
Mathlib.RingTheory.Algebraic.Integral
Mathlib.RingTheory.AlgebraicIndependent.Basic
Mathlib.RingTheory.AlgebraicIndependent.Defs
Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Mathlib.RingTheory.AlgebraicIndependent.Transcendental
Mathlib.RingTheory.Finiteness.Basic
Mathlib.RingTheory.Finiteness.Defs
Mathlib.RingTheory.Localization.FractionRing
Mathlib.RingTheory.Polynomial.Tower
Mathlib.RingTheory.SimpleRing.Basic
Mathlib.Tactic.Convert
Mathlib.Tactic.FinCases

Imported by3

theorem

isTranscendenceBasis_polynomial_X

L65 ↗

AlgebraicCurves.FunctionFields.Proofs.FunctionField_finite_of_ratFuncAlgHom.G1.isTranscendenceBasis_polynomial_X

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.FunctionField_finite_of_ratFuncAlgHom
open Polynomial
namespace G1

Lean source · statement

theorem isTranscendenceBasis_polynomial_X (K : Type*) [Field K] :
    IsTranscendenceBasis K ![(X : K[X])]

theorem

isTranscendenceBasis_ratFunc_X

L74 ↗

AlgebraicCurves.FunctionFields.Proofs.FunctionField_finite_of_ratFuncAlgHom.G1.isTranscendenceBasis_ratFunc_X

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.FunctionField_finite_of_ratFuncAlgHom
open Polynomial
namespace G1

Lean source · statement

theorem isTranscendenceBasis_ratFunc_X (K : Type*) [Field K] :
    IsTranscendenceBasis K ![(RatFunc.X : RatFunc K)]

theorem

isTranscendenceBasis_t0

L90 ↗

AlgebraicCurves.FunctionFields.Proofs.FunctionField_finite_of_ratFuncAlgHom.G1.isTranscendenceBasis_t0

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.FunctionField_finite_of_ratFuncAlgHom
open Polynomial
namespace G1
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
  [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F]

Lean source · statement

theorem isTranscendenceBasis_t0 :
    IsTranscendenceBasis K ![algebraMap (RatFunc K) F RatFunc.X]

theorem

transcendental_apply_X

L100 ↗

AlgebraicCurves.FunctionFields.Proofs.FunctionField_finite_of_ratFuncAlgHom.G1.transcendental_apply_X

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.FunctionField_finite_of_ratFuncAlgHom
open Polynomial
namespace G1
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
  [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F]
omit [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F]
    [FiniteDimensional (RatFunc K) F] in

Lean source · statement

theorem transcendental_apply_X (φ : RatFunc K →ₐ[K] F) : Transcendental K (φ RatFunc.X)

theorem

isTranscendenceBasis_apply_X

L109 ↗

AlgebraicCurves.FunctionFields.Proofs.FunctionField_finite_of_ratFuncAlgHom.G1.isTranscendenceBasis_apply_X

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.FunctionField_finite_of_ratFuncAlgHom
open Polynomial
namespace G1
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
  [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F]

Lean source · statement

theorem isTranscendenceBasis_apply_X (φ : RatFunc K →ₐ[K] F) :
    IsTranscendenceBasis K (Subtype.val : ({φ RatFunc.X} : Set F) → F)

theorem

algebraMap_polynomial_mem

L133 ↗

AlgebraicCurves.FunctionFields.Proofs.FunctionField_finite_of_ratFuncAlgHom.G1.algebraMap_polynomial_mem

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.FunctionField_finite_of_ratFuncAlgHom
open Polynomial
namespace G1
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
  [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F]
omit [FiniteDimensional (RatFunc K) F] in

Lean source · statement

theorem algebraMap_polynomial_mem {E : Type*} [Field E] [Algebra K E] [Algebra E F] [IsScalarTower
  K E F]
    (T : IntermediateField E F) (ht : algebraMap (RatFunc K) F RatFunc.X ∈ T) (p : K[X]) :
    algebraMap (RatFunc K) F (algebraMap K[X] (RatFunc K) p) ∈ T

theorem

finite_over_adjoin

L145 ↗

AlgebraicCurves.FunctionFields.Proofs.FunctionField_finite_of_ratFuncAlgHom.G1.finite_over_adjoin

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.FunctionField_finite_of_ratFuncAlgHom
open Polynomial
namespace G1
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
  [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional (RatFunc K) F]

Lean source · statement

theorem finite_over_adjoin (φ : RatFunc K →ₐ[K] F) :
    FiniteDimensional (IntermediateField.adjoin K ({φ RatFunc.X} : Set F)) F

theorem

finite_of_ratFuncAlgHom

L185 ↗

AlgebraicCurve.FunctionField.finite_of_ratFuncAlgHom

Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.FunctionFields.Proofs.FunctionField_finite_of_ratFuncAlgHom
open Polynomial
open G1 in

Lean source · statement

theorem _root_.AlgebraicCurve.FunctionField.finite_of_ratFuncAlgHom {K F : Type*} [Field K] [Field
  F] [Algebra K F] [Algebra (RatFunc K) F] [IsScalarTower K (RatFunc K) F] [FiniteDimensional
  (RatFunc K) F] (φ : RatFunc K →ₐ[K] F) : @Module.Finite (RatFunc K) F _ _
  (φ.toRingHom.toAlgebra).toModule

Module documentation

Function Field finite of rat Func Alg Hom

Declarations