Theorems · Definition · commutative algebra

AlgHom.liftEquiv

(R : Type u_4) →
  (S : Type u_5) →
    (A : Type u_6) →
      (B : Type u_7) →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring S] →
            [inst_2 : Semiring A] →
              [inst_3 : Semiring B] →
                [inst_4 : Algebra R A] →
                  [inst_5 : Algebra S B] →
                    [inst_6 : Algebra R S] →
                      [inst_7 : Algebra R B] → [IsScalarTower R S B] → (A →ₐ[R] B) ≃ (TensorProduct R S A →ₐ[S] B)

Universal property of the base change of algebra. An algebra map from the base change is equivalent to an algebra map over the base ring. In categorical terms, this is an adjunction between: 1. A ↦ S ⊗[R] A, a functor R-Alg ⥤ S-Alg (the base change). 2. B ↦ B, a functor S-Alg ⥤ R-Alg (the restriction).

Defined in

Mathlib.RingTheory.TensorProduct.Basic

Cited by

4 results in Mathlib

Foundations

Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringCommSemiringSemiringSemiringAlgebraAlgebraAlgebraAlgebraIsScalarTower