AlgebraicCurve.Pic0.range_eq_setOf_cartier_fixed_and_isRegularDiff
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace JacobianVarieties.Pic0.Proofs.Pic0_range_eq_setOf_cartier_fixed_and_isRegularDiff
attribute [-instance]
AlgebraicCurve.Place.instIsPrimeCenter AlgebraicCurve.Place.instIsFractionRingIntegralClosureAt
attribute [-instance]
instIsTorsionFreeSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
attribute [-instance]
AlgebraicCurve.Place.instIsDedekindDomainIntegralClosureAt
AlgebraicCurve.Place.instFiniteSubtypeMemValuationSubringToValuationSubringIntegralClosureAt
AlgebraicCurve.instFundamentalIdentityOfSumRamificationInertia
AlgebraicCurve.Place.instIsScalarTowerResidueFieldRestrictPushforward
AlgebraicCurve.Place.instAlgebraResidueFieldRestrictPushforward
AlgebraicCurve.Place.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
universe u v
open KaehlerDifferential AlgebraicCurveLean source · statement
theorem _root_.AlgebraicCurve.Pic0.range_eq_setOf_cartier_fixed_and_isRegularDiff
{K : Type u} {F : Type v} [Field K] [Field F] [Algebra K F]
[AlgebraicCurve.IsCurveOver K F]
(p : ℕ) [Fact p.Prime] [CharP K p] [PerfectField K]
(x : F) [FiniteDimensional (IntermediateField.adjoin K ({x} : Set F)) F]
(C : Ω[F⁄K] →+ Ω[F⁄K])
(hsemi : ∀ (f : F) (ω : Ω[F⁄K]), C (f ^ p • ω) = f • C ω)
(hker : ∀ f : F, C (D K F f) = 0)
(hlog : ∀ f : F, C (f ^ (p - 1) • D K F f) = D K F f)
(δ : Pic0.torsion K F p →+ Ω[F⁄K])
(hδ : ∀ (y : Pic0.torsion K F p) (E : Divisor.degZero (K := K) (F := F)) (g : F),
Pic0.mk E = (y : Pic0 K F) → g ≠ 0 →
(∀ v : Place K F, (p : ℤ) * (E : Divisor K F) v = v.ord g) →
δ y = g⁻¹ • D K F g) :
Set.range δ = {ω : Ω[F⁄K] | C ω = ω ∧ AlgebraicCurve.IsRegularDiff K F ω}