RingHom.formallySmooth_and_formallyUnramified_eval2RingHom_of_maximalIdeal_eq_span_pair
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace RingHom_formallySmooth_and_formallyUnramified_eval2RingHom_of_maximalIdeal_eq_span_pair
open IsLocalRing
open _root_.RingHom
(existsUnique_eq_smul_kaehlerDifferential_D_of_formallySmooth_of_maximalIdeal_eq_span_pair) inLean source · statement
theorem
_root_.RingHom.formallySmooth_and_formallyUnramified_eval2RingHom_of_maximalIdeal_eq_span_pair
{A : Type} [CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
(ϖ : A) (hϖ : maximalIdeal A = Ideal.span {ϖ})
{S : Type} [CommRing S] [IsDomain S] [IsLocalRing S]
(i : A →+* S) (hi : i.FormallySmooth) (hif : i.EssFiniteType)
(hres : Function.Surjective ((IsLocalRing.residue S).comp i))
(t : S) (hm : maximalIdeal S = Ideal.span {i ϖ, t}) (ht : t ∉ Ideal.span {i ϖ}) :
(Polynomial.eval₂RingHom i t).FormallySmooth ∧ (Polynomial.eval₂RingHom i t).FormallyUnramified
∧
(Polynomial.eval₂RingHom i t).EssFiniteType