Theorems · Inductive type · commutative algebra

Algebra.Generators.Hom

{R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : Algebra R S] →
            Algebra.Generators R S ι →
              {R' : Type u_1} →
                {S' : Type u_2} →
                  {ι' : Type u_3} →
                    [inst : CommRing R'] →
                      [inst_3 : CommRing S'] →
                        [inst_4 : Algebra R' S'] →
                          Algebra.Generators R' S' ι' → [Algebra S S'] → Type (max (max u_1 u_3) w)

Given a commuting square R --→ P = R[X] → S | | ↓ ↓ R' -→ P' = R'[X'] → S A hom between P and P' is an assignment I → P' such that the arrows commute. Also see Algebra.Generators.Hom.equivAlgHom.

Defined in

Mathlib.RingTheory.Extension.Generators

Cited by

28 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

CommRingCommRingAlgebraCommRingCommRingAlgebraAlgebra