NYLL
Module

RelativeGroupLaw_etale_schemeNsmul_of_isUnit_of_smoothOfRelativeDimension.lean

Nyll.AlgebraicCurves.Geometry.AbelianSchemes.Theorems.RelativeGroupLaw_etale_schemeNsmul_of_isUnit_of_smoothOfRelativeDimension
11 declarations indexed from sourceView source ↗

Module documentation

Etaleness from smoothness of equal relative dimension

Formal unramifiedness and smoothness of the two structure maps imply etaleness. This criterion applies to multiplication maps of a smooth relative group law.

Imports8
Imported by4

Declarations

theorem

subsingleton_kaehler_of_surjective

L48 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_schemeNsmul_of_isUnit_of_smoothOfRelativeDimension.R1NeronObjE4.subsingleton_kaehler_of_surjective
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_schemeNsmul_of_isUnit_of_smoothOfRelativeDimension
open _root_.KaehlerDifferential
open _root_.Algebra
open _root_.TensorProduct
open _root_.Algebra.TensorProduct
universe u
namespace R1NeronObjE4
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

L64 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_schemeNsmul_of_isUnit_of_smoothOfRelativeDimension.R1NeronObjE4.formallyEtale_of_formallySmooth_of_bijective
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_schemeNsmul_of_isUnit_of_smoothOfRelativeDimension
open _root_.KaehlerDifferential
open _root_.Algebra
open _root_.TensorProduct
open _root_.Algebra.TensorProduct
universe u
namespace R1NeronObjE4
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

mapBaseChange_surjective_of_formallyUnramified

L89 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_schemeNsmul_of_isUnit_of_smoothOfRelativeDimension.R1NeronObjE4.mapBaseChange_surjective_of_formallyUnramified
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_schemeNsmul_of_isUnit_of_smoothOfRelativeDimension
open _root_.KaehlerDifferential
open _root_.Algebra
open _root_.TensorProduct
open _root_.Algebra.TensorProduct
universe u
namespace R1NeronObjE4
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 mapBaseChange_surjective_of_formallyUnramified [Algebra.FormallyUnramified S T] :
    Function.Surjective (KaehlerDifferential.mapBaseChange R S T)
theorem

bijective_of_surjective_of_finrank_eq

L96 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_schemeNsmul_of_isUnit_of_smoothOfRelativeDimension.R1NeronObjE4.bijective_of_surjective_of_finrank_eq
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_schemeNsmul_of_isUnit_of_smoothOfRelativeDimension
open _root_.KaehlerDifferential
open _root_.Algebra
open _root_.TensorProduct
open _root_.Algebra.TensorProduct
universe u
namespace R1NeronObjE4
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 bijective_of_surjective_of_finrank_eq {A : Type*} [CommRing A] [Nontrivial A]
    {M N : Type*} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N]
    [Module.Free A M] [Module.Finite A M] [Module.Free A N] [Module.Finite A N]
    (f : M →ₗ[A] N) (hf : Function.Surjective f)
    (hrank : Module.finrank A M = Module.finrank A N) : Function.Bijective f
theorem

formallyEtale_of_formallyUnramified_of_isStandardSmoothOfRelativeDimension

L104 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_schemeNsmul_of_isUnit_of_smoothOfRelativeDimension.R1NeronObjE4.formallyEtale_of_formallyUnramified_of_isStandardSmoothOfRelativeDimension
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_schemeNsmul_of_isUnit_of_smoothOfRelativeDimension
open _root_.KaehlerDifferential
open _root_.Algebra
open _root_.TensorProduct
open _root_.Algebra.TensorProduct
universe u
namespace R1NeronObjE4
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_formallyUnramified_of_isStandardSmoothOfRelativeDimension (n : ℕ)
    [Algebra.IsStandardSmoothOfRelativeDimension n R S]
    [Algebra.IsStandardSmoothOfRelativeDimension n R T]
    [Algebra.FormallyUnramified S T] :
    Algebra.FormallyEtale S T
theorem

etale_of_formallyUnramified_of_isStandardSmoothOfRelativeDimension

L129 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_schemeNsmul_of_isUnit_of_smoothOfRelativeDimension.R1NeronObjE4.etale_of_formallyUnramified_of_isStandardSmoothOfRelativeDimension
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_schemeNsmul_of_isUnit_of_smoothOfRelativeDimension
open _root_.KaehlerDifferential
open _root_.Algebra
open _root_.TensorProduct
open _root_.Algebra.TensorProduct
universe u
namespace R1NeronObjE4
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 etale_of_formallyUnramified_of_isStandardSmoothOfRelativeDimension (n : ℕ)
    [Algebra.IsStandardSmoothOfRelativeDimension n R S]
    [Algebra.IsStandardSmoothOfRelativeDimension n R T]
    [Algebra.FormallyUnramified S T] :
    Algebra.Etale S T
theorem

ringHom_etale_of_formallyUnramified_of_isStandardSmoothOfRelativeDimension

