Module

Algebra_FormallySmooth_of_maximalIdeal_eq_span_of_isSeparable_residueField.lean

Nyll.AlgebraicCurves.Foundations.CommutativeAlgebra.Algebra_FormallySmooth_of_maximalIdeal_eq_span_of_isSeparable_residueField

1 declaration indexed from sourceView source ↗

Module documentation

Algebra Formally Smooth of maximal Ideal eq span of is Separable residue Field

Imports8

Mathlib.RingTheory.Smooth.Fiber
Mathlib.RingTheory.Unramified.LocalRing
Mathlib.RingTheory.Flat.TorsionFree
Mathlib.RingTheory.LocalRing.ResidueField.Instances
Mathlib.RingTheory.EssentialFiniteness
Mathlib.RingTheory.FinitePresentation
Mathlib.RingTheory.Ideal.Quotient.Operations
Mathlib.FieldTheory.Minpoly.Field

Imported by2

theorem

of_maximalIdeal_eq_span_of_isSeparable_residueField

L37 ↗

Algebra.FormallySmooth.of_maximalIdeal_eq_span_of_isSeparable_residueField

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs
namespace Algebra_FormallySmooth_of_maximalIdeal_eq_span_of_isSeparable_residueField
universe u v
open IsLocalRing Polynomial
attribute [local instance] Ideal.Quotient.field

Lean source · statement

theorem _root_.Algebra.FormallySmooth.of_maximalIdeal_eq_span_of_isSeparable_residueField
    (K₀ : Type u) [Field K₀] (𝒪 : Type v) [CommRing 𝒪] [IsLocalRing 𝒪] [IsDomain 𝒪]
      [IsNoetherianRing 𝒪]
    [Algebra K₀ 𝒪] [Algebra.EssFiniteType K₀ 𝒪]
    (u : 𝒪) (hu0 : u ≠ 0) (hu : maximalIdeal 𝒪 = Ideal.span {u})
    [Algebra.IsAlgebraic K₀ (ResidueField 𝒪)] [Algebra.IsSeparable K₀ (ResidueField 𝒪)] :
    Algebra.FormallySmooth K₀ 𝒪

Module documentation

Algebra Formally Smooth of maximal Ideal eq span of is Separable residue Field

Declarations

of_maximalIdeal_eq_span_of_isSeparable_residueField