Algebra.FiniteEtale.bijective_algebraMap_of_quotientSection
A finite étale algebra is the base algebra if it has a section over a Jacobson quotient and every element of its reduction is a base scalar.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
open scoped TensorProduct
universe u v
namespace Algebra.FiniteEtaleLean source · statement
theorem bijective_algebraMap_of_quotientSection
{R : Type u} {A : Type v} [CommRing R] [CommRing A] [Algebra R A]
[Module.Finite R A] [Algebra.Etale R A]
(I : Ideal R) (hI : I ≤ Ideal.jacobson ⊥) (σ : A →ₐ[R] R ⧸ I)
(hsurj : Function.Surjective
(algebraMap (R ⧸ I) (A ⧸ I.map (algebraMap R A)))) :
Function.Bijective (algebraMap R A)