Module

Algebra_FormallyEtale_of_formallySmooth_of_bijective_mapBaseChange.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Algebra_FormallyEtale_of_formallySmooth_of_bijective_mapBaseChange

3 declarations indexed from sourceView source ↗

Module documentation

Algebra Formally Etale of formally Smooth of bijective map Base Change

Imports2

Mathlib.RingTheory.Etale.Basic
Mathlib.RingTheory.Kaehler.JacobiZariski

Imported by2

theorem

subsingleton_kaehler_of_surjective

L39 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallyEtale_of_formallySmooth_of_bijective_mapBaseChange.R1NeronObjE1.subsingleton_kaehler_of_surjective

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallyEtale_of_formallySmooth_of_bijective_mapBaseChange
open _root_.KaehlerDifferential
open _root_.Algebra
open _root_.TensorProduct
open _root_.Algebra.TensorProduct
universe u
namespace R1NeronObjE1
section algebra
variable {R S T : Type*} [CommRing R] [CommRing S] [CommRing T]
  [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T]

Lean source · statement

theorem subsingleton_kaehler_of_surjective
    (h : Function.Surjective (KaehlerDifferential.mapBaseChange R S T)) :
    Subsingleton Ω[T⁄S]

theorem

formallyEtale_of_formallySmooth_of_bijective

L55 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Algebra_FormallyEtale_of_formallySmooth_of_bijective_mapBaseChange.R1NeronObjE1.formallyEtale_of_formallySmooth_of_bijective

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallyEtale_of_formallySmooth_of_bijective_mapBaseChange
open _root_.KaehlerDifferential
open _root_.Algebra
open _root_.TensorProduct
open _root_.Algebra.TensorProduct
universe u
namespace R1NeronObjE1
section algebra
variable {R S T : Type*} [CommRing R] [CommRing S] [CommRing T]
  [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T]

Lean source · statement

theorem formallyEtale_of_formallySmooth_of_bijective [Algebra.FormallySmooth R T]
    (h : Function.Bijective (KaehlerDifferential.mapBaseChange R S T)) :
    Algebra.FormallyEtale S T

theorem

of_formallySmooth_of_bijective_mapBaseChange

L84 ↗

Algebra.FormallyEtale.of_formallySmooth_of_bijective_mapBaseChange

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Algebra_FormallyEtale_of_formallySmooth_of_bijective_mapBaseChange
open _root_.KaehlerDifferential
open _root_.Algebra
open _root_.TensorProduct
open _root_.Algebra.TensorProduct
universe u

Lean source · statement

theorem _root_.Algebra.FormallyEtale.of_formallySmooth_of_bijective_mapBaseChange
    {R S T : Type*} [CommRing R] [CommRing S] [CommRing T]
    [Algebra R S] [Algebra R T] [Algebra S T] [IsScalarTower R S T]
    [Algebra.FormallySmooth R T]
    (h : Function.Bijective (KaehlerDifferential.mapBaseChange R S T)) :
    Algebra.FormallyEtale S T

Module documentation

Algebra Formally Etale of formally Smooth of bijective map Base Change

Declarations

subsingleton_kaehler_of_surjective

formallyEtale_of_formallySmooth_of_bijective

of_formallySmooth_of_bijective_mapBaseChange