Module

KaehlerDifferential_map_injective_of_constantFieldExtension.lean

Nyll.AlgebraicCurves.Differentials.KaehlerDifferential_map_injective_of_constantFieldExtension

3 declarations indexed from sourceView source ↗

Module documentation

Kaehler Differential map injective of constant Field Extension

Imports1

Nyll.AlgebraicCurves.FunctionFields.CurveOver

Imported by1

Nyll.AlgebraicCurves.Differentials.All

def

kerField

L29 ↗

AlgebraicCurves.Differentials.Proofs.KaehlerDifferential_map_injective_of_constantFieldExtension.KInjSol.kerField

Documentation

The intermediate field of elements annihilated by the specified derivation.

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs
namespace KaehlerDifferential_map_injective_of_constantFieldExtension
open AlgebraicCurve KaehlerDifferential
namespace KInjSol

Lean source · full declaration

def kerField {E FE : Type*} [Field E] [Field FE] [Algebra E FE]
    (d : Derivation E FE Ω[FE⁄E]) : IntermediateField E FE where
  carrier := {z | d z = 0}
  mul_mem' {a b} ha hb := by
    simp only [Set.mem_ofPred_eq] at ha hb ⊢
    rw [Derivation.leibniz, ha, hb, smul_zero, smul_zero, add_zero]
  one_mem' := by simp only [Set.mem_ofPred_eq]; exact Derivation.map_one_eq_zero _
  add_mem' {a b} ha hb := by
    simp only [Set.mem_ofPred_eq] at ha hb ⊢
    rw [map_add, ha, hb, add_zero]
  zero_mem' := by simp only [Set.mem_ofPred_eq]; exact map_zero _
  algebraMap_mem' r := by simp only [Set.mem_ofPred_eq]; exact Derivation.map_algebraMap _ _
  inv_mem' a ha := by
    simp only [Set.mem_ofPred_eq] at ha ⊢
    rw [Derivation.leibniz_inv, ha, smul_zero]

theorem

mem_kerField

L45 ↗

AlgebraicCurves.Differentials.Proofs.KaehlerDifferential_map_injective_of_constantFieldExtension.KInjSol.mem_kerField

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs
namespace KaehlerDifferential_map_injective_of_constantFieldExtension
open AlgebraicCurve KaehlerDifferential
namespace KInjSol

Lean source · statement

theorem mem_kerField {E FE : Type*} [Field E] [Field FE] [Algebra E FE]
    (d : Derivation E FE Ω[FE⁄E]) (z : FE) : z ∈ kerField d ↔ d z = 0

theorem

kaehlerDifferential_map_injective_of_constantFieldExtension

L51 ↗

AlgebraicCurve.kaehlerDifferential_map_injective_of_constantFieldExtension

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs
namespace KaehlerDifferential_map_injective_of_constantFieldExtension
open AlgebraicCurve KaehlerDifferential
open KInjSol in

Lean source · statement

theorem _root_.AlgebraicCurve.kaehlerDifferential_map_injective_of_constantFieldExtension
    {K F E FE : Type*} [Field K] [Field F] [Field E] [Field FE]
    [Algebra K F] [Algebra K E] [Algebra E FE] [Algebra F FE] [Algebra K FE]
    [IsScalarTower K E FE] [IsScalarTower K F FE]
    [PerfectField K] [AlgebraicCurve.IsCurveOver K F] [AlgebraicCurve.IsCurveOver E FE]
    (hgen : IntermediateField.adjoin E (Set.range (algebraMap F FE)) = ⊤) :
    Function.Injective (KaehlerDifferential.map K E F FE)

Module documentation

Kaehler Differential map injective of constant Field Extension

Declarations

kerField

mem_kerField

kaehlerDifferential_map_injective_of_constantFieldExtension