Theorems · Inductive type · commutative algebra

Module.Relations.Solution.IsPresentationCore

{A : Type u} →
  [inst : Ring A] →
    {relations : Module.Relations A} →
      {M : Type v} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module A M] → relations.Solution M → Type (max (max (max u v) (w' + 1)) w₀)

Helper structure in order to prove Module.Relations.Solutions.IsPresentation by showing the universal property of the module defined by generators and relations. The universal property is restricted to modules that are in Type w' for an auxiliary universe w'. See IsPresentationCore.isPresentation.

Defined in

Mathlib.Algebra.Module.Presentation.Basic

Cited by

7 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

RingAddCommGroupModule