NYLL
Module

Smooth.lean

Nyll.SchemeTheory.Pi1.Morphisms.Smooth
2 declarations indexed from sourceView source ↗

Module documentation

Localization criteria for smooth ring maps

Smoothness satisfies the localization-span criterion. Bijective algebra maps give formally smooth algebras, and fraction fields of multivariate polynomial algebras are formally smooth.

Imports2
  • Mathlib.RingTheory.RingHom.Smooth
  • Mathlib.RingTheory.TotallySplit
Imported by2

Declarations

lemma

of_bijective_algebraMap

L38 ↗
Algebra.FormallySmooth.of_bijective_algebraMap
Source context 3 commands

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

@[expose] public section
open TensorProduct
universe u
Lean source · statement
lemma Algebra.FormallySmooth.of_bijective_algebraMap {R S : Type u} [CommRing R] [CommRing S]
    [Algebra R S] (h : Function.Bijective (algebraMap R S)) :
    Algebra.FormallySmooth R S
instance

(anonymous instance)

L46 ↗
Source context 4 commands

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

@[expose] public section
open TensorProduct
universe u
namespace Algebra
Lean source · statement
instance {k ι : Type u} [Field k] : FormallySmooth k (FractionRing (MvPolynomial ι k))

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.