NYLL
Module

HenselianEtaleMapLift.lean

Nyll.SchemeTheory.FiniteEtale.Algebra.HenselianEtaleMapLift
1 declaration indexed from sourceView source ↗

Module documentation

Lifting pointed étale maps into a Henselian target

An étale algebra over A need not be an algebra over the target S. Base change to S and the native AlgHom.liftEquiv reduce existence to the existing Henselian section theorem. The existing Jacobson rigidity theorem supplies uniqueness over A directly. No module-finiteness or comparison map is assumed.

This is the affine pointed-lifting supplier for maps from the constructed geometric stalk into an actual strictly henselian local target.

Imports6
Imported by2

Declarations

theorem

bijective_comp_quotient_of_henselian_target

L39 ↗
Algebra.Etale.bijective_comp_quotient_of_henselian_target
Documentation

Reduction modulo a Henselian ideal in the target gives a bijection on maps out of every étale A-algebra. The source and target rings share the ambient universe used by the native Henselian section theorem; the base algebra A may have an independent universe.

Source context 4 commands

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

noncomputable section
open scoped TensorProduct
namespace Algebra.Etale
universe u v
Lean source · statement
theorem bijective_comp_quotient_of_henselian_target
    {A : Type u} {B S : Type v}
    [CommRing A] [CommRing B] [CommRing S] [Algebra A B] [Algebra A S]
    [Algebra.Etale A B] (I : Ideal S) [HenselianRing S I] :
    Function.Bijective
      ((Ideal.Quotient.mkₐ A I).comp : (B →ₐ[A] S) → B →ₐ[A] S ⧸ I)

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