NYLL
Module

FlatEqualizer.lean

Nyll.SchemeTheory.Pi1.Descent.FlatEqualizer
16 declarations indexed from sourceView source ↗

Module documentation

Flat base change of algebra equalizers

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

Imports3
Imported by2

Declarations

def

equalizerCancelBaseChange

L50 ↗
AlgHom.equalizerCancelBaseChange
Documentation

Identifies equalizers after canceling repeated base change from R to T.

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 (S) in
Lean source · statement
def _root_.AlgHom.equalizerCancelBaseChange (f g : A →ₐ[R] B) (T : Type u) [CommRing T]
    [Algebra R T] :
    (((T ⊗[R] S) ⊗ₘ (T ⊗ₘ f)) ≟ₐ ((T ⊗[R] S) ⊗ₘ (T ⊗ₘ g))) ≃ₐ[T]
      (((T ⊗[R] S) ⊗ₘ f) ≟ₐ ((T ⊗[R] S) ⊗ₘ g))
lemma

equalizerCancelBaseChange_algebraMap

L60 ↗
AlgHom.equalizerCancelBaseChange_algebraMap
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 (S) in
Lean source · statement
lemma _root_.AlgHom.equalizerCancelBaseChange_algebraMap (f g : A →ₐ[R] B) (T : Type u) [CommRing T]
    [Algebra R T] (x : T ⊗[R] S) :
    AlgHom.equalizerCancelBaseChange S f g T (algebraMap _ _ x) = algebraMap _ _ x
lemma

equalizerCongr_symm_apply

L65 ↗
AlgHom.equalizerCongr_symm_apply
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 (S) in
Lean source · statement
lemma _root_.AlgHom.equalizerCongr_symm_apply {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)
    (x : AlgHom.equalizer f' g') :
    (AlgHom.equalizerCongr eA eB hf hg).symm x =
      ⟨eA.symm x, ((AlgHom.equalizerCongr eA eB hf hg).symm x).2⟩
lemma

equalizerCongr_apply

L76 ↗
AlgHom.equalizerCongr_apply
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 (S) in
Lean source · statement
lemma _root_.AlgHom.equalizerCongr_apply {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)
    (x : AlgHom.equalizer f g) :
    AlgHom.equalizerCongr eA eB hf hg x =
      ⟨eA x, (AlgHom.equalizerCongr eA eB hf hg x).2⟩
lemma

equalizerCancelBaseChange_tmul

L88 ↗
AlgHom.equalizerCancelBaseChange_tmul
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 (S) in
Lean source · full declaration
lemma _root_.AlgHom.equalizerCancelBaseChange_tmul (f g : A →ₐ[R] B) (T : Type u) [CommRing T]
    [Algebra R T] (x : A) (hx : x ∈ AlgHom.equalizer f g) :
    ((AlgHom.equalizerCancelBaseChange S f g T)
      ⟨1 ⊗ₜ[T] (1 ⊗ₜ[R] x), by simp [show f x = g x from hx]⟩) =
        ⟨1 ⊗ₜ x, by simp [show f x = g x from hx]⟩ := by
  ext : 1
  simp [AlgHom.equalizerCancelBaseChange, AlgHom.equalizerCongr_apply]
lemma

tensorEqualizerEquiv_symm_apply

L96 ↗
AlgHom.tensorEqualizerEquiv_symm_apply
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 (S) in
Lean source · full declaration
lemma _root_.AlgHom.tensorEqualizerEquiv_symm_apply
    {R : Type*} (S : Type*) [CommRing R]
    [CommRing S] [Algebra R S] (T : Type*) [CommRing T]
    [Algebra R T] [Algebra S T] [IsScalarTower R S T]
    {A B : Type*} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
    (f g : A →ₐ[R] B) [Module.Flat R T]
    (x : A) (hx : x ∈ AlgHom.equalizer f g) :
    (f.tensorEqualizerEquiv S T g).symm ⟨1 ⊗ₜ x, by simp [show f x = g x from hx]⟩ =
      1 ⊗ₜ ⟨x, hx⟩ := by
  apply (f.tensorEqualizerEquiv S T g).injective
  ext
  simp
