OAI/AlgebraicGeometry/CommutingDerivations/DescentFamily.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Properties of an actual descended family with a common clearing power. All hypotheses describe explicit maps and identities; none assumes the desired family properties on the original ring.

  1. theorem OAI.AbhyankarSathaye.CommutingDerivations.descended_fixes_parameter line 15
  2. theorem OAI.AbhyankarSathaye.CommutingDerivations.descended_kernel line 22
  3. theorem OAI.AbhyankarSathaye.CommutingDerivations.descended_locallyNilpotent line 36
  4. theorem OAI.AbhyankarSathaye.CommutingDerivations.descended_commute line 45
  5. theorem OAI.AbhyankarSathaye.CommutingDerivations.descended_linearIndependent line 62

    Source documentation

    Localized coordinate slices prove independence over the original ring. Each slice is required to have an actual denominator-clearing witness. This is provided by the defining surjectivity of localization, with no assumption that the slices already lie in A.

    theorem descended_linearIndependent [Fintype I] [DecidableEq I]
    (ι : A →ₐ[K] L) (hinj : Function.Injective ι) (c : A)
    (hu : IsUnit (ι c)) (N : ℕ)
    (D : I → Derivation K L L) (d : I → Derivation K A A)
    (hdesc : ∀ i a, ι (d i a) = (ι c)^N * D i (ι a))
    (hfix : ∀ i, D i (ι c) = 0)
    (t : I → L) (ht : ∀ i j, D i (t j) = if i = j then 1 else 0)
    (hfrac : ∀ j, ∃ (n : ℕ) (r : A), t j * (ι c)^n = ι r) :
    LinearIndependent A d := by
…