Algebra.FormallyEtale.comp_bijective_of_isAdicComplete
Maps from a formally étale algebra to an adically complete algebra are uniquely determined by, and uniquely lift from, their reduction modulo the ideal of definition.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace Algebra.FormallyEtale
universe u v w
variable {R : Type u} {A : Type v} {S : Type w}
variable [CommRing R] [CommRing A] [CommRing S]
variable [Algebra R A] [Algebra R S]Lean source · statement
theorem comp_bijective_of_isAdicComplete [FormallyEtale R A]
(I : Ideal S) [IsAdicComplete I S] :
Function.Bijective
((Ideal.Quotient.mkₐ R I).comp :
(A →ₐ[R] S) → A →ₐ[R] S ⧸ I)