Module

EqualizerScalars.lean

Nyll.SchemeTheory.Pi1.Descent.EqualizerScalars

2 declarations indexed from sourceView source ↗

Module documentation

Scalar restriction of algebra equalizers

Scalar restriction and tensor-product comparisons identify equalizers after flat base change, using the original algebra homomorphisms.

Imports2

Mathlib.RingTheory.TensorProduct.Maps
Nyll.SchemeTheory.Pi1.FiniteEtale.Algebra.Equalizer

Imported by2

def

equalizerRestrictScalars

L48 ↗

AlgHom.equalizerRestrictScalars

Documentation

Restricting scalars from S to R preserves the underlying equalizer subalgebra.

Source context 8 commands

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

@[expose] public section
universe u
open TensorProduct
variable {R S A B : Type u} [CommRing R] [CommRing S] [CommRing A] [CommRing B]
  [Algebra R A] [Algebra R S] [Algebra R B]
namespace Algebra
local notation f " ≟ₐ " g => AlgHom.equalizer f g
--local notation "eq(" f " , " g ")" => AlgHom.equalizer f g
local notation S " ⊗ₘ " f => Algebra.TensorProduct.map (AlgHom.id S S) f
variable (R) in

Lean source · statement

def _root_.AlgHom.equalizerRestrictScalars [Algebra S A] [Algebra S B]
    [IsScalarTower R S A] [IsScalarTower R S B]
    (f g : A →ₐ[S] B) :
    AlgHom.equalizer (f.restrictScalars R) (g.restrictScalars R) ≃ₐ[R]
      AlgHom.equalizer f g

lemma

equalizerRestrictScalars_symm_apply

L56 ↗

AlgHom.equalizerRestrictScalars_symm_apply