Theorems · Inductive type · commutative algebra

Algebra.SubmersivePresentation

(R : Type u) →
  (S : Type v) →
    Type w →
      (σ : Type t) →
        [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → [Finite σ] → Type (max (max (max t u) v) w)

A PreSubmersivePresentation is submersive if its Jacobian is a unit in S and the presentation is finite.

Defined in

Mathlib.RingTheory.Extension.Presentation.Submersive

Cited by

52 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

CommRingCommRingAlgebraFinite