Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)def unifLDR : FSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)theorem unifLDR_mem : v.unifLDR ∈ v.toValuationSubringSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)theorem dCoord_eq_D_unifLDR : v.dCoord = D K F v.unifLDRThe differential coefficient becomes integral after multiplication by a uniformizer power.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)def HasPoleOrderLE (n : ℕ) (ω : Ω[F⁄K]) : PropThe function becomes integral after multiplication by a uniformizer power.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)def FnPoleOrderLE (n : ℕ) (g : F) : PropThe uniformizer times the differential coefficient has the specified residue.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)def HasLogResidue (ω : Ω[F⁄K]) (a : K) : PropSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)
variable {v}
variable (v) intheorem hasPoleOrderLE_zero_right (n : ℕ) : v.HasPoleOrderLE n (0 : Ω[F⁄K])Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)
variable {v}
variable (v) intheorem HasPoleOrderLE.add {n : ℕ} {ω η : Ω[F⁄K]} (hω : v.HasPoleOrderLE n ω)
(hη : v.HasPoleOrderLE n η) : v.HasPoleOrderLE n (ω + η)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)
variable {v}
variable (v) intheorem HasPoleOrderLE.neg {n : ℕ} {ω : Ω[F⁄K]} (hω : v.HasPoleOrderLE n ω) :
v.HasPoleOrderLE n (-ω)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)
variable {v}
variable (v) intheorem HasPoleOrderLE.sub {n : ℕ} {ω η : Ω[F⁄K]} (hω : v.HasPoleOrderLE n ω)
(hη : v.HasPoleOrderLE n η) : v.HasPoleOrderLE n (ω - η)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)
variable {v}
variable (v) intheorem HasPoleOrderLE.smul {n : ℕ} (c : K) {ω : Ω[F⁄K]} (hω : v.HasPoleOrderLE n ω) :
v.HasPoleOrderLE n (c • ω)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)
variable {v}
variable (v) intheorem HasPoleOrderLE.of_le {m n : ℕ} (h : m ≤ n) {ω : Ω[F⁄K]} (hω : v.HasPoleOrderLE m ω) :
v.HasPoleOrderLE n ωSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)
variable {v}
variable (v) intheorem hasPoleOrderLE_zero_of_mem {f : F} (hf : f ∈ v.toValuationSubring) :
v.HasPoleOrderLE 0 (f • v.dCoord)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)
variable {v}
variable (v) intheorem FnPoleOrderLE.add {n : ℕ} {g h : F} (hg : v.FnPoleOrderLE n g) (hh : v.FnPoleOrderLE n h) :
v.FnPoleOrderLE n (g + h)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)
variable {v}
variable (v) intheorem FnPoleOrderLE.smul {n : ℕ} (c : K) {g : F} (hg : v.FnPoleOrderLE n g) :
v.FnPoleOrderLE n (algebraMap K F c * g)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)
variable {v}
variable (v) intheorem fnPoleOrderLE_zero_iff (g : F) : v.FnPoleOrderLE 0 g ↔ g ∈ v.toValuationSubringSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace Place
variable (v : Place K F)
variable {v}
variable (v) intheorem HasLogResidue.hasPoleOrderLE {ω : Ω[F⁄K]} {a : K} (h : v.HasLogResidue ω a) :
v.HasPoleOrderLE 1 ωDifferentials regular off the specified places and with at most simple poles at those places.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section LogForms
variable (K F)def logForms (S : Set (Place K F)) : Submodule K Ω[F⁄K] where
carrier := {ω | ∀ v : Place K F, (v ∉ S → v.HasPoleOrderLE 0 ω) ∧ (v ∈ S → v.HasPoleOrderLE 1 ω)}
zero_mem' v := ⟨fun _ => v.hasPoleOrderLE_zero_right 0, fun _ => v.hasPoleOrderLE_zero_right 1⟩
add_mem' hω hη v :=
⟨fun hv => ((hω v).1 hv).add ((hη v).1 hv), fun hv => ((hω v).2 hv).add ((hη v).2 hv)⟩
smul_mem' c _ hω v := ⟨fun hv => ((hω v).1 hv).smul c, fun hv => ((hω v).2 hv).smul c⟩Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section LogForms
variable (K F)
variable {K F}theorem mem_logForms_iff {S : Set (Place K F)} {ω : Ω[F⁄K]} :
ω ∈ logForms K F S ↔
∀ v : Place K F, (v ∉ S → v.HasPoleOrderLE 0 ω) ∧ (v ∈ S → v.HasPoleOrderLE 1 ω)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
section LogForms
variable (K F)
variable {K F}theorem regularDifferentials_le_logForms (S : Set (Place K F)) :
regularDifferentials K F ≤ logForms K F SDifferential-function pairs satisfying the logarithmic regularity conditions.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace LogDeRham
variable (K F)def cocycles (S : Set (Place K F)) : Submodule K (Ω[F⁄K] × F) where
carrier := {c | (∀ v : Place K F, v ∉ S → v.HasPoleOrderLE 0 c.1) ∧
(∀ v : Place K F, v ∈ S → v.HasPoleOrderLE 1 (c.1 - D K F c.2))}
zero_mem' := by
refine ⟨fun v _ => ?_, fun v _ => ?_⟩
· exact v.hasPoleOrderLE_zero_right 0
· change v.HasPoleOrderLE 1 ((0 : Ω[F⁄K]) - D K F (0 : F))
rw [map_zero, sub_zero]; exact v.hasPoleOrderLE_zero_right 1
add_mem' {c c'} hc hc' := by
refine ⟨fun v hv => ?_, fun v hv => ?_⟩
· change v.HasPoleOrderLE 0 (c.1 + c'.1)
exact (hc.1 v hv).add (hc'.1 v hv)
· have h := (hc.2 v hv).add (hc'.2 v hv)
change v.HasPoleOrderLE 1 ((c.1 + c'.1) - D K F (c.2 + c'.2))
rw [map_add]
convert h using 1
abel
smul_mem' a {c} hc := by
refine ⟨fun v hv => ?_, fun v hv => ?_⟩
· change v.HasPoleOrderLE 0 (a • c.1)
exact (hc.1 v hv).smul a
· have h := (hc.2 v hv).smul a
rw [smul_sub] at h
change v.HasPoleOrderLE 1 (a • c.1 - D K F (a • c.2))
have hD : D K F (a • c.2) = a • D K F c.2 := by
rw [Algebra.smul_def, Derivation.leibniz, Derivation.map_algebraMap, smul_zero, add_zero,
← algebraMap_smul F a (D K F c.2)]
rw [hD]; exact hExact differential-function pairs arising from functions regular off the specified places.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace LogDeRham
variable (K F)def exactPart (S : Set (Place K F)) : Submodule K (Ω[F⁄K] × F) where
carrier := {c | ∃ h : F, (∀ v : Place K F, v ∉ S → h ∈ v.toValuationSubring) ∧ c = (D K F h, h)}
zero_mem' := ⟨0, fun v _ => zero_mem _, Prod.ext (by simp) rfl⟩
add_mem' := by
rintro _ _ ⟨h, hh, rfl⟩ ⟨h', hh', rfl⟩
exact ⟨h + h', fun v hv => add_mem (hh v hv) (hh' v hv), Prod.ext (by simp [map_add]) rfl⟩
smul_mem' := by
rintro a _ ⟨h, hh, rfl⟩
refine ⟨a • h, fun v hv => ?_, ?_⟩
· rw [Algebra.smul_def]; exact mul_mem (v.algebraMap_mem' a) (hh v hv)
· have hD : D K F (a • h) = a • D K F h := by
rw [Algebra.smul_def, Derivation.leibniz, Derivation.map_algebraMap, smul_zero, add_zero,
← algebraMap_smul F a (D K F h)]
exact Prod.ext (by rw [Prod.smul_mk, hD]) (by rw [Prod.smul_mk])Pairs with zero differential and a function regular on the specified places.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace LogDeRham
variable (K F)def localPart (S : Set (Place K F)) : Submodule K (Ω[F⁄K] × F) where
carrier := {c | c.1 = 0 ∧ ∀ v : Place K F, v ∈ S → c.2 ∈ v.toValuationSubring}
zero_mem' := ⟨rfl, fun v _ => zero_mem _⟩
add_mem' {c c'} hc hc' := ⟨by rw [Prod.fst_add, hc.1, hc'.1, add_zero],
fun v hv => add_mem (hc.2 v hv) (hc'.2 v hv)⟩
smul_mem' a {c} hc := ⟨by rw [Prod.smul_fst, hc.1, smul_zero], fun v hv => by
rw [Prod.smul_snd, Algebra.smul_def]; exact mul_mem (v.algebraMap_mem' a) (hc.2 v hv)⟩The sum of the exact and locally regular subspaces.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace LogDeRham
variable (K F)def coboundaries (S : Set (Place K F)) : Submodule K (Ω[F⁄K] × F)The coboundary subspace regarded as a subspace of cocycles.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace LogDeRham
variable (K F)abbrev coboundariesIn (S : Set (Place K F)) : Submodule K ↥(cocycles K F S)Logarithmic de Rham cocycles modulo coboundaries.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace LogDeRham
variable (K F)abbrev H1 (S : Set (Place K F)) : Type _Functions integral at every place outside the specified set.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace LogDeRham
variable (K F)def regularOff (S : Set (Place K F)) : Submodule K F where
carrier := {h | ∀ v : Place K F, v ∉ S → h ∈ v.toValuationSubring}
zero_mem' v _ := zero_mem _
add_mem' {h h'} hh hh' v hv := add_mem (hh v hv) (hh' v hv)
smul_mem' a {h} hh v hv := by rw [Algebra.smul_def]; exact mul_mem (v.algebraMap_mem' a) (hh v hv)Functions integral at every place in the specified set.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace LogDeRham
variable (K F)def regularOn (S : Set (Place K F)) : Submodule K F where
carrier := {r | ∀ v : Place K F, v ∈ S → r ∈ v.toValuationSubring}
zero_mem' v _ := zero_mem _
add_mem' {h h'} hh hh' v hv := add_mem (hh v hv) (hh' v hv)
smul_mem' a {h} hh v hv := by rw [Algebra.smul_def]; exact mul_mem (v.algebraMap_mem' a) (hh v hv)Functions modulo the sum of the subspaces regular on and off the specified set.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace LogDeRham
variable (K F)abbrev H1O (S : Set (Place K F)) : Type _The quotient map from logarithmic cocycles to their cohomology classes.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace LogDeRham
variable (K F)
namespace H1
variable {K F}
variable (S : Set (Place K F))def mk : ↥(cocycles K F S) →ₗ[K] H1 K F SSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace LogDeRham
variable (K F)
namespace H1
variable {K F}
variable (S : Set (Place K F))theorem inl_mem_cocycles {ω : Ω[F⁄K]} (hω : ω ∈ logForms K F S) : (ω, (0 : F)) ∈ cocycles K F SThe cohomology class of a logarithmic differential with zero function component.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace LogDeRham
variable (K F)
namespace H1
variable {K F}
variable (S : Set (Place K F))def ofLog : ↥(logForms K F S) →ₗ[K] H1 K F SThe logarithmic cohomology class of a regular differential.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace LogDeRham
variable (K F)
namespace H1
variable {K F}
variable (S : Set (Place K F))def ofRegular : ↥(regularDifferentials K F) →ₗ[K] H1 K F SSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace LogDeRham
variable (K F)
namespace H1
variable {K F}
variable (S : Set (Place K F))theorem snd_mem_of_mem_coboundaries {c : Ω[F⁄K] × F} (hc : c ∈ coboundaries K F S) :
c.2 ∈ regularOff K F S ⊔ regularOn K F SThe map on cohomology induced by the function component of a cocycle.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace LogDeRham
variable (K F)
namespace H1
variable {K F}
variable (S : Set (Place K F))def toH1O : H1 K F S →ₗ[K] H1O K F SA representative of the class has the specified logarithmic residue at the place.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace LogDeRham
variable (K F)
namespace H1
variable {K F}
variable (S : Set (Place K F))def HasResidueAt (v : Place K F) (x : H1 K F S) (a : K) : PropThe cohomology class has residue zero at each specified place.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace LogDeRham
variable (K F)
namespace H1
variable {K F}
variable (S : Set (Place K F))def IsSecondKind (x : H1 K F S) : PropThe differential represents the class with a function component of bounded pole order.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace LogDeRham
variable (K F)
namespace H1
variable {K F}
variable (S : Set (Place K F))def IsClassOfWithTail (m : ℕ) (ω : Ω[F⁄K]) (x : H1 K F S) : PropThe map on differentials induced by the given algebra homomorphism.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace LogDeRham
variable (K F)
section Map
variable {K F}
variable {F' : Type*} [Field F'] [Algebra K F']def pullbackForm (φ : F →ₐ[K] F') : Ω[F⁄K] →ₗ[K] Ω[F'⁄K]Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace LogDeRham
variable (K F)
section Map
variable {K F}
variable {F' : Type*} [Field F'] [Algebra K F']theorem pullbackForm_D (φ : F →ₐ[K] F') (x : F) :
pullbackForm φ (D K F x) = D K F' (φ x)Apply the induced map on differentials and the algebra map to a cocycle pair.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace LogDeRham
variable (K F)
section Map
variable {K F}
variable {F' : Type*} [Field F'] [Algebra K F']def pullbackPair (φ : F →ₐ[K] F') : (Ω[F⁄K] × F) →ₗ[K] (Ω[F'⁄K] × F')Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace LogDeRham
variable (K F)
section Map
variable {K F}
variable {F' : Type*} [Field F'] [Algebra K F']theorem pullbackPair_apply (φ : F →ₐ[K] F') (c : Ω[F⁄K] × F) :
pullbackPair φ c = (pullbackForm φ c.1, φ c.2)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace LogDeRham
variable (K F)
section Map
variable {K F}
variable {F' : Type*} [Field F'] [Algebra K F']theorem pullbackPair_D (φ : F →ₐ[K] F') (h : F) :
pullbackPair φ (D K F h, h) = (D K F' (φ h), φ h)The map on logarithmic cohomology induced by a map preserving cocycles and coboundaries.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace LogDeRham
variable (K F)
section Map
variable {K F}
variable {F' : Type*} [Field F'] [Algebra K F']def H1.map (S : Set (Place K F)) (T : Set (Place K F')) (φ : F →ₐ[K] F')
(hZ : ∀ c ∈ cocycles K F S, pullbackPair φ c ∈ cocycles K F' T)
(hB : ∀ c ∈ coboundaries K F S, pullbackPair φ c ∈ coboundaries K F' T) :
H1 K F S →ₗ[K] H1 K F' TSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace LogDeRham
variable (K F)
section Map
variable {K F}
variable {F' : Type*} [Field F'] [Algebra K F']theorem H1.map_mk (S : Set (Place K F)) (T : Set (Place K F')) (φ : F →ₐ[K] F')
(hZ : ∀ c ∈ cocycles K F S, pullbackPair φ c ∈ cocycles K F' T)
(hB : ∀ c ∈ coboundaries K F S, pullbackPair φ c ∈ coboundaries K F' T)
(c : ↥(cocycles K F S)) :
H1.map S T φ hZ hB (H1.mk S c) = H1.mk T ⟨pullbackPair φ c, hZ c c.2⟩Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace LogDeRham
variable (K F)
section Frobenius
variable {K F}
variable (p : ℕ) [Fact p.Prime] [CharP K p]
omit [Fact p.Prime] intheorem D_pow_char (g : F) : D K F (g ^ p) = 0The Frobenius-semilinear map taking a pair to zero and the power of its function component.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace LogDeRham
variable (K F)
section Frobenius
variable {K F}
variable (p : ℕ) [Fact p.Prime] [CharP K p]def frobPair : (Ω[F⁄K] × F) →ₛₗ[frobenius K p] (Ω[F⁄K] × F) where
toFun c := (0, c.2 ^ p)
map_add' c c' := by
ext
· simp
· have : CharP F p := charP_of_injective_algebraMap (algebraMap K F).injective p
change (c.2 + c'.2) ^ p = c.2 ^ p + c'.2 ^ p
exact add_pow_char (p := p) c.2 c'.2
map_smul' a c := by
ext
· simp
· simp only [Prod.smul_snd, frobenius_def, Algebra.smul_def, mul_pow, map_pow]Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace LogDeRham
variable (K F)
section Frobenius
variable {K F}
variable (p : ℕ) [Fact p.Prime] [CharP K p]
variable (S : Set (Place K F))theorem frobPair_mem_cocycles (c : ↥(cocycles K F S)) : frobPair p (c : Ω[F⁄K] × F) ∈ cocycles K F
SThe Frobenius-semilinear map restricted to logarithmic cocycles.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace LogDeRham
variable (K F)
section Frobenius
variable {K F}
variable (p : ℕ) [Fact p.Prime] [CharP K p]
variable (S : Set (Place K F))def frobCocycles : ↥(cocycles K F S) →ₛₗ[frobenius K p] ↥(cocycles K F S)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace LogDeRham
variable (K F)
section Frobenius
variable {K F}
variable (p : ℕ) [Fact p.Prime] [CharP K p]
variable (S : Set (Place K F))theorem coboundariesIn_le_comap_frobCocycles :
coboundariesIn K F S ≤ (coboundariesIn K F S).comap (frobCocycles p S)The Frobenius-semilinear endomorphism of logarithmic cohomology.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace LogDeRham
variable (K F)
section Frobenius
variable {K F}
variable (p : ℕ) [Fact p.Prime] [CharP K p]
variable (S : Set (Place K F))def H1.frob : H1 K F S →ₛₗ[frobenius K p] H1 K F SThe semilinearity, exactness, and pole-preservation properties required of a Cartier map.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace LogDeRham
variable (K F)
section Cartier
variable {K F}
variable (p : ℕ) [Fact p.Prime] [CharP K p] [PerfectRing K p]structure CartierHypotheses (C : Ω[F⁄K] →+ Ω[F⁄K]) : Prop where
/-- The map is semilinear for inverse Frobenius on the base field. -/
semi : ∀ (a : K) (ω : Ω[F⁄K]), C (a • ω) = (frobeniusEquiv K p).symm a • C ω
/-- The map kills exact differentials. -/
ker : ∀ f : F, C (D K F f) = 0
/-- The map preserves regularity at each place. -/
regular : ∀ (v : Place K F) (ω : Ω[F⁄K]), v.HasPoleOrderLE 0 ω → v.HasPoleOrderLE 0 (C ω)
/-- The map preserves the bound of at most a simple pole at each place. -/
log : ∀ (v : Place K F) (ω : Ω[F⁄K]), v.HasPoleOrderLE 1 ω → v.HasPoleOrderLE 1 (C ω)Apply the Cartier map to the differential component and set the function component to zero.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace LogDeRham
variable (K F)
section Cartier
variable {K F}
variable (p : ℕ) [Fact p.Prime] [CharP K p] [PerfectRing K p]
variable {p}
variable {C : Ω[F⁄K] →+ Ω[F⁄K]} (hC : CartierHypotheses p C)
variable (S : Set (Place K F))def cartierPair :
(Ω[F⁄K] × F) →ₛₗ[((frobeniusEquiv K p).symm : K →+* K)] (Ω[F⁄K] × F) where
toFun c := (C c.1, 0)
map_add' c c' := by ext <;> simp [map_add]
map_smul' a c := by
ext
· simp only [Prod.smul_fst, RingHom.coe_coe]; exact hC.semi a c.1
· simpSurrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace LogDeRham
variable (K F)
section Cartier
variable {K F}
variable (p : ℕ) [Fact p.Prime] [CharP K p] [PerfectRing K p]
variable {p}
variable {C : Ω[F⁄K] →+ Ω[F⁄K]} (hC : CartierHypotheses p C)
variable (S : Set (Place K F))theorem cartierPair_mem_cocycles (c : ↥(cocycles K F S)) :
cartierPair hC (c : Ω[F⁄K] × F) ∈ cocycles K F SThe inverse-Frobenius-semilinear Cartier map restricted to logarithmic cocycles.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace LogDeRham
variable (K F)
section Cartier
variable {K F}
variable (p : ℕ) [Fact p.Prime] [CharP K p] [PerfectRing K p]
variable {p}
variable {C : Ω[F⁄K] →+ Ω[F⁄K]} (hC : CartierHypotheses p C)
variable (S : Set (Place K F))def cartierCocycles :
↥(cocycles K F S) →ₛₗ[((frobeniusEquiv K p).symm : K →+* K)] ↥(cocycles K F S)Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace LogDeRham
variable (K F)
section Cartier
variable {K F}
variable (p : ℕ) [Fact p.Prime] [CharP K p] [PerfectRing K p]
variable {p}
variable {C : Ω[F⁄K] →+ Ω[F⁄K]} (hC : CartierHypotheses p C)
variable (S : Set (Place K F))theorem coboundariesIn_le_comap_cartierCocycles :
coboundariesIn K F S ≤ (coboundariesIn K F S).comap (cartierCocycles hC S)The Cartier endomorphism induced on logarithmic cohomology.
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open KaehlerDifferential
namespace AlgebraicCurve
variable {K F : Type*} [Field K] [Field F] [Algebra K F]
namespace LogDeRham
variable (K F)
section Cartier
variable {K F}
variable (p : ℕ) [Fact p.Prime] [CharP K p] [PerfectRing K p]
variable {p}
variable {C : Ω[F⁄K] →+ Ω[F⁄K]} (hC : CartierHypotheses p C)
variable (S : Set (Place K F))def H1.cartier :
H1 K F S →ₛₗ[((frobeniusEquiv K p).symm : K →+* K)] H1 K F S