def

auxEquivRHS

L112 ↗
Algebra.auxEquivRHS
Documentation

For flat T, identifies the base change of the equalizer of the S-base-changed maps with the equalizer of the further base-changed maps over T ⊗[R] S.

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 (S) in
Lean source · statement
def auxEquivRHS (f g : A →ₐ[R] B) (T : Type u) [CommRing T] [Algebra R T]
    [Module.Flat R T] :
    T ⊗[R] ((S ⊗ₘ f) ≟ₐ (S ⊗ₘ g)) ≃ₐ[T]
      ((T ⊗[R] S) ⊗ₘ (T ⊗ₘ f)) ≟ₐ ((T ⊗[R] S) ⊗ₘ (T ⊗ₘ g))
lemma

auxEquivRHS_symm_tmul

L140 ↗
Algebra.auxEquivRHS_symm_tmul
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 (S) in
Lean source · statement
lemma auxEquivRHS_symm_tmul (f g : A →ₐ[R] B) (T : Type u) [CommRing T] [Algebra R T]
    [Module.Flat R T] (x : S) :
    (auxEquivRHS (S := S) f g T).symm (algebraMap (T ⊗[R] S) _ (1 ⊗ₜ x)) =
      1 ⊗ₜ algebraMap _ _ x
lemma

auxEquivRHS_symm_tmul'

L163 ↗
Algebra.auxEquivRHS_symm_tmul'
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 (S) in
Lean source · full declaration
lemma auxEquivRHS_symm_tmul' (f g : A →ₐ[R] B) (T : Type u) [CommRing T] [Algebra R T]
    [Module.Flat R T] (x : AlgHom.equalizer f g) :
    (auxEquivRHS (S := S) f g T).symm ⟨1 ⊗ₜ (1 ⊗ₜ x), by simp [show f x = g x from x.2]⟩ =
      1 ⊗ₜ ⟨1 ⊗ₜ x, by simp [show f x = g x from x.2]⟩ := by
  apply (auxEquivRHS (S := S) f g T).injective
  rw [AlgEquiv.apply_symm_apply]
  apply (f.equalizerCancelBaseChange S g T).injective
  change _ = (f.equalizerCancelBaseChange S g T)
    ((f.equalizerCancelBaseChange S g T).symm _)
  rw [AlgEquiv.apply_symm_apply]
  apply Subtype.ext
  simp only [SetLike.coe_mem, AlgHom.equalizerCancelBaseChange_tmul, AlgEquiv.toEquiv_eq_coe,
    EquivLike.coe_coe, TensorProduct.congr_apply, AlgEquiv.refl_toAlgHom,
    TensorProduct.map_tmul, AlgHom.coe_id, id_eq, AlgEquiv.coe_toAlgHom,
    AlgHom.equalizerRestrictScalars_symm_apply, AlgHom.tensorEqualizerEquiv_apply,
    AlgEquiv.trans_apply, AlgHom.equalizerRestrictScalars_apply]
  change
    (1 ⊗ₜ[R] (1 : S)) ⊗ₜ[R] (x : A) =
      (TensorProduct.assoc R R T T S A).symm
        (1 ⊗ₜ[R] ((1 : S) ⊗ₜ[R] (x : A)))
  rw [TensorProduct.assoc_symm_tmul]
def

auxEquivLHS

L188 ↗
Algebra.auxEquivLHS
Documentation

For flat T, reassociates T ⊗[R] (S ⊗[R] equalizer f g) and identifies it with (T ⊗[R] S) ⊗[T] equalizer(T ⊗ f, T ⊗ g) by flat base change.

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 (S) in
Lean source · statement
def auxEquivLHS (f g : A →ₐ[R] B) (T : Type u) [CommRing T] [Algebra R T] [Module.Flat R T] :
    T ⊗[R] (S ⊗[R] f ≟ₐ g) ≃ₐ[T] (T ⊗[R] S) ⊗[T] ((T ⊗ₘ f) ≟ₐ (T ⊗ₘ g))
