Nyll.SchemeTheory.RingTheory.OpenImmersionFiniteFactor

Module documentation

Extracting a finite quotient factor inside an open immersion

A finite open factor of a closed fiber of an affine open immersion is an actual factor of the target closed fiber. Its defining idempotent has a representative whose principal open lies in the image of the immersion. Localizing at that representative makes the original algebra map bijective.

theorem

exists_quotient_factor_and_awayMap_bijective

L37 ↗

AlgHom.exists_quotient_factor_and_awayMap_bijective

Documentation

A finite open quotient-fiber factor extends across an affine open immersion, and a representative of its unit makes the original map an isomorphism after principal localization.

Source context 4 commands

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

@[expose] public section
open CategoryTheory AlgebraicGeometry TopologicalSpace
universe u
namespace AlgHom

Lean source · statement

theorem exists_quotient_factor_and_awayMap_bijective
    {R A B D : Type u} [CommRing R] [CommRing A] [CommRing B] [CommRing D]
    [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (I : Ideal R)
    [IsOpenImmersion (Spec.map (CommRingCat.ofHom f.toRingHom))]
    [Algebra (R ⧸ I) D] [Module.Finite (R ⧸ I) D]
    (p : B ⧸ I.map (algebraMap R B) →ₐ[R ⧸ I] D)
    [IsOpenImmersion (Spec.map (CommRingCat.ofHom p.toRingHom))] :
    ∃ e : A ⧸ I.map (algebraMap R A), IsIdempotentElem e ∧
      ∃ E : (A ⧸ I.map (algebraMap R A)) ≃ₐ[R ⧸ I]
          D × ((A ⧸ I.map (algebraMap R A)) ⧸ Ideal.span {1 - e}),
        (∀ x, (E x).1 = p (f.quotientBaseChange I x)) ∧
        (∀ x, (E x).2 = Ideal.Quotient.mk (Ideal.span {1 - e}) x) ∧
        ∃ g : A, Ideal.Quotient.mk (I.map (algebraMap R A)) g = 1 - e ∧
          E (Ideal.Quotient.mk (I.map (algebraMap R A)) g) = (1, 0) ∧
          Function.Bijective (Localization.awayMap f.toRingHom g)

Module documentation

Extracting a finite quotient factor inside an open immersion

Declarations

exists_quotient_factor_and_awayMap_bijective