Module

EtaleSection.lean

Nyll.SchemeTheory.FiniteEtale.Algebra.EtaleSection

6 declarations indexed from sourceView source ↗

Module documentation

Étale sections over a quotient base

An algebra map from an étale algebra to a quotient of the base factors canonically through reduction by the extended ideal. The resulting map is surjective and induces an open immersion on spectra. Thus it supplies an actual finite open factor of the quotient fiber.

Imports8

Mathlib.Algebra.Algebra.Tower
Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
Mathlib.RingTheory.Etale.Basic
Mathlib.RingTheory.FinitePresentation
Mathlib.RingTheory.Ideal.IdempotentFG
Mathlib.RingTheory.Ideal.Over
Mathlib.RingTheory.Ideal.Quotient.Operations
Mathlib.RingTheory.TensorProduct.Quotient

Imported by5

theorem

isOpenImmersion_SpecMap_of_surjective_of_etale

L37 ↗

AlgHom.isOpenImmersion_SpecMap_of_surjective_of_etale

Documentation

A surjective map between étale algebras induces an open immersion. Its kernel is a finitely generated idempotent ideal.

Source context 4 commands

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

@[expose] public section
open AlgebraicGeometry
universe u v
namespace AlgHom

Lean source · statement

theorem isOpenImmersion_SpecMap_of_surjective_of_etale
    {R : Type v} {A B : Type u} [CommRing R] [CommRing A] [CommRing B]
    [Algebra R A] [Algebra R B] [Algebra.Etale R A] [Algebra.Etale R B]
    (f : A →ₐ[R] B) (hf : Function.Surjective f) :
    IsOpenImmersion (Spec.map (CommRingCat.ofHom f.toRingHom))

lemma

extendedIdeal_le_ker_quotientSection

L59 ↗

AlgHom.extendedIdeal_le_ker_quotientSection

Source context 6 commands

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

@[expose] public section
open AlgebraicGeometry
universe u v
namespace AlgHom
section QuotientSection
variable {R : Type u} {B : Type v} [CommRing R] [CommRing B] [Algebra R B]
    (I : Ideal R) (σ : B →ₐ[R] R ⧸ I)

Lean source · statement

lemma extendedIdeal_le_ker_quotientSection :
    I.map (algebraMap R B) ≤ RingHom.ker σ.toRingHom

def

quotientSection

L68 ↗

AlgHom.quotientSection

Documentation

The map over the quotient base induced by an algebra map to that quotient.

Source context 6 commands

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

@[expose] public section
open AlgebraicGeometry
universe u v
namespace AlgHom
section QuotientSection
variable {R : Type u} {B : Type v} [CommRing R] [CommRing B] [Algebra R B]
    (I : Ideal R) (σ : B →ₐ[R] R ⧸ I)

Lean source · statement

def quotientSection : B ⧸ I.map (algebraMap R B) →ₐ[R ⧸ I] R ⧸ I

theorem

quotientSection_mk

L74 ↗

AlgHom.quotientSection_mk

Source context 6 commands

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

@[expose] public section
open AlgebraicGeometry
universe u v
namespace AlgHom
section QuotientSection
variable {R : Type u} {B : Type v} [CommRing R] [CommRing B] [Algebra R B]
    (I : Ideal R) (σ : B →ₐ[R] R ⧸ I)

Lean source · statement

theorem quotientSection_mk (b : B) :
    quotientSection I σ (Ideal.Quotient.mk (I.map (algebraMap R B)) b) = σ b

theorem

quotientSection_surjective

L79 ↗

AlgHom.quotientSection_surjective

Documentation

A section to the quotient base is surjective because it fixes base scalars.

Source context 6 commands

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

@[expose] public section
open AlgebraicGeometry
universe u v
namespace AlgHom
section QuotientSection
variable {R : Type u} {B : Type v} [CommRing R] [CommRing B] [Algebra R B]
    (I : Ideal R) (σ : B →ₐ[R] R ⧸ I)

Lean source · statement

theorem quotientSection_surjective : Function.Surjective (quotientSection I σ)

theorem

isOpenImmersion_SpecMap_quotientSection

L88 ↗

AlgHom.isOpenImmersion_SpecMap_quotientSection

Documentation

A section of an étale algebra over a quotient base defines an open immersion into the quotient fiber. Its source is the base itself, hence is finite over it.

Source context 4 commands

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

@[expose] public section
open AlgebraicGeometry
universe u v
namespace AlgHom

Lean source · statement

theorem isOpenImmersion_SpecMap_quotientSection
    {R B : Type u} [CommRing R] [CommRing B] [Algebra R B] [Algebra.Etale R B]
    (I : Ideal R) (σ : B →ₐ[R] R ⧸ I) :
    IsOpenImmersion (Spec.map (CommRingCat.ofHom (quotientSection I σ).toRingHom))

Module documentation

Étale sections over a quotient base

Declarations

isOpenImmersion_SpecMap_of_surjective_of_etale

extendedIdeal_le_ker_quotientSection

quotientSection

quotientSection_mk

quotientSection_surjective

isOpenImmersion_SpecMap_quotientSection