Module

Algebra_isSmoothAt_of_isSmoothAt_fiber.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_isSmoothAt_of_isSmoothAt_fiber

2 declarations indexed from sourceView source ↗

Module documentation

Algebra is Smooth At of is Smooth At fiber

Imports2

Mathlib.RingTheory.Flat.Localization
Mathlib.RingTheory.Smooth.Fiber

Imported by2

theorem

includeRight_surjective_of_residueField

L30 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_isSmoothAt_of_isSmoothAt_fiber.PtwiseSmooth.includeRight_surjective_of_residueField

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_isSmoothAt_of_isSmoothAt_fiber
universe u
open TensorProduct
namespace PtwiseSmooth

Lean source · statement

theorem includeRight_surjective_of_residueField (Rp Sq : Type u) [CommRing Rp] [IsLocalRing Rp]
  [CommRing Sq]
    [Algebra Rp Sq] :
    Function.Surjective (Algebra.TensorProduct.includeRight :
      Sq →ₐ[Rp] IsLocalRing.ResidueField Rp ⊗[Rp] Sq)

theorem

isSmoothAt_of_isSmoothAt_fiber

L50 ↗

Algebra.isSmoothAt_of_isSmoothAt_fiber