Computation of Jacobian of presentations from basis of Cotangent

Let P be a presentation of an R-algebra S with kernel I = (fᵢ). In this file we provide lemmas to show that P is submersive when given suitable bases of I/I² and Ω[S⁄R].

We will later deduce from this a presentation-independent characterisation of standard smooth algebras (TODO @chrisflav).

Main results

• PreSubmersivePresentation.isUnit_jacobian_of_cotangentRestrict_bijective: If the fᵢ form a basis of I/I² and the restricted cotangent complex I/I² → S ⊗[R] (Ω[R[Xᵢ]⁄R]) = ⊕ᵢ S → ⊕ⱼ S is bijective, P is submersive.

theorem Algebra.Generators.cotangentRestrict_bijective_of_isCompl {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {ι : Type u_3} {σ : Type u_4} {κ : Type u_5} (P : Generators R S ι) {u : σ → ι} (hu : Function.Injective u) {v : κ → ι} (huv : IsCompl (Set.range v) (Set.range u)) (hm : Submodule.span S (Set.range fun (i : κ) => (KaehlerDifferential.D R S) (P.val (v i))) = ⊤) (hk : Disjoint (LinearMap.ker P.toExtension.toKaehler) (Submodule.span S (Set.range fun (x : κ) => P.cotangentSpaceBasis (v x)))) [Subsingleton (H1Cotangent R S)] : Function.Bijective ⇑(P.cotangentRestrict hu)

If H¹(L_{S/R}) = 0 and R[xᵢ] → S are generators indexed by σ ⊕ κ such that the images of dxₖ for k : κ span Ω[S⁄R] and the span of the dXₖ for k : κ in S ⊗[R] Ω[R[Xᵢ⁄R]] intersects the kernel of the projection trivially, then the restriction of I/I² → ⊕ S dxᵢ to the direct sum indexed by i : ι is an isomorphism.

The assumptions are in particular satisfied if the dsₖ form an S-basis of Ω[S⁄R], see Generators.disjoint_ker_toKaehler_of_linearIndependent for one half. Via PreSubmersivePresentation.isUnit_jacobian_of_cotangentRestrict_bijective, this can be useful to show a presentation is submersive.

theorem Algebra.Generators.disjoint_ker_toKaehler_of_linearIndependent {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {ι : Type u_3} {κ : Type u_5} (P : Generators R S ι) {v : κ → ι} (h : LinearIndependent S fun (k : κ) => (KaehlerDifferential.D R S) (P.val (v k))) : Disjoint (LinearMap.ker P.toExtension.toKaehler) (Submodule.span S (Set.range fun (x : κ) => P.cotangentSpaceBasis (v x)))

theorem Algebra.PreSubmersivePresentation.isUnit_jacobian_of_cotangentRestrict_bijective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [Algebra R S] {ι : Type u_3} {σ : Type u_4} (P : PreSubmersivePresentation R S ι σ) [Finite σ] (b : Module.Basis σ S P.toExtension.Cotangent) (hb : ∀ (r : σ), b r = Extension.Cotangent.mk ⟨P.relation r, ⋯⟩) (h : 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.