Module

Connected.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.GenericFiber.Connected

2 declarations indexed from sourceView source ↗

Module documentation

Connected finite-etale algebras over normal domains

A connected finite-etale algebra over an integrally closed domain has only one generic-fibre field component. The selected-component normalization is an idempotent factor of the algebra; connectedness makes that factor the whole algebra, and hence embeds the algebra into a field.

Imports3

Mathlib.RingTheory.Ideal.IdempotentFG
Mathlib.RingTheory.Spectrum.Prime.Topology
Nyll.EtaleFundamentalGroups.FiniteEtale.GenericFiber.Component

Imported by4

theorem

finiteEtale_isDomain_of_connectedSpace_primeSpectrum

L30 ↗

EtaleFundamentalGroups.finiteEtale_isDomain_of_connectedSpace_primeSpectrum

Documentation

A finite-etale algebra over an integrally closed domain whose prime spectrum is connected is a domain.

Source context 4 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open scoped TensorProduct
universe uR uT uK

Lean source · statement

theorem finiteEtale_isDomain_of_connectedSpace_primeSpectrum
    {R : Type uR} {T : Type uT} {K : Type uK}
    [CommRing R] [IsDomain R] [IsIntegrallyClosed R]
    [CommRing T] [Algebra R T] [Module.Finite R T] [Algebra.Etale R T]
    [Field K] [Algebra R K] [IsFractionRing R K]
    [ConnectedSpace (PrimeSpectrum T)] : IsDomain T

theorem

finiteEtale_isIntegrallyClosed_of_connectedSpace_primeSpectrum

L111 ↗

EtaleFundamentalGroups.finiteEtale_isIntegrallyClosed_of_connectedSpace_primeSpectrum