Cartier_map_eq_map_cartier_of_constantFieldExtension.lean

theorem C_pow_smul_D_eq_zero {K F : Type*} [Field K] [Field F] [Algebra K F] (p : ℕ) [CharP F p]
    (C : Ω[F⁄K] →+ Ω[F⁄K]) (hker : ∀ f : F, C (D K F f) = 0) (t : F) {i : ℕ} (hi : i + 1 < p) :
    C (t ^ i • D K F t) = 0

theorem C_digits_smul_D {K F : Type*} [Field K] [Field F] [Algebra K F] (p : ℕ) [hp : Fact p.Prime]
    [CharP F p] (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)
    (t : F) (a : Fin p → F) :
    C ((∑ i : Fin p, a i ^ p * t ^ (i : ℕ)) • D K F t)
      = a ⟨p - 1, Nat.sub_lt hp.out.pos Nat.one_pos⟩ • D K F t

theorem exists_eq_smul_D {K F : Type*} [Field K] [Field F] [Algebra K F] (p : ℕ) [CharP F p] (t : F)
    (hdig : ∀ g : F, ∃ a : Fin p → F, g = ∑ i : Fin p, a i ^ p * t ^ (i : ℕ)) (ω : Ω[F⁄K]) :
    ∃ g : F, ω = g • D K F t

theorem _root_.AlgebraicCurve.cartier_map_eq_map_cartier_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']
    [PerfectField K] [AlgebraicCurve.IsCurveOver K F]
    (p : ℕ) [Fact p.Prime] [CharP K p]
    (hfg : ∃ x : F, Transcendental K x ∧ 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 (KaehlerDifferential.D K F f) = 0)
    (hlog : ∀ f : F, C (f ^ (p - 1) • KaehlerDifferential.D K F f) = KaehlerDifferential.D K F f)
    (C' : Ω[F'⁄K'] →+ Ω[F'⁄K'])
    (hsemi' : ∀ (f : F') (ω : Ω[F'⁄K']), C' (f ^ p • ω) = f • C' ω)
    (hker' : ∀ f : F', C' (KaehlerDifferential.D K' F' f) = 0)
    (hlog' : ∀ f : F', C' (f ^ (p - 1) • KaehlerDifferential.D K' F' f) = KaehlerDifferential.D K'
      F' f) :
    ∀ ω : Ω[F⁄K], C' (KaehlerDifferential.map K K' F F' ω) = KaehlerDifferential.map K K' F F' (C
      ω)