AlgebraicCurve.map_mem_polarDifferentials_and_mem_span_image_of_constantFieldExtension_of_isAlgClosed
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurve
open _root_.AlgebraicCurves.Differentials.Proofs in
open Map_mem_polarDifferentials_and_mem_span_image_of_constantFieldExtension_of_isAlgClosed in
open AlgebraicCurve inLean source · statement
theorem map_mem_polarDifferentials_and_mem_span_image_of_constantFieldExtension_of_isAlgClosed
(K F K' F' : Type*)
[Field K] [Field F] [Field K'] [Field F'] [Algebra K F] [Algebra K' F']
[Algebra K K'] [Algebra F F'] [Algebra K F'] [IsScalarTower K K' F'] [IsScalarTower K F F']
[SMulCommClass K' F F']
[IsAlgClosed K] [IsAlgClosed K'] [IsCurveOver K F] [IsCurveOver K' F']
[Algebra.EssFiniteType K F] [Algebra.EssFiniteType K' F']
(hfg : ∃ x : F, Transcendental K x ∧ FiniteDimensional (IntermediateField.adjoin K ({x} : Set
F)) F)
(hfg' : ∃ x : F', Transcendental K' x ∧
FiniteDimensional (IntermediateField.adjoin K' ({x} : Set F')) F')
(hgen : IntermediateField.adjoin K' (Set.range (algebraMap F F')) = ⊤)
(hdK : ∀ v : Place K F, v.DCoordGenerates) (hdK' : ∀ w : Place K' F', w.DCoordGenerates)
(S : Set (Place K F)) :
(∀ ω ∈ polarDifferentials K F S,
KaehlerDifferential.map K K' F F' ω ∈ polarDifferentials K' F'
{w : Place K' F' | ∃ v ∈ S, w.toValuationSubring.comap (algebraMap F F') =
v.toValuationSubring}) ∧
(∀ η ∈ polarDifferentials K' F'
{w : Place K' F' | ∃ v ∈ S, w.toValuationSubring.comap (algebraMap F F') =
v.toValuationSubring},
η ∈ Submodule.span K'
(KaehlerDifferential.map K K' F F' '' (polarDifferentials K F S : Set (Ω[F⁄K]))))