Module

Basic.lean

Nyll.SchemeTheory.Pi1.FiniteEtale.Algebra.Basic

9 declarations indexed from sourceView source ↗

Module documentation

Finite etale algebras

The finite etale property combines etaleness with module finiteness. The accompanying lemmas transport this property across algebra equivalences and localizations.

Imports5

Mathlib.Algebra.Lie.OfAssociative
Mathlib.RingTheory.RingHom.Etale
Mathlib.RingTheory.RingHom.Finite
Mathlib.RingTheory.TotallySplit
Mathlib.RingTheory.Finiteness.Defs

Imported by2

class

FiniteEtale

L41 ↗

Algebra.FiniteEtale

Documentation

An R-algebra is finite étale when it is étale and finite as an R-module.

Source context 3 commands

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

@[expose] public section
open TensorProduct
universe u

Lean source · full declaration

class Algebra.FiniteEtale (R S : Type u) [CommRing R] [CommRing S] [Algebra R S] : Prop
  extends Algebra.Etale R S, Module.Finite R S

lemma

of_equiv

L44 ↗

Algebra.FiniteEtale.of_equiv

Source context 3 commands

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

@[expose] public section
open TensorProduct
universe u

Lean source · statement

lemma Algebra.FiniteEtale.of_equiv {R S S' : Type u} [CommRing R] [CommRing S] [Algebra R S]
    [Algebra.FiniteEtale R S] [CommRing S'] [Algebra R S'] (e : S ≃ₐ[R] S') :
    Algebra.FiniteEtale R S'

instance

(anonymous instance)

L51 ↗

Source context 3 commands

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

@[expose] public section
open TensorProduct
universe u

Lean source · full declaration

instance (R S : Type u) [CommRing R] [CommRing S] [Algebra R S]
    [Algebra.IsFiniteSplit R S] : Algebra.FiniteEtale R S where

lemma

of_exists_of_isPrime

L58 ↗

RingHom.OfLocalizationSpan.of_exists_of_isPrime

Source context 5 commands

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

@[expose] public section
open TensorProduct
universe u
section
variable (P : ∀ {R S : Type u} [CommRing R] [CommRing S], (R →+* S) → Prop)

Lean source · statement

lemma RingHom.OfLocalizationSpan.of_exists_of_isPrime
    (hP : RingHom.OfLocalizationSpan P)
    {R S : Type u}
    [CommRing R] [CommRing S] (f : R →+* S)
    (H : ∀ (p : Ideal R) [p.IsPrime], ∃ r ∉ p, P (Localization.awayMap f r)) :
    P f

lemma

tmul

L79 ↗

IsUnit.tmul

Source context 5 commands

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

@[expose] public section
open TensorProduct
universe u
section
variable (P : ∀ {R S : Type u} [CommRing R] [CommRing S], (R →+* S) → Prop)

Lean source · statement

lemma IsUnit.tmul {R S T : Type*} [CommRing R] [CommRing S]
    [CommRing T] [Algebra R T] [Algebra R S] {s : S} {t : T} (hs : IsUnit s) (ht : IsUnit t) :
    IsUnit (s ⊗ₜ[R] t)

lemma

of_exists_of_isPrime'

L88 ↗

RingHom.OfLocalizationSpan.of_exists_of_isPrime'

Source context 5 commands

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

@[expose] public section
open TensorProduct
universe u
section
variable (P : ∀ {R S : Type u} [CommRing R] [CommRing S], (R →+* S) → Prop)

Lean source · statement

lemma RingHom.OfLocalizationSpan.of_exists_of_isPrime'
    {P : ∀ {R S : Type u} [CommRing R] [CommRing S], (R →+* S) → Prop}
    (hP : RingHom.OfLocalizationSpan P)
    (hPi : RingHom.RespectsIso P)
    {R S : Type u} [CommRing R] [CommRing S] [Algebra R S]
    (H : ∀ (p : Ideal R) [p.IsPrime], ∃ r ∉ p,
      P (algebraMap (Localization.Away r) (Localization.Away r ⊗[R] S))) :
    P (algebraMap R S)

lemma

of_exists_of_isPrime

L119 ↗

Algebra.Etale.of_exists_of_isPrime

Source context 5 commands

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

@[expose] public section
open TensorProduct
universe u
section
variable (P : ∀ {R S : Type u} [CommRing R] [CommRing S], (R →+* S) → Prop)

Lean source · statement

lemma Algebra.Etale.of_exists_of_isPrime {R S : Type u} [CommRing R] [CommRing S]
    [Algebra R S] (H : ∀ (p : Ideal R) [p.IsPrime], ∃ r ∉ p,
      Algebra.Etale (Localization.Away r) (Localization.Away r ⊗[R] S)) : Algebra.Etale R S

lemma

of_exists_of_isPrime

L129 ↗

Module.Finite.of_exists_of_isPrime

Source context 5 commands

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

@[expose] public section
open TensorProduct
universe u
section
variable (P : ∀ {R S : Type u} [CommRing R] [CommRing S], (R →+* S) → Prop)

Lean source · statement

lemma Module.Finite.of_exists_of_isPrime {R S : Type u} [CommRing R] [CommRing S]
    [Algebra R S] (H : ∀ (p : Ideal R) [p.IsPrime], ∃ r ∉ p,
      Module.Finite (Localization.Away r) (Localization.Away r ⊗[R] S)) : Module.Finite R S

lemma

of_exists_of_isPrime

L140 ↗

Algebra.FiniteEtale.of_exists_of_isPrime

Source context 5 commands

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

@[expose] public section
open TensorProduct
universe u
section
variable (P : ∀ {R S : Type u} [CommRing R] [CommRing S], (R →+* S) → Prop)

Lean source · statement

lemma Algebra.FiniteEtale.of_exists_of_isPrime {R S : Type u} [CommRing R] [CommRing S]
    [Algebra R S] (H : ∀ (p : Ideal R) [p.IsPrime], ∃ r ∉ p,
      Algebra.FiniteEtale (Localization.Away r) (Localization.Away r ⊗[R] S)) :
    Algebra.FiniteEtale R S

Module documentation

Finite etale algebras

Declarations