lemma

auxEquivLHS_one_tmul_one

L197 ↗
Algebra.auxEquivLHS_one_tmul_one
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 (S) in
Lean source · statement
lemma auxEquivLHS_one_tmul_one (f g : A →ₐ[R] B) (T : Type u) [CommRing T] [Algebra R T]
    [Module.Flat R T] (x : S) :
    auxEquivLHS f g T (1 ⊗ₜ[R] (x ⊗ₜ[R] 1)) = (1 ⊗ₜ x) ⊗ₜ 1
lemma

auxEquivLHS_one_one_tmul

L202 ↗
Algebra.auxEquivLHS_one_one_tmul
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 (S) in
Lean source · full declaration
lemma auxEquivLHS_one_one_tmul (f g : A →ₐ[R] B) (T : Type u) [CommRing T] [Algebra R T]
    [Module.Flat R T] (x : AlgHom.equalizer f g) :
    (auxEquivLHS (S := S) f g T) (1 ⊗ₜ[R] (1 ⊗ₜ[R] x)) =
      1 ⊗ₜ ⟨1 ⊗ₜ x, by simp [show f x.1 = g x.1 from x.2]⟩ :=
  rfl
lemma

tensorEqualizer_tmul_one

L208 ↗
AlgHom.tensorEqualizer_tmul_one
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 (S) in
Lean source · statement
lemma _root_.AlgHom.tensorEqualizer_tmul_one (f g : A →ₐ[R] B) (x : S) :
    f.tensorEqualizer S S g (x ⊗ₜ 1) = algebraMap S _ x
lemma

tensorEqualizer_one_tmul

L212 ↗
AlgHom.tensorEqualizer_one_tmul
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 (S) in
Lean source · full declaration
lemma _root_.AlgHom.tensorEqualizer_one_tmul {R : Type*} (S : Type*) [CommRing R]
      [CommRing S] [Algebra R S] (T : Type*) [CommRing T]
      [Algebra R T] [Algebra S T] [IsScalarTower R S T]
      {A B : Type*} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
      (f g : A →ₐ[R] B) (x : AlgHom.equalizer f g) :
    f.tensorEqualizer S T g (1 ⊗ₜ x) = ⟨1 ⊗ₜ x, by simp [show f x.1 = g x.1 from x.2]⟩ :=
  rfl
lemma

tensorEqualizer_tmul_one'

L220 ↗
AlgHom.tensorEqualizer_tmul_one'
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 (S) in
Lean source · full declaration
lemma _root_.AlgHom.tensorEqualizer_tmul_one' {R : Type*} (S : Type*) [CommRing R]
      [CommRing S] [Algebra R S] (T : Type*) [CommRing T]
      [Algebra R T] [Algebra S T] [IsScalarTower R S T]
      {A B : Type*} [CommRing A] [CommRing B] [Algebra R A] [Algebra R B]
      (f g : A →ₐ[R] B) (x : T) :
    f.tensorEqualizer S T g (x ⊗ₜ 1) = ⟨x ⊗ₜ 1, by simp⟩ :=
  rfl
lemma

map_tensorEqualizer_bijective_iff_tensorEqualizer_map_bijective

L229 ↗
Algebra.TensorProduct.map_tensorEqualizer_bijective_iff_tensorEqualizer_map_bijective
Source context 9 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 (S) in
variable (S) in
Lean source · statement
lemma TensorProduct.map_tensorEqualizer_bijective_iff_tensorEqualizer_map_bijective
    (f g : A →ₐ[R] B) (T : Type u) [CommRing T] [Algebra R T] [Module.Flat R T] :
    Function.Bijective ⇑(TensorProduct.map (AlgHom.id T T) (AlgHom.tensorEqualizer R S f g)) ↔
    Function.Bijective
            ((TensorProduct.map (.id T T) f).tensorEqualizer T (T ⊗[R] S)
                  (TensorProduct.map (.id T T) g))

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