noncomputable def DModules.endBracketMul {k : Type u} [CommRing k] {A : Type v} [CommRing A] [Algebra k A] (L : Module.End k A) (f : A) : Module.End k A

noncomputable def DModules.diffOpOrder (k : Type u) [CommRing k] (A : Type v) [CommRing A] [Algebra k A] : ℕ → Submodule k (Module.End k A)

noncomputable def DModules.diffOps (k : Type u) [CommRing k] (A : Type v) [CommRing A] [Algebra k A] : Submodule k (Module.End k A)

structure DModules.LeftDModule (k : Type u) [CommRing k] (A : Type v) [CommRing A] [Algebra k A] (M : Type w) [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] : Type (max v w)

• vecFieldAction : Derivation k A A → M →ₗ[k] M
• vecFieldAction_smul (v : Derivation k A A) (f : A) (m : M) : (self.vecFieldAction v) (f • m) = f • (self.vecFieldAction v) m + v f • m
• vecFieldAction_smul_vec (f : A) (v : Derivation k A A) (m : M) : (self.vecFieldAction (f • v)) m = f • (self.vecFieldAction v) m
• vecFieldAction_lie (v w : Derivation k A A) (m : M) : (self.vecFieldAction v) ((self.vecFieldAction w) m) - (self.vecFieldAction w) ((self.vecFieldAction v) m) = (self.vecFieldAction ⁅v, w⁆) m

structure DModules.RightDModule (k : Type u) [CommRing k] (A : Type v) [CommRing A] [Algebra k A] (M : Type w) [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] : Type (max v w)

• vecFieldAction : Derivation k A A → M →ₗ[k] M
• right_leibniz (v : Derivation k A A) (f : A) (m : M) : (self.vecFieldAction v) (f • m) = f • (self.vecFieldAction v) m - v f • m
• lin_in_vec (f : A) (v : Derivation k A A) (m : M) : (self.vecFieldAction (f • v)) m = f • (self.vecFieldAction v) m
• flat (v w : Derivation k A A) (m : M) : (self.vecFieldAction v) ((self.vecFieldAction w) m) - (self.vecFieldAction w) ((self.vecFieldAction v) m) = -(self.vecFieldAction ⁅v, w⁆) m

structure DModules.SheafOfDiffOps (k : Type u) [CommRing k] : Type (max (max u (v + 1)) (w + 1))

• I : Type v
• coordRing : self.I → Type w
• instCommRing (i : self.I) : CommRing (self.coordRing i)
• instAlgebra (i : self.I) : Algebra k (self.coordRing i)
• diffOpsRing : self.I → Type w
• instDiffRing (i : self.I) : Ring (self.diffOpsRing i)
• instDiffAlgebra (i : self.I) : Algebra (self.coordRing i) (self.diffOpsRing i)
• incl : self.I → self.I → Prop
• incl_refl (i : self.I) : self.incl i i
• incl_trans {i j k : self.I} : self.incl i j → self.incl j k → self.incl i k
• coordRestrict {i j : self.I} : self.incl i j → self.coordRing i →+* self.coordRing j
• diffOpsRestrict {i j : self.I} : self.incl i j → self.diffOpsRing i →+* self.diffOpsRing j

noncomputable def DModules.SheafOfDiffOps.baseChangeType {k : Type u} [CommRing k] (D : SheafOfDiffOps k) {i j : D.I} (h : D.incl i j) (Mi : Type w) (inst_acg : AddCommGroup Mi) (inst_mod : Module (D.diffOpsRing i) Mi) : Type w

@[reducible]

noncomputable def DModules.SheafOfDiffOps.baseChangeAddCommGroup {k : Type u} [CommRing k] (D : SheafOfDiffOps k) {i j : D.I} (h : D.incl i j) (Mi : Type w) (inst_acg : AddCommGroup Mi) (inst_mod : Module (D.diffOpsRing i) Mi) : AddCommGroup (D.baseChangeType h Mi inst_acg inst_mod)

structure DModules.LeftDModuleSheaf (k : Type u) [CommRing k] (D : SheafOfDiffOps k) : Type (max v (w + 1))

