Module

KaehlerDifferential_span_D_eq_top_of_transcendental.lean

Nyll.AlgebraicCurves.Differentials.Kaehler.KaehlerDifferential_span_D_eq_top_of_transcendental

2 declarations indexed from sourceView source ↗

Module documentation

The differential of a transcendental coordinate spans the differential module.

Imports9

Mathlib.RingTheory.Etale.Kaehler
Mathlib.RingTheory.Etale.Field
Mathlib.RingTheory.Kaehler.Polynomial
Mathlib.FieldTheory.RatFunc.AsPolynomial
Mathlib.LinearAlgebra.TensorProduct.Basis
Mathlib.RingTheory.Kaehler.Basic
Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Mathlib.FieldTheory.Separable
Mathlib.RingTheory.Algebraic.Defs

Imported by10

theorem

exists_basis

L45 ↗

AlgebraicCurves.Differentials.Kaehler.Proofs.KaehlerDifferential_span_D_eq_top_of_transcendental.KaehlerDifferential.FF2.exists_basis

Source context 12 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs
namespace KaehlerDifferential_span_D_eq_top_of_transcendental
noncomputable section
open _root_.Polynomial
open _root_.KaehlerDifferential
namespace KaehlerDifferential
open _root_.KaehlerDifferential
namespace FF2
open _root_.KaehlerDifferential
variable {K F : Type*} [Field K] [Field F] [Algebra K F] {x : F} (hx : Transcendental K x)
  [Algebra.IsSeparable (IntermediateField.adjoin K ({x} : Set F)) F]
include hx in

Lean source · statement

theorem exists_basis : ∃ b : Module.Basis Unit F Ω[F⁄K], b () = D K F x

theorem

span_D_eq_top_of_transcendental

L87 ↗

KaehlerDifferential.span_D_eq_top_of_transcendental

Source context 6 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Kaehler.Proofs
namespace KaehlerDifferential_span_D_eq_top_of_transcendental
noncomputable section
open _root_.Polynomial
open _root_.KaehlerDifferential

Lean source · statement

theorem _root_.KaehlerDifferential.span_D_eq_top_of_transcendental (K : Type*) [Field K] {F :
    Type*} [Field F] [Algebra K F] (x : F) (hx : Transcendental K x)
    [Algebra.IsSeparable (IntermediateField.adjoin K ({x} : Set F)) F] :
    Submodule.span F ({KaehlerDifferential.D K F x} : Set (KaehlerDifferential K F)) = ⊤

Module documentation

Declarations

exists_basis

span_D_eq_top_of_transcendental