Algebra.FiniteEtale.bijective_of_baseChange_quotient
A map of finite étale algebras that becomes bijective after reduction by a Jacobson ideal was already bijective.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
open scoped TensorProduct
universe u v w
namespace Algebra.FiniteEtaleLean source · statement
theorem bijective_of_baseChange_quotient
{R : Type u} {A : Type v} {B : Type w}
[CommRing R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
[Module.Finite R A] [Algebra.Etale R A]
[Module.Finite R B] [Algebra.Etale R B]
(I : Ideal R) (hI : I ≤ Ideal.jacobson ⊥) (f : A →ₐ[R] B)
(hf : Function.Bijective
(Algebra.TensorProduct.map (.id (R ⧸ I) (R ⧸ I)) f)) :
Function.Bijective f