NYLL
Module

SectionFactor.lean

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

Module documentation

Splitting off an étale section

An algebra section of a finite étale algebra cuts out an idempotent factor isomorphic to the base. The complementary factor is an actual quotient by the complementary idempotent, and remains finite étale. The product isomorphism has the prescribed section as its first coordinate.

Imports6
Imported by1

Declarations

theorem

exists_prod_of_section

L35 ↗
Algebra.Etale.exists_prod_of_section
Documentation

A section splits a finite étale algebra as the base times an actual finite étale complementary factor, with the specified first projection.

Source context 4 commands

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

@[expose] public noncomputable section
open AlgebraicGeometry
universe u
namespace Algebra.Etale
Lean source · statement
theorem exists_prod_of_section
    {R C : Type u} [CommRing R] [CommRing C] [Algebra R C]
    [Module.Finite R C] [Algebra.Etale R C] (σ : C →ₐ[R] R) :
    ∃ (D : Type u) (_ : CommRing D) (_ : Algebra R D),
      Module.Finite R D ∧ Algebra.Etale R D ∧
      ∃ E : C ≃ₐ[R] R × D, ∀ c : C, (E c).1 = σ c

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