Module

EtaleDominantQuotient.lean

Nyll.EtaleFundamentalGroups.Normalization.EtaleDominantQuotient

1 declaration indexed from sourceView source ↗

Module documentation

Dominant domain quotients of étale algebras over normal domains

A quotient of an étale algebra over a normal domain which is itself a domain and remains faithful over the base is an idempotent factor, hence étale. The generic fibre selects its primitive idempotent; smooth base change of integral closure descends that idempotent to the original algebra.

Imports3

Nyll.EtaleFundamentalGroups.FiniteEtale.GenericFiber.Component
Mathlib.RingTheory.Localization.FractionRing
Mathlib.RingTheory.TensorProduct.Maps

Imported by2

theorem

etale_of_surjective_of_domain_of_faithful

L32 ↗

EtaleFundamentalGroups.etale_of_surjective_of_domain_of_faithful

Documentation

A surjective map from an étale algebra over a normal domain to a domain which is faithful over the base realizes the target as an étale algebra. No finiteness hypothesis on the source as a module is needed.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
open Polynomial
universe uR uA uB

Lean source · statement

theorem etale_of_surjective_of_domain_of_faithful
    {R : Type uR} {A : Type uA} {B : Type uB}
    [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
    [CommRing A] [Algebra R A] [Algebra.Etale R A]
    [CommRing B] [IsDomain B] [Algebra R B] [FaithfulSMul R B]
    (φ : A →ₐ[R] B) (hφ : Function.Surjective φ) : Algebra.Etale R B

Module documentation

Dominant domain quotients of étale algebras over normal domains

Declarations

etale_of_surjective_of_domain_of_faithful