L148 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_schemeNsmul_of_isUnit_of_smoothOfRelativeDimension.R1NeronObjE4.ringHom_etale_of_formallyUnramified_of_isStandardSmoothOfRelativeDimension
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_schemeNsmul_of_isUnit_of_smoothOfRelativeDimension
open _root_.KaehlerDifferential
open _root_.Algebra
open _root_.TensorProduct
open _root_.Algebra.TensorProduct
universe u
namespace R1NeronObjE4
section ringHom
Lean source · statement
theorem ringHom_etale_of_formallyUnramified_of_isStandardSmoothOfRelativeDimension
    {R S T : Type*} [CommRing R] [CommRing S] [CommRing T] (n : ℕ)
    (φ : R →+* S) (ψ : S →+* T)
    (hφ : φ.IsStandardSmoothOfRelativeDimension n)
    (hψφ : (ψ.comp φ).IsStandardSmoothOfRelativeDimension n)
    (hψ : ψ.FormallyUnramified) : ψ.Etale
theorem

ringHom_etale_of_formallyUnramified_of_locally_isStandardSmoothOfRelativeDimension

L158 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_schemeNsmul_of_isUnit_of_smoothOfRelativeDimension.R1NeronObjE4.ringHom_etale_of_formallyUnramified_of_locally_isStandardSmoothOfRelativeDimension
Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_schemeNsmul_of_isUnit_of_smoothOfRelativeDimension
open _root_.KaehlerDifferential
open _root_.Algebra
open _root_.TensorProduct
open _root_.Algebra.TensorProduct
universe u
namespace R1NeronObjE4
section ringHom
Lean source · statement
theorem ringHom_etale_of_formallyUnramified_of_locally_isStandardSmoothOfRelativeDimension
    {R S T : Type u} [CommRing R] [CommRing S] [CommRing T] (n : ℕ)
    (φ : R →+* S) (ψ : S →+* T)
    (hφ : RingHom.Locally (RingHom.IsStandardSmoothOfRelativeDimension n) φ)
    (hψφ : RingHom.Locally (RingHom.IsStandardSmoothOfRelativeDimension n) (ψ.comp φ))
    (hψ : ψ.FormallyUnramified) : ψ.Etale
theorem

scheme_etale_of_formallyUnramified_of_smoothOfRelativeDimension

L234 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_schemeNsmul_of_isUnit_of_smoothOfRelativeDimension.R1NeronObjE4.scheme_etale_of_formallyUnramified_of_smoothOfRelativeDimension
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_schemeNsmul_of_isUnit_of_smoothOfRelativeDimension
open _root_.KaehlerDifferential
open _root_.Algebra
open _root_.TensorProduct
open _root_.Algebra.TensorProduct
universe u
namespace R1NeronObjE4
section scheme
open AlgebraicGeometry CategoryTheory
Lean source · statement
theorem scheme_etale_of_formallyUnramified_of_smoothOfRelativeDimension
    {X Y Z : Scheme.{u}} (n : ℕ) {f : X ⟶ Y} {g : Y ⟶ Z}
    (h1 : SmoothOfRelativeDimension n (f ≫ g)) (h2 : SmoothOfRelativeDimension n g)
    (h3 : FormallyUnramified f) : Etale f
theorem

groupLaw_etale_schemeNsmul

L292 ↗
AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs.RelativeGroupLaw_etale_schemeNsmul_of_isUnit_of_smoothOfRelativeDimension.R1NeronObjE4.groupLaw_etale_schemeNsmul
Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
namespace RelativeGroupLaw_etale_schemeNsmul_of_isUnit_of_smoothOfRelativeDimension
open _root_.KaehlerDifferential
open _root_.Algebra
open _root_.TensorProduct
open _root_.Algebra.TensorProduct
universe u
namespace R1NeronObjE4
section groupLaw
open AlgebraicGeometry CategoryTheory NeronModelInfra GoodReductionJacobian
Lean source · statement
theorem groupLaw_etale_schemeNsmul
    {R : Type u} [CommRing R] [IsLocalRing R] {A : Scheme.{u}}
    {f : A ⟶ Spec (CommRingCat.of R)} (G : RelativeGroupLaw R f)
    (hcomm : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (x y : SchemeHomOver t f),
      G.mul t x y = G.mul t y x)
    (d : ℕ) [SmoothOfRelativeDimension d f] (n : ℕ) (hn : IsUnit (n : R)) :
    Etale (G.schemeNsmul n)
theorem

etale_schemeNsmul_of_isUnit_of_smoothOfRelativeDimension

L325 ↗
GoodReductionJacobian.RelativeGroupLaw.etale_schemeNsmul_of_isUnit_of_smoothOfRelativeDimension
Source context 8 commands

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

section ProofImplementation
universe u
open AlgebraicCurves.Geometry.AbelianSchemes.Theorems.Proofs
open RelativeGroupLaw_etale_schemeNsmul_of_isUnit_of_smoothOfRelativeDimension
open R1NeronObjE4
open CategoryTheory CategoryTheory.MonoidalCategory AlgebraicGeometry
namespace GoodReductionJacobian.RelativeGroupLaw
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry NeronModelInfra GoodReductionJacobian
Lean source · statement
theorem etale_schemeNsmul_of_isUnit_of_smoothOfRelativeDimension
    {R : Type u} [CommRing R] [IsLocalRing R] {A : Scheme.{u}} {f : A ⟶ Spec (CommRingCat.of R)}
    (G : RelativeGroupLaw R f)
    (hcomm : ∀ {T : Scheme.{u}} (t : T ⟶ Spec (CommRingCat.of R)) (x y : SchemeHomOver t f),
      G.mul t x y = G.mul t y x)
    (d : ℕ) [SmoothOfRelativeDimension d f]
    (n : ℕ) (hn : IsUnit (n : R)) :
    Etale (G.schemeNsmul n)

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