• sections : D.I → Type w
• instAddCommGroup (i : D.I) : AddCommGroup (self.sections i)
• instModule (i : D.I) : Module (D.diffOpsRing i) (self.sections i)
• restrict {i j : D.I} : D.incl i j → self.sections i → self.sections j
• restrict_add {i j : D.I} (h : D.incl i j) (s t : self.sections i) : self.restrict h (s + t) = self.restrict h s + self.restrict h t
• restrict_smul {i j : D.I} (h : D.incl i j) (d : D.diffOpsRing i) (s : self.sections i) : self.restrict h (d • s) = (D.diffOpsRestrict h) d • self.restrict h s
• restrict_id (i : D.I) (s : self.sections i) : self.restrict ⋯ s = s
• restrict_comp {i j k : D.I} (hij : D.incl i j) (hjk : D.incl j k) (s : self.sections i) : self.restrict ⋯ s = self.restrict hjk (self.restrict hij s)
• locality (i : D.I) (s : self.sections i) : (∀ (j : D.I) (h : D.incl i j), self.restrict h s = 0) → s = 0
• gluing {i : D.I} (cover : D.I → Prop) (hcover : ∀ (j : D.I), cover j → D.incl i j) (sec : (j : D.I) → cover j → self.sections j) : (∀ (j : D.I) (hj : cover j) (l : D.I) (hl : cover l) (m : D.I) (hjm : D.incl j m) (hlm : D.incl l m), self.restrict hjm (sec j hj) = self.restrict hlm (sec l hl)) → ∃ (s : self.sections i), ∀ (j : D.I) (hj : cover j), self.restrict ⋯ s = sec j hj
• quasicoherent {i j : D.I} (h : D.incl i j) (s : self.sections j) : ∃ (n : ℕ) (fs : Fin n → D.coordRing j) (gs : Fin n → self.sections i), s = ∑ t : Fin n, (algebraMap (D.coordRing j) (D.diffOpsRing j)) (fs t) • self.restrict h (gs t)
• quasicoherent_iso {i j : D.I} (h : D.incl i j) : Nonempty (D.baseChangeType h (self.sections i) (self.instAddCommGroup i) (self.instModule i) ≃+ self.sections j)

structure DModules.RightDModuleSheaf (k : Type u) [CommRing k] (D : SheafOfDiffOps k) : Type (max v (w + 1))

• sections : D.I → Type w
• instAddCommGroup (i : D.I) : AddCommGroup (self.sections i)
• instModule (i : D.I) : Module (D.diffOpsRing i)ᵐᵒᵖ (self.sections i)
• restrict {i j : D.I} : D.incl i j → self.sections i → self.sections j
• restrict_add {i j : D.I} (h : D.incl i j) (s t : self.sections i) : self.restrict h (s + t) = self.restrict h s + self.restrict h t
• restrict_smul {i j : D.I} (h : D.incl i j) (d : (D.diffOpsRing i)ᵐᵒᵖ) (s : self.sections i) : self.restrict h (d • s) = MulOpposite.op ((D.diffOpsRestrict h) (MulOpposite.unop d)) • self.restrict h s
• restrict_id (i : D.I) (s : self.sections i) : self.restrict ⋯ s = s
• restrict_comp {i j k : D.I} (hij : D.incl i j) (hjk : D.incl j k) (s : self.sections i) : self.restrict ⋯ s = self.restrict hjk (self.restrict hij s)
• locality (i : D.I) (s : self.sections i) : (∀ (j : D.I) (h : D.incl i j), self.restrict h s = 0) → s = 0
• gluing {i : D.I} (cover : D.I → Prop) (hcover : ∀ (j : D.I), cover j → D.incl i j) (sec : (j : D.I) → cover j → self.sections j) : (∀ (j : D.I) (hj : cover j) (l : D.I) (hl : cover l) (m : D.I) (hjm : D.incl j m) (hlm : D.incl l m), self.restrict hjm (sec j hj) = self.restrict hlm (sec l hl)) → ∃ (s : self.sections i), ∀ (j : D.I) (hj : cover j), self.restrict ⋯ s = sec j hj
• quasicoherent {i j : D.I} (h : D.incl i j) (s : self.sections j) : ∃ (n : ℕ) (fs : Fin n → D.coordRing j) (gs : Fin n → self.sections i), s = ∑ t : Fin n, MulOpposite.op ((algebraMap (D.coordRing j) (D.diffOpsRing j)) (fs t)) • self.restrict h (gs t)

