Theorems · Definition · algebraic geometry

CommAlgCat.FiniteEtale.ofHom

{R : Type u} →
  [inst : CommRing R] →
    {S T : Type v} →
      [inst_1 : CommRing S] →
        [inst_2 : CommRing T] →
          [inst_3 : Algebra R S] →
            [inst_4 : Algebra R T] →
              [inst_5 : Module.Finite R S] →
                [inst_6 : Algebra.Etale R S] →
                  [inst_7 : Module.Finite R T] →
                    [inst_8 : Algebra.Etale R T] →
                      (S →ₐ[R] T) → (CommAlgCat.FiniteEtale.of R S ⟶ CommAlgCat.FiniteEtale.of R T)

Construct a morphism in FiniteEtale R from an algebra map.

Defined in

Mathlib.RingTheory.Etale.Finite

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingCommRingCommRingAlgebraAlgebraModule.FiniteAlgebra.EtaleModule.FiniteAlgebra.Etale