AlgebraicCurve.exists_mem_smul_D_of_map_mem_regularDifferentials_of_constantFieldExtension
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Differentials.Proofs
namespace Exists_mem_smul_D_of_map_mem_regularDifferentials_of_constantFieldExtension
attribute [-instance]
instIsPrimeCenter
instIsFractionRingIntegralClosureAt
instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
instIsDedekindDomainIntegralClosureAt
instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
instIsScalarTowerResidueFieldRestrictPushforward
instAlgebraResidueFieldRestrictPushforward
instIsLocalHomRestrictInclusion
attribute [-simp] AlgebraicCurve.Place.placeOfPrime_toValuationSubring
AlgebraicCurve.Place.mem_fiberOver AlgebraicCurve.Place.fiberEquiv_symm_apply
AlgebraicCurve.Place.fiberEquiv_apply AlgebraicCurve.Place.centerHeightOneSpectrum_asIdeal
AlgebraicCurve.Divisor.mapRestrict_single AlgebraicCurve.Divisor.pushforward_single
AlgebraicCurve.Place.coe_restrictInclusion AlgebraicCurve.Place.mem_fiber
AlgebraicCurve.Place.restrict_toValuationSubring AlgebraicCurve.Divisor.degree_pushforward
AlgebraicCurve.Place.restrictResidueMap_residue AlgebraicCurve.Pic0.coe_pushforwardDegZeroHom
AlgebraicCurve.Pic0.coe_pullbackDegZeroHom
attribute [-simp] AlgebraicCurve.Pic.baseChange_mk
AlgebraicCurve.Place.forgetConstants_toValuationSubring
AlgebraicCurve.Place.constantFieldEquiv_symm_apply AlgebraicCurve.Place.ord_forgetConstants
AlgebraicCurve.Place.extendConstants_toValuationSubring
AlgebraicCurve.Place.constantFieldEquiv_apply_toValuationSubring
AlgebraicCurve.Place.mem_fiberConstants AlgebraicCurve.Place.restrictConstants_toValuationSubring
open KaehlerDifferential AlgebraicCurveLean source · statement
theorem
_root_.AlgebraicCurve.exists_mem_smul_D_of_map_mem_regularDifferentials_of_constantFieldExtension
(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']
[CharZero K] [Algebra.IsAlgebraic K K'] [IsAlgClosed K'] [Algebra.IsIntegral F F']
(hfg : ∃ x : F, Transcendental K x ∧ FiniteDimensional (IntermediateField.adjoin K ({x} : Set
F)) F)
[AlgebraicCurve.IsCurveOver K' F']
(hfg' : ∃ x : F', Transcendental K' x ∧ FiniteDimensional (IntermediateField.adjoin K' ({x} :
Set F')) F')
(hgen : Algebra.adjoin F (Set.range (algebraMap K' F')) = ⊤)
(ω : Ω[F⁄K]) (hω : KaehlerDifferential.map K K' F F' ω ∈ AlgebraicCurve.regularDifferentials K'
F')
(v : AlgebraicCurve.Place K F) :
∃ c ∈ v.toValuationSubring, ∃ t ∈ v.toValuationSubring, ω = c • KaehlerDifferential.D K F t