Module

Equalizer.lean

Nyll.SchemeTheory.Pi1.FiniteEtale.Algebra.Equalizer

21 declarations indexed from sourceView source ↗

Module documentation

Equalizers of finite split algebras

Equalizers of maps between finite products are described by function coequalizers. Localization provides covers on which finite étale maps have these split presentations.

Imports5

Mathlib.Algebra.Group.Basic
Mathlib.Algebra.Group.Idempotent
Mathlib.Logic.Function.Coequalizer
Mathlib.RingTheory.Finiteness.ModuleFinitePresentation
Nyll.SchemeTheory.Pi1.FiniteEtale.Algebra.Descent

Imported by5

lemma

exists_cover_eq_of_eq

L45 ↗

AlgHom.exists_cover_eq_of_eq

Source context 6 commands

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

@[expose] public section
attribute [local instance] Module.FinitePresentation.of_finite_of_finitePresentation
open TensorProduct
universe u v
section
open Localization in

Lean source · statement

lemma AlgHom.exists_cover_eq_of_eq {R A B : Type*} [CommRing R] (S : Submonoid R)
    [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
    [Module.Finite R A]
    (Rₚ : Type*) (Aₚ Bₚ : Type u) [CommRing Rₚ] [CommRing Aₚ] [CommRing Bₚ]
    [Algebra R Rₚ] [Algebra R Aₚ] [Algebra R Bₚ] [Algebra Rₚ Aₚ] [Algebra Rₚ Bₚ]
    [Algebra A Aₚ] [Algebra B Bₚ]
    [IsScalarTower R A Aₚ] [IsScalarTower R B Bₚ] [IsScalarTower R Rₚ Aₚ] [IsScalarTower R Rₚ Bₚ]
    [IsLocalization S Rₚ] [IsLocalization (Algebra.algebraMapSubmonoid A S) Aₚ]
    [IsLocalization (Algebra.algebraMapSubmonoid B S) Bₚ]
    (f g : A →ₐ[R] B) (hf : IsLocalization.mapₐ S Rₚ Aₚ Bₚ f = IsLocalization.mapₐ S Rₚ Aₚ Bₚ g) :
    ∃ (r : S),
      Algebra.TensorProduct.map (.id (Away r.val) (Away r.val)) f =
        Algebra.TensorProduct.map (.id (Away r.val) (Away r.val)) g

def

equalizerCongr

L90 ↗

AlgHom.equalizerCongr

Documentation

Transports equalizers along algebra equivalences that intertwine both defining maps.

Source context 5 commands

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

@[expose] public section
attribute [local instance] Module.FinitePresentation.of_finite_of_finitePresentation
open TensorProduct
universe u v
section Equalizer

Lean source · statement

def AlgHom.equalizerCongr {R A A' B B' : Type*} [CommSemiring R]
    [Semiring A] [Semiring A'] [Semiring B] [Semiring B']
    [Algebra R A] [Algebra R A'] [Algebra R B] [Algebra R B']
    (eA : A ≃ₐ[R] A') (eB : B ≃ₐ[R] B')
    {f g : A →ₐ[R] B} {f' g' : A' →ₐ[R] B'}
    (hf : eB.toAlgHom.comp f = f'.comp eA) (hg : eB.toAlgHom.comp g = g'.comp eA) :
    AlgHom.equalizer f g ≃ₐ[R] AlgHom.equalizer f' g'

def

equalizerCongrOfEq

L116 ↗

AlgHom.equalizerCongrOfEq

Documentation

Identifies equalizers when both defining algebra homomorphisms are equal.

Source context 5 commands

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

@[expose] public section
attribute [local instance] Module.FinitePresentation.of_finite_of_finitePresentation
open TensorProduct
universe u v
section Equalizer

Lean source · statement

def AlgHom.equalizerCongrOfEq {R A B : Type*} [CommSemiring R] [Semiring A] [Semiring B]
    [Algebra R A] [Algebra R B] {f g f' g' : A →ₐ[R] B}
    (hf : f = f') (hg : g = g') :
    AlgHom.equalizer f g ≃ₐ[R] AlgHom.equalizer f' g'

lemma

exists_cover_rankAtStalk_eq

L132 ↗

Algebra.exists_cover_rankAtStalk_eq

Source context 5 commands

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

@[expose] public section
attribute [local instance] Module.FinitePresentation.of_finite_of_finitePresentation
open TensorProduct
universe u v
section rankAtStalk

Lean source · statement

lemma Algebra.exists_cover_rankAtStalk_eq {R : Type*} (S : Type*) [CommRing R] [CommRing S]
    [Algebra R S] [Module.FinitePresentation R S] [Module.Flat R S] (p : Ideal R) [p.IsPrime] :
    ∃ r ∉ p,
      Module.rankAtStalk (R := Localization.Away r) (Localization.Away r ⊗[R] S) =
        Module.rankAtStalk S ⟨p, inferInstance⟩

def

IsFiniteSplit

L160 ↗

RingHom.IsFiniteSplit

Documentation

A ring hom is split of (constant) rank n if S is R-split of rank n.

Source context 5 commands

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

@[expose] public section
attribute [local instance] Module.FinitePresentation.of_finite_of_finitePresentation
open TensorProduct
universe u v
namespace RingHom

Lean source · statement

def IsFiniteSplit {R S : Type*} [CommRing R] [CommRing S] (f : R →+* S) : Prop

def

compRight

L172 ↗

AlgHom.compRight

Documentation

Precomposition with σ as an R-algebra homomorphism between function algebras.

Source context 6 commands

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

@[expose] public section
attribute [local instance] Module.FinitePresentation.of_finite_of_finitePresentation
open TensorProduct
universe u v
section
variable {E F : Type*}

Lean source · statement

def AlgHom.compRight (R S : Type*) [CommRing R] [CommRing S] [Algebra R S] (σ : E → F) :
    (F → S) →ₐ[R] E → S

instance

(anonymous instance)

L176 ↗

Source context 6 commands

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

@[expose] public section
attribute [local instance] Module.FinitePresentation.of_finite_of_finitePresentation
open TensorProduct
universe u v
section
variable {E F : Type*}

Lean source · statement

instance [Finite F] (σ τ : E → F) : Finite (Function.Coequalizer σ τ)

def

compRight

L180 ↗

RingHom.compRight

Documentation

Precomposition with σ as a ring homomorphism between function rings.

Source context 6 commands

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

@[expose] public section
attribute [local instance] Module.FinitePresentation.of_finite_of_finitePresentation
open TensorProduct
universe u v
section
variable {E F : Type*}

Lean source · statement

def RingHom.compRight (R : Type*) [CommRing R] {E F : Type*} (σ : E → F) :
    (F → R) →+* (E → R)

lemma

compRight_apply

L185 ↗

RingHom.compRight_apply

Source context 6 commands

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

@[expose] public section
attribute [local instance] Module.FinitePresentation.of_finite_of_finitePresentation
open TensorProduct
universe u v
section
variable {E F : Type*}

Lean source · statement

lemma RingHom.compRight_apply (R : Type*) [CommRing R] {E F : Type*} (σ : E → F)
    (x : F → R) (i : E) :
    compRight R σ x i = x (σ i)

def

equalizerCompRightEquiv

L192 ↗

AlgHom.equalizerCompRightEquiv

Documentation

Identifies functions equal after precomposition by σ and τ with functions on their coequalizer.

Source context 6 commands

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

@[expose] public section
attribute [local instance] Module.FinitePresentation.of_finite_of_finitePresentation
open TensorProduct
universe u v
section
variable {E F : Type*}

Lean source · statement

def AlgHom.equalizerCompRightEquiv (R S : Type*) [CommRing R] [CommRing S] [Algebra R S]
    (σ τ : E → F) :
    AlgHom.equalizer (AlgHom.compRight R S σ) (AlgHom.compRight R S τ) ≃ₐ[R]
      Function.Coequalizer σ τ → S

instance

(anonymous instance)

L210 ↗

Source context 6 commands

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

@[expose] public section
attribute [local instance] Module.FinitePresentation.of_finite_of_finitePresentation
open TensorProduct
universe u v
section
variable {E F : Type*}

Lean source · statement

instance (R : Type*) [CommRing R] [Finite E] [Finite F] (σ τ : E → F) :
    Algebra.IsFiniteSplit R
      (AlgHom.equalizer (AlgHom.compRight R R σ) (AlgHom.compRight R R τ))

lemma

eq_compRight_of_no_nontrivial_isIdempotentElem

L215 ↗

AlgHom.eq_compRight_of_no_nontrivial_isIdempotentElem

Source context 6 commands

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

@[expose] public section
attribute [local instance] Module.FinitePresentation.of_finite_of_finitePresentation
open TensorProduct
universe u v
section
variable {E F : Type*}

Lean source · statement

lemma AlgHom.eq_compRight_of_no_nontrivial_isIdempotentElem {R E F : Type*} [_root_.Finite E]
    [Nonempty E] [CommRing R] (H : ∀ e : R, IsIdempotentElem e → e = 0 ∨ e = 1)
    (f : (E → R) →ₐ[R] F → R) : ∃ (σ : F → E), f = .compRight R R σ

lemma

eq_compRight_of_no_nontrivial_isIdempotentElem'

L267 ↗

AlgHom.eq_compRight_of_no_nontrivial_isIdempotentElem'

Source context 6 commands

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

@[expose] public section
attribute [local instance] Module.FinitePresentation.of_finite_of_finitePresentation
open TensorProduct
universe u v
section
variable {E F : Type*}

Lean source · statement

lemma AlgHom.eq_compRight_of_no_nontrivial_isIdempotentElem' {R E F : Type*} [_root_.Finite E]
    [CommRing R] [Nontrivial R] (H : ∀ e : R, IsIdempotentElem e → e = 0 ∨ e = 1)
    (f : (E → R) →ₐ[R] F → R) : ∃ (σ : F → E), f = .compRight R R σ

lemma

isIdempotentElem_iff_eq_zero_or_eq_one

L278 ↗

IsLocalRing.isIdempotentElem_iff_eq_zero_or_eq_one

Source context 6 commands

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

@[expose] public section
attribute [local instance] Module.FinitePresentation.of_finite_of_finitePresentation
open TensorProduct
universe u v
section
variable {E F : Type*}

Lean source · statement

lemma IsLocalRing.isIdempotentElem_iff_eq_zero_or_eq_one {R : Type*} [CommRing R] [IsLocalRing R]
    {e : R} : IsIdempotentElem e ↔ e = 0 ∨ e = 1

lemma

eq_compRight_of_isLocalHom

L289 ↗

RingHom.eq_compRight_of_isLocalHom

Source context 6 commands

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

@[expose] public section
attribute [local instance] Module.FinitePresentation.of_finite_of_finitePresentation
open TensorProduct
universe u v
section
variable {E F : Type*}

Lean source · statement

lemma RingHom.eq_compRight_of_isLocalHom {R E F : Type*} [_root_.Finite E] [CommRing R]
    (f : (E → R) →ₐ[R] F → R) [IsLocalRing R] :
    ∃ (σ : F → E), f = .compRight R R σ

lemma

exists_cover_eq_compRight''

L298 ↗

AlgHom.exists_cover_eq_compRight''

Source context 7 commands

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

@[expose] public section
attribute [local instance] Module.FinitePresentation.of_finite_of_finitePresentation
open TensorProduct
universe u v
section
variable {E F : Type*}
open Localization in

Lean source · statement

lemma AlgHom.exists_cover_eq_compRight'' {R : Type*} {E F : Type u}
    [_root_.Finite E] [_root_.Finite F]
    [CommRing R]
    (f : (E → R) →ₐ[R] F → R) (p : Ideal R) [p.IsPrime] :
    ∃ r ∉ p, ∃ (σ : F → E),
      Algebra.TensorProduct.map (.id (Away r) (Away r)) f =
        Algebra.TensorProduct.map (.id (Away r) (Away r)) (.compRight _ _ σ)

lemma

exists_cover_eq_compRight''₂

L336 ↗

AlgHom.exists_cover_eq_compRight''₂

Source context 7 commands

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

@[expose] public section
attribute [local instance] Module.FinitePresentation.of_finite_of_finitePresentation
open TensorProduct
universe u v
section
variable {E F : Type*}
open Localization in

Lean source · statement

lemma AlgHom.exists_cover_eq_compRight''₂ {R : Type*} {E F : Type u}
    [_root_.Finite E] [_root_.Finite F] [CommRing R] (f g : (E → R) →ₐ[R] F → R)
    (p : Ideal R) [p.IsPrime] :
    ∃ r ∉ p, ∃ (σ τ : F → E),
      Algebra.TensorProduct.map (.id (Away r) (Away r)) f =
        Algebra.TensorProduct.map (.id (Away r) (Away r)) (.compRight _ _ σ) ∧
      Algebra.TensorProduct.map (.id (Away r) (Away r)) g =
        Algebra.TensorProduct.map (.id (Away r) (Away r)) (.compRight _ _ τ)

lemma

equalizer_fun

L396 ↗

Algebra.FiniteEtale.equalizer_fun

Source context 4 commands

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

@[expose] public section
attribute [local instance] Module.FinitePresentation.of_finite_of_finitePresentation
open TensorProduct
universe u v

Lean source · statement

lemma Algebra.FiniteEtale.equalizer_fun {R : Type u} {E F : Type} [CommRing R] [Finite E] [Finite F]
    (f g : (E → R) →ₐ[R] (F → R)) :
    Algebra.FiniteEtale R (AlgHom.equalizer f g)

lemma

equalizer_of_isFiniteSplit

L422 ↗

Algebra.FiniteEtale.equalizer_of_isFiniteSplit

Source context 4 commands

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

@[expose] public section
attribute [local instance] Module.FinitePresentation.of_finite_of_finitePresentation
open TensorProduct
universe u v

Lean source · statement

lemma Algebra.FiniteEtale.equalizer_of_isFiniteSplit {R S T : Type u} [CommRing R]
    [CommRing S] [CommRing T] [Algebra R S]
    [Algebra R T] [Algebra.IsFiniteSplit R S] [Algebra.IsFiniteSplit R T] (f g : S →ₐ[R] T) :
    Algebra.FiniteEtale R (AlgHom.equalizer f g)

lemma

equalizer_of_rankAtStalk_eq

L436 ↗

Algebra.FiniteEtale.equalizer_of_rankAtStalk_eq

Source context 4 commands

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

@[expose] public section
attribute [local instance] Module.FinitePresentation.of_finite_of_finitePresentation
open TensorProduct
universe u v

Lean source · statement

lemma Algebra.FiniteEtale.equalizer_of_rankAtStalk_eq {R S T : Type u} [CommRing R] [CommRing S]
    [CommRing T] [Algebra R S] [Algebra R T]
    [Module.Finite R S] [Module.Finite R T] [Algebra.Etale R S] [Algebra.Etale R T]
    {n m : ℕ} (hn : Module.rankAtStalk (R := R) S = n) (hm : Module.rankAtStalk (R := R) T = m)
    (f g : S →ₐ[R] T) :
    Algebra.FiniteEtale R (AlgHom.equalizer f g)

theorem

equalizer

L479 ↗

Algebra.Etale.equalizer

Source context 4 commands

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

@[expose] public section
attribute [local instance] Module.FinitePresentation.of_finite_of_finitePresentation
open TensorProduct
universe u v

Lean source · statement

theorem Algebra.Etale.equalizer {R S T : Type u} [CommRing R] [CommRing S] [CommRing T]
    [Algebra R S] [Algebra R T]
    [Module.Finite R S] [Module.Finite R T] [Algebra.Etale R S] [Algebra.Etale R T]
    (f g : S →ₐ[R] T) :
    Algebra.FiniteEtale R (AlgHom.equalizer f g)

Module documentation

Equalizers of finite split algebras

Declarations