Theorems · Theorem · commutative algebra

Algebra.PreSubmersivePresentation.isUnit_jacobian_of_cotangentRestrict_bijective

∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type u_3}
  {σ : Type u_4} (P : Algebra.PreSubmersivePresentation R S ι σ) [inst_3 : Finite σ]
  (b : Module.Basis σ S P.toExtension.Cotangent),
  (∀ (r : σ), b r = Algebra.Extension.Cotangent.mk ⟨P.relation r, ⋯⟩) →
    Function.Bijective ⇑(P.cotangentRestrict ⋯) → IsUnit P.jacobian

To show a pre-submersive presentation with kernel I = (fᵢ) is submersive, it suffices to show that the images of the fᵢ form a basis of I/I² and that the restricted cotangent complex I/I² → S ⊗[R] (Ω[R[Xᵢ]⁄R]) = ⊕ᵢ S → ⊕ⱼ S is bijective.

Defined in

Mathlib.RingTheory.Extension.Cotangent.Free

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraFinite