Theorems · Theorem · commutative algebra

Algebra.Generators.exists_presentation_of_basis_cotangent

∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.FinitePresentation R S] {α : Type u_4} (P : Algebra.Generators R S α) [Finite α] {σ : Type u_5}
  (b₀ : Module.Basis σ S P.toExtension.Cotangent),
  ∃ P' b, P'.val ∘ Sum.inr = P.val ∧ ∀ (r : Unit ⊕ σ), b r = Algebra.Extension.Cotangent.mk ⟨P'.relation r, ⋯⟩

Version of Algebra.Generators.exists_presentation_of_free_cotangent taking a basis instead of a Module.Free assumption. Note that the basis b₀ only serves as a way of saying that I/I² is free of rank σ, which gives more definitional control over σ. If this does not matter, use Algebra.Generators.exists_presentation_of_free_cotangent instead.

Defined in

Mathlib.RingTheory.Extension.Cotangent.Basis

Cited by

2 results in Mathlib

Foundations

Depth 153 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCommRingAlgebraAlgebra.FinitePresentationFinite