Theorems · Theorem · commutative algebra

Algebra.FormallyEtale.iff_comp_bijective

∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A],
  Algebra.FormallyEtale R A ↔
    ∀ ⦃B : Type (max u v)⦄ [inst_3 : CommRing B] [inst_4 : Algebra R B] (I : Ideal B),
      I ^ 2 = ⊥ → Function.Bijective (Ideal.Quotient.mkₐ R I).comp

An R-algebra A is formally etale iff "for every R-algebra B, every square-zero ideal I : Ideal B and f : A →ₐ[R] B ⧸ I, there exists a unique lift A →ₐ[R] B".

Defined in

Mathlib.RingTheory.Etale.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebra