Module

CyclicIdempotentFactor.lean

Nyll.SchemeTheory.RingTheory.CyclicIdempotentFactor

1 declaration indexed from sourceView source ↗

Module documentation

The special fiber of a cyclic idempotent factor

If multiplication by the reduction of e has cyclic image, imposing e = 1 makes the resulting special fiber generated by its unit over the quotient base. Thus its canonical algebra map from the quotient base is surjective. No idempotence or finiteness assumption is needed for this implication.

Imports5

Nyll.SchemeTheory.RingTheory.QuotientBaseChange
Mathlib.Algebra.Algebra.Tower
Mathlib.RingTheory.Ideal.Over
Mathlib.RingTheory.Ideal.Quotient.Operations
Mathlib.RingTheory.Ideal.Span

Imported by3

theorem

surjective_algebraMap_quotient_idempotentFactor_of_cyclic

L32 ↗

Algebra.surjective_algebraMap_quotient_idempotentFactor_of_cyclic

Documentation

A cyclic quotient factor is a quotient of the base after imposing e = 1. The map in the conclusion is the canonical algebra map.

Source context 3 commands

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

@[expose] public section
universe u v
namespace Algebra

Lean source · statement

theorem surjective_algebraMap_quotient_idempotentFactor_of_cyclic
    {R : Type u} {C : Type v} [CommRing R] [CommRing C] [Algebra R C]
    (I : Ideal R) (e : C)
    (hcyc : ∀ x : C ⧸ I.map (algebraMap R C), ∃ r : R,
      Ideal.Quotient.mk (I.map (algebraMap R C)) e * x =
        r • Ideal.Quotient.mk (I.map (algebraMap R C)) e) :
    Function.Surjective (algebraMap (R ⧸ I)
      ((C ⧸ Ideal.span {1 - e}) ⧸
        I.map (algebraMap R (C ⧸ Ideal.span {1 - e}))))

Module documentation

The special fiber of a cyclic idempotent factor

Declarations

surjective_algebraMap_quotient_idempotentFactor_of_cyclic