Theorems · Definition · algebraic geometry

AlgebraicGeometry.Spec.mapMulEquiv

{R S T : Type u} →
  [inst : CommRing R] →
    [inst_1 : CommRing S] →
      [inst_2 : CommRing T] →
        [inst_3 : Bialgebra R S] →
          [inst_4 : Algebra R T] →
            WithConv (S →ₐ[R] T) ≃*
              ((AlgebraicGeometry.Spec (CommRingCat.of T)).asOver (AlgebraicGeometry.Spec (CommRingCat.of R)) ⟶
                (AlgebraicGeometry.Spec (CommRingCat.of S)).asOver (AlgebraicGeometry.Spec (CommRingCat.of R)))

Spec.map as a MulEquiv on hom-sets.

Defined in

Mathlib.AlgebraicGeometry.Group.Affine

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRingCommRingCommRingBialgebraAlgebra