NYLL
Module

IdempotentQuotientFactor.lean

Nyll.SchemeTheory.RingTheory.IdempotentQuotientFactor
1 declaration indexed from sourceView source ↗

Module documentation

A quotient which is an open immersion is an algebra factor

For a surjective algebra map inducing an open immersion on spectra, the kernel is generated by an idempotent. The complementary idempotent gives a concrete product decomposition, with its first projection equal to the original map.

Imports5
  • Mathlib.Algebra.Algebra.Prod
  • Mathlib.Algebra.Ring.Idempotent
  • Mathlib.AlgebraicGeometry.Morphisms.OpenImmersion
  • Mathlib.RingTheory.Idempotents
  • Mathlib.RingTheory.Ideal.Quotient.Operations
Imported by2

Declarations

theorem

exists_prod_quotient_equiv_of_isOpenImmersion

L32 ↗
AlgHom.exists_prod_quotient_equiv_of_isOpenImmersion
Documentation

A surjective algebra map whose spectrum is an open immersion identifies the target with one factor of a product. Both projections of the constructed algebra equivalence are the specified quotient maps.

Source context 3 commands

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

@[expose] public section
universe u
namespace AlgHom
Lean source · statement
theorem exists_prod_quotient_equiv_of_isOpenImmersion
    {A R S : Type u} [CommRing A] [CommRing R] [CommRing S]
    [Algebra A R] [Algebra A S] (f : R →ₐ[A] S)
    (hf : Function.Surjective f)
    [AlgebraicGeometry.IsOpenImmersion
      (AlgebraicGeometry.Spec.map (CommRingCat.ofHom f.toRingHom))] :
    ∃ e : R, IsIdempotentElem e ∧ RingHom.ker f.toRingHom = Ideal.span {e} ∧
      ∃ E : R ≃ₐ[A] S × (R ⧸ Ideal.span {1 - e}),
        (∀ r : R, (E r).1 = f r) ∧
        (∀ r : R, (E r).2 = Ideal.Quotient.mk (Ideal.span {1 - e}) r)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.