Theorems · Inductive type · commutative algebra

Algebra.PreSubmersivePresentation

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

A PreSubmersivePresentation of an R-algebra S is a Presentation with relations equipped with an injective map : relations → vars. This map determines how the differential of P is constructed. See PreSubmersivePresentation.differential for details.

Defined in

Mathlib.RingTheory.Extension.Presentation.Submersive

Cited by

54 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

CommRingCommRingAlgebra