Module

IdempotentFactor.lean

Nyll.SchemeTheory.FiniteEtale.Algebra.IdempotentFactor

1 declaration indexed from sourceView source ↗

Module documentation

Étale idempotent factors

The quotient imposing e = 1 for an idempotent e is localization at e. Consequently, an idempotent factor of an étale algebra is again étale over the original base, with the canonical quotient algebra structure.

Imports3

Mathlib.RingTheory.Etale.Basic
Mathlib.RingTheory.Ideal.Quotient.Operations
Mathlib.RingTheory.Localization.Away.Basic

Imported by6

theorem

quotient_one_sub_of_isIdempotentElem

L28 ↗

Algebra.Etale.quotient_one_sub_of_isIdempotentElem

Documentation

The factor on which an idempotent becomes 1 is étale over the base.

Source context 3 commands

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

@[expose] public section
universe u v
namespace Algebra.Etale

Lean source · statement

theorem quotient_one_sub_of_isIdempotentElem
    {R : Type u} {B : Type v} [CommRing R] [CommRing B] [Algebra R B]
    [Algebra.Etale R B] (e : B) (he : IsIdempotentElem e) :
    Algebra.Etale R (B ⧸ Ideal.span {1 - e})

Module documentation

Étale idempotent factors

Declarations

quotient_one_sub_of_isIdempotentElem