structure DModules.Connection (k : Type u) [CommRing k] (A : Type v) [CommRing A] [Algebra k A] (M : Type w) [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] : Type (max v w)

• nabla : M →ₗ[k] TensorProduct A M Ω[A⁄k]
• leibniz (f : A) (m : M) : self.nabla (f • m) = f • self.nabla m + ((TensorProduct.mk A M Ω[A⁄k]) m) ((KaehlerDifferential.D k A) f)

noncomputable def DModules.covariantDerivative {k : Type u} [CommRing k] {A : Type v} [CommRing A] [Algebra k A] {M : Type w} [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] (v : Derivation k A A) (conn : Connection k A M) : M →ₗ[k] M

noncomputable def DModules.curvature {k : Type u} [CommRing k] {A : Type v} [CommRing A] [Algebra k A] {M : Type w} [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] (conn : Connection k A M) (v w : Derivation k A A) : M →ₗ[k] M

def DModules.Connection.IsFlat {k : Type u} [CommRing k] {A : Type v} [CommRing A] [Algebra k A] {M : Type w} [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] (conn : Connection k A M) : Prop

theorem DModules.liftKaehlerDifferential_smul {k : Type u} [CommRing k] {A : Type v} [CommRing A] [Algebra k A] (f : A) (v : Derivation k A A) : (f • v).liftKaehlerDifferential = f • v.liftKaehlerDifferential

noncomputable def DModules.LeftDModule.ofFlatConnection {k : Type u} [CommRing k] {A : Type v} [CommRing A] [Algebra k A] {M : Type w} [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] (conn : Connection k A M) (hflat : conn.IsFlat) : LeftDModule k A M

theorem DModules.LeftDModule.exists_flat_connection {k : Type u} [CommRing k] {A : Type v} [CommRing A] [Algebra k A] {M : Type w} [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] [Module.Projective A Ω[A⁄k]] (D : LeftDModule k A M) : ∃ (conn : Connection k A M), conn.IsFlat ∧ ∀ (v : Derivation k A A) (m : M), (covariantDerivative v conn) m = (D.vecFieldAction v) m

noncomputable def DModules.LeftDModule.connectionOfLeftDModule {k : Type u} [CommRing k] {A : Type v} [CommRing A] [Algebra k A] {M : Type w} [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] [Module.Projective A Ω[A⁄k]] (D : LeftDModule k A M) : Connection k A M

theorem DModules.LeftDModule.connectionOfLeftDModule_covariantDerivative {k : Type u} [CommRing k] {A : Type v} [CommRing A] [Algebra k A] {M : Type w} [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] [Module.Projective A Ω[A⁄k]] (D : LeftDModule k A M) (v : Derivation k A A) (m : M) : (covariantDerivative v D.connectionOfLeftDModule) m = (D.vecFieldAction v) m

theorem DModules.LeftDModule.connectionOfLeftDModule_isFlat {k : Type u} [CommRing k] {A : Type v} [CommRing A] [Algebra k A] {M : Type w} [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] [Module.Projective A Ω[A⁄k]] (D : LeftDModule k A M) : D.connectionOfLeftDModule.IsFlat

@[reducible, inline]

noncomputable abbrev DModules.TransferBimodule (OY : Type u) [CommRing OY] (OX : Type v) [CommRing OX] [Algebra OY OX] (DY : Type w) [AddCommGroup DY] [Module OY DY] : Type (max v w)

@[reducible, inline]

noncomputable abbrev DModules.inverseImageModule (OY : Type u) [CommRing OY] (OX : Type v) [CommRing OX] [Algebra OY OX] (N : Type w) [AddCommGroup N] [Module OY N] : Type (max v w)

@[reducible, inline]

noncomputable abbrev DModules.directImageModule (OY : Type u) [CommRing OY] (OX : Type v) [CommRing OX] [Algebra OY OX] (DY : Type w) [AddCommGroup DY] [Module OY DY] (M : Type x) [AddCommGroup M] [Module OX M] : Type (max x v w)