Module

AlgEquivDescent.lean

Nyll.EtaleFundamentalGroups.GenericTensor.FilteredColimit.AlgEquivDescent

9 declarations indexed from sourceView source ↗

Module documentation

Descending tensor-product equivalences from filtered colimits

A finite presentation over a base ring is compact with respect to filtered colimits. Applying this twice, to the forward and inverse maps of an equivalence after base change, and then moving the two inverse equations to a common later stage, descends the whole equivalence to one finite stage.

This is the finite-data descent needed after a strict-Henselian splitting. It does not assume or construct a strict henselization: the input is an arbitrary filtered colimit of pointed base algebras.

Imports11

Mathlib.Algebra.Category.Ring.FinitePresentation
Mathlib.Algebra.MvPolynomial.Basic
Mathlib.Algebra.MvPolynomial.Eval
Mathlib.Algebra.Category.Ring.Under.Basic
Mathlib.CategoryTheory.Limits.Constructions.Over.Connected
Mathlib.CategoryTheory.Presentable.Basic
Mathlib.RingTheory.FiniteStability
Mathlib.RingTheory.FinitePresentation
Mathlib.Data.Fintype.EquivFin
Mathlib.RingTheory.TensorProduct.Maps
Nyll.EtaleFundamentalGroups.GenericTensor.FilteredColimit.CoconeLeg

Imported by7

instance

underCommRingCatAlgebraDescent

L42 ↗

EtaleFundamentalGroups.underCommRingCatAlgebraDescent

Source context 5 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u

Lean source · statement

instance underCommRingCatAlgebraDescent
    {R : Type u} [CommRing R] (A : Under (CommRingCat.of R)) : Algebra R A

theorem

exists_tensorProduct_algHom_stage_of_filteredColimit

L50 ↗

EtaleFundamentalGroups.exists_tensorProduct_algHom_stage_of_filteredColimit

Documentation

Descend one tensor-product morphism to a finite stage of the coefficient colimit. Only the source algebra needs a finite presentation. The descended map is an actual algebra homomorphism between the two stage tensor products, and its scalar extension recovers the given morphism along the literal cocone maps.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u
local instance underCommRingCatAlgebraDescent
    {R : Type u} [CommRing R] (A : Under (CommRingCat.of R)) : Algebra R A :=
  RingHom.toAlgebra A.hom.hom

Lean source · statement

theorem exists_tensorProduct_algHom_stage_of_filteredColimit
    {R B D : Type u} [CommRing R] [CommRing B] [CommRing D]
    [Algebra R B] [Algebra R D]
    [Algebra.FinitePresentation R B]
    {J : Type u} [SmallCategory J] [IsFiltered J]
    (F : J ⥤ Under (CommRingCat.of R))
    (c : Cocone F) (hc : IsColimit c)
    (f : (c.pt ⊗[R] B) →ₐ[c.pt] (c.pt ⊗[R] D)) :
    ∃ (i : J) (fᵢ : (F.obj i ⊗[R] B) →ₐ[F.obj i] (F.obj i ⊗[R] D)),
      (filteredTensorToColimitAlgHom c i (A := D)).comp (fᵢ.restrictScalars R) =
        (f.restrictScalars R).comp
          (filteredTensorToColimitAlgHom c i (A := B))

theorem

exists_stage_algHom_pair_of_filteredColimit

L149 ↗

EtaleFundamentalGroups.exists_stage_algHom_pair_of_filteredColimit

Documentation

Descend both maps of an equivalence to a common finite stage.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u
local instance underCommRingCatAlgebraDescent
    {R : Type u} [CommRing R] (A : Under (CommRingCat.of R)) : Algebra R A :=
  RingHom.toAlgebra A.hom.hom

Lean source · statement

theorem exists_stage_algHom_pair_of_filteredColimit
    {R B D : Type u} [CommRing R] [CommRing B] [CommRing D]
    [Algebra R B] [Algebra R D]
    [Algebra.FinitePresentation R B]
    [Algebra.FinitePresentation R D]
    {J : Type u} [SmallCategory J] [IsFiltered J]
    (F : J ⥤ Under (CommRingCat.of R))
    (c : Cocone F) (hc : IsColimit c)
    (e : (c.pt ⊗[R] B) ≃ₐ[c.pt] (c.pt ⊗[R] D)) :
    ∃ (k : J)
      (fₖ : B →ₐ[R] (F.obj k ⊗[R] D))
      (gₖ : D →ₐ[R] (F.obj k ⊗[R] B)),
      (filteredTensorToColimitAlgHom c k (A := D)).comp
          ((AlgHom.liftEquiv R (F.obj k) B (F.obj k ⊗[R] D) fₖ).restrictScalars R) =
        (e.toAlgHom.restrictScalars R).comp
          (filteredTensorToColimitAlgHom c k (A := B)) ∧
      (filteredTensorToColimitAlgHom c k (A := B)).comp
          ((AlgHom.liftEquiv R (F.obj k) D (F.obj k ⊗[R] B) gₖ).restrictScalars R) =
        (e.symm.toAlgHom.restrictScalars R).comp
          (filteredTensorToColimitAlgHom c k (A := D))

theorem

stage_comp_identity_at_colimit

L252 ↗

EtaleFundamentalGroups.stage_comp_identity_at_colimit

Documentation

The two descended maps compose to the identity after applying the colimit cocone.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u
local instance underCommRingCatAlgebraDescent
    {R : Type u} [CommRing R] (A : Under (CommRingCat.of R)) : Algebra R A :=
  RingHom.toAlgebra A.hom.hom

Lean source · full declaration

theorem stage_comp_identity_at_colimit
    {R B D : Type u} [CommRing R] [CommRing B] [CommRing D]
    [Algebra R B] [Algebra R D]
    {J : Type u} [SmallCategory J] [IsFiltered J]
    (F : J ⥤ Under (CommRingCat.of R))
    (c : Cocone F) (k : J)
    (e : (c.pt ⊗[R] B) ≃ₐ[c.pt] (c.pt ⊗[R] D))
    (φₖ : (F.obj k ⊗[R] B) →ₐ[F.obj k] (F.obj k ⊗[R] D))
    (ψₖ : (F.obj k ⊗[R] D) →ₐ[F.obj k] (F.obj k ⊗[R] B))
    (hφₖ :
      (filteredTensorToColimitAlgHom c k (A := D)).comp
          (φₖ.restrictScalars R) =
        (e.toAlgHom.restrictScalars R).comp
          (filteredTensorToColimitAlgHom c k (A := B)))
    (hψₖ :
      (filteredTensorToColimitAlgHom c k (A := B)).comp
          (ψₖ.restrictScalars R) =
        (e.symm.toAlgHom.restrictScalars R).comp
          (filteredTensorToColimitAlgHom c k (A := D))) :
    let compB : B →ₐ[R] (B ⊗[R] F.obj k) :=
      (Algebra.TensorProduct.comm R (F.obj k) B).toAlgHom.comp
        (((ψₖ.comp φₖ).restrictScalars R).comp
          Algebra.TensorProduct.includeRight)
    let idB : B →ₐ[R] (B ⊗[R] F.obj k) :=
      Algebra.TensorProduct.includeLeft
    let compBB : (B ⊗[R] B) →ₐ[B] (B ⊗[R] F.obj k) :=
      AlgHom.liftEquiv R B B (B ⊗[R] F.obj k) compB
    let idBB : (B ⊗[R] B) →ₐ[B] (B ⊗[R] F.obj k) :=
      AlgHom.liftEquiv R B B (B ⊗[R] F.obj k) idB
    (filteredBaseChangeCoconeLegAlgHom c k (A := B)).comp compBB =
      (filteredBaseChangeCoconeLegAlgHom c k (A := B)).comp idBB := by
  let compB : B →ₐ[R] (B ⊗[R] F.obj k) :=
    (Algebra.TensorProduct.comm R (F.obj k) B).toAlgHom.comp
      (((ψₖ.comp φₖ).restrictScalars R).comp
        Algebra.TensorProduct.includeRight)
  let idB : B →ₐ[R] (B ⊗[R] F.obj k) :=
    Algebra.TensorProduct.includeLeft
  let compBB : (B ⊗[R] B) →ₐ[B] (B ⊗[R] F.obj k) :=
    AlgHom.liftEquiv R B B (B ⊗[R] F.obj k) compB
  let idBB : (B ⊗[R] B) →ₐ[B] (B ⊗[R] F.obj k) :=
    AlgHom.liftEquiv R B B (B ⊗[R] F.obj k) idB
  change (filteredBaseChangeCoconeLegAlgHom c k (A := B)).comp compBB =
    (filteredBaseChangeCoconeLegAlgHom c k (A := B)).comp idBB
  apply Algebra.TensorProduct.ext_ring
  ext b
  simp only [AlgHom.comp_apply, AlgHom.restrictScalars_apply,
    compBB, idBB, AlgHom.liftEquiv_tmul, one_smul,
    compB, idB, Algebra.TensorProduct.includeRight_apply]
  change filteredBaseChangeCoconeLegAlgHom c k
      ((Algebra.TensorProduct.comm R (F.obj k) B)
        (ψₖ (φₖ (1 ⊗ₜ[R] b)))) =
    filteredBaseChangeCoconeLegAlgHom c k (b ⊗ₜ[R] 1)
  nth_rewrite 2 [← Algebra.TensorProduct.comm_tmul]
  rw [filteredBaseChangeCoconeLegAlgHom_comm,
    filteredBaseChangeCoconeLegAlgHom_comm]
  have hψ := congrArg (fun h ↦ h (φₖ (1 ⊗ₜ[R] b))) hψₖ
  have hφ := congrArg (fun h ↦ h (1 ⊗ₜ[R] b)) hφₖ
  have hinner :
      filteredTensorToColimitAlgHom c k (ψₖ (φₖ (1 ⊗ₜ[R] b))) =
        filteredTensorToColimitAlgHom c k (1 ⊗ₜ[R] b) := by
    calc
      filteredTensorToColimitAlgHom c k (ψₖ (φₖ (1 ⊗ₜ[R] b))) =
        ((filteredTensorToColimitAlgHom c k).comp
          (ψₖ.restrictScalars R)) (φₖ (1 ⊗ₜ[R] b)) := rfl
      _ = ((e.symm.toAlgHom.restrictScalars R).comp
          (filteredTensorToColimitAlgHom c k))
            (φₖ (1 ⊗ₜ[R] b)) := hψ
      _ = e.symm (((filteredTensorToColimitAlgHom c k).comp
          (φₖ.restrictScalars R)) (1 ⊗ₜ[R] b)) := rfl
      _ = e.symm (((e.toAlgHom.restrictScalars R).comp
          (filteredTensorToColimitAlgHom c k)) (1 ⊗ₜ[R] b)) := by
            rw [hφ]
      _ = filteredTensorToColimitAlgHom c k (1 ⊗ₜ[R] b) :=
        e.symm_apply_apply _
  exact congrArg (fun z ↦ Algebra.TensorProduct.comm R c.pt B z) hinner

theorem

exists_baseChange_algHom_eq_stage

L330 ↗

EtaleFundamentalGroups.exists_baseChange_algHom_eq_stage

Documentation

Equality of two maps from a finitely presented algebra into a base-change stage is detected after one common transition of the coefficient diagram.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u
local instance underCommRingCatAlgebraDescent
    {R : Type u} [CommRing R] (A : Under (CommRingCat.of R)) : Algebra R A :=
  RingHom.toAlgebra A.hom.hom

Lean source · statement

theorem exists_baseChange_algHom_eq_stage
    {R B A : Type u} [CommRing R] [CommRing B] [CommRing A]
    [Algebra R B] [Algebra B A] [Algebra.FinitePresentation B A]
    {J : Type u} [SmallCategory J] [IsFiltered J]
    (F : J ⥤ Under (CommRingCat.of R))
    (c : Cocone F) (hc : IsColimit c) (k : J)
    (f g : A →ₐ[B] (B ⊗[R] F.obj k))
    (hfg : (filteredBaseChangeCoconeLegAlgHom c k (A := B)).comp f =
      (filteredBaseChangeCoconeLegAlgHom c k (A := B)).comp g) :
    ∃ (l : J) (hkl : k ⟶ l),
      f.toUnder ≫ (F ⋙ CommRingCat.tensorProd (CommRingCat.of R)
          (CommRingCat.of B)).map hkl =
        g.toUnder ≫ (F ⋙ CommRingCat.tensorProd (CommRingCat.of R)
          (CommRingCat.of B)).map hkl

theorem

exists_stage_comp_identity

L367 ↗

EtaleFundamentalGroups.exists_stage_comp_identity

Documentation

A finitely presented algebra detects one composite identity at a finite stage.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u
local instance underCommRingCatAlgebraDescent
    {R : Type u} [CommRing R] (A : Under (CommRingCat.of R)) : Algebra R A :=
  RingHom.toAlgebra A.hom.hom

Lean source · full declaration

theorem exists_stage_comp_identity
    {R B D : Type u} [CommRing R] [CommRing B] [CommRing D]
    [Algebra R B] [Algebra R D]
    [Algebra.FinitePresentation R B]
    {J : Type u} [SmallCategory J] [IsFiltered J]
    (F : J ⥤ Under (CommRingCat.of R))
    (c : Cocone F) (hc : IsColimit c) (k : J)
    (e : (c.pt ⊗[R] B) ≃ₐ[c.pt] (c.pt ⊗[R] D))
    (φₖ : (F.obj k ⊗[R] B) →ₐ[F.obj k] (F.obj k ⊗[R] D))
    (ψₖ : (F.obj k ⊗[R] D) →ₐ[F.obj k] (F.obj k ⊗[R] B))
    (hφₖ :
      (filteredTensorToColimitAlgHom c k (A := D)).comp
          (φₖ.restrictScalars R) =
        (e.toAlgHom.restrictScalars R).comp
          (filteredTensorToColimitAlgHom c k (A := B)))
    (hψₖ :
      (filteredTensorToColimitAlgHom c k (A := B)).comp
          (ψₖ.restrictScalars R) =
        (e.symm.toAlgHom.restrictScalars R).comp
          (filteredTensorToColimitAlgHom c k (A := D))) :
    let R₀ : CommRingCat.{u} := CommRingCat.of R
    let B₀ : CommRingCat.{u} := CommRingCat.of B
    let tB : Under R₀ ⥤ Under B₀ := CommRingCat.tensorProd R₀ B₀
    let FB : J ⥤ Under B₀ := F ⋙ tB
    let compB : B →ₐ[R] (B ⊗[R] F.obj k) :=
      (Algebra.TensorProduct.comm R (F.obj k) B).toAlgHom.comp
        (((ψₖ.comp φₖ).restrictScalars R).comp
          Algebra.TensorProduct.includeRight)
    let idB : B →ₐ[R] (B ⊗[R] F.obj k) :=
      Algebra.TensorProduct.includeLeft
    let compBB : (B ⊗[R] B) →ₐ[B] (B ⊗[R] F.obj k) :=
      AlgHom.liftEquiv R B B (B ⊗[R] F.obj k) compB
    let idBB : (B ⊗[R] B) →ₐ[B] (B ⊗[R] F.obj k) :=
      AlgHom.liftEquiv R B B (B ⊗[R] F.obj k) idB
    ∃ (l : J) (hkl : k ⟶ l),
      compBB.toUnder ≫ FB.map hkl = idBB.toUnder ≫ FB.map hkl := by
  intro R₀ B₀ tB FB compB idB compBB idBB
  exact exists_baseChange_algHom_eq_stage (A := B ⊗[R] B) F c hc k compBB idBB
    (stage_comp_identity_at_colimit F c k e φₖ ψₖ hφₖ hψₖ)

theorem

exists_common_stage_for_inverse_equations

L408 ↗

EtaleFundamentalGroups.exists_common_stage_for_inverse_equations

Documentation

A later finite stage makes both descended composites the identity.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u
local instance underCommRingCatAlgebraDescent
    {R : Type u} [CommRing R] (A : Under (CommRingCat.of R)) : Algebra R A :=
  RingHom.toAlgebra A.hom.hom

Lean source · full declaration

theorem exists_common_stage_for_inverse_equations
    {R B D : Type u} [CommRing R] [CommRing B] [CommRing D]
    [Algebra R B] [Algebra R D]
    [Algebra.FinitePresentation R B] [Algebra.FinitePresentation R D]
    {J : Type u} [SmallCategory J] [IsFiltered J]
    (F : J ⥤ Under (CommRingCat.of R))
    (c : Cocone F) (hc : IsColimit c) (k : J)
    (e : (c.pt ⊗[R] B) ≃ₐ[c.pt] (c.pt ⊗[R] D))
    (φₖ : (F.obj k ⊗[R] B) →ₐ[F.obj k] (F.obj k ⊗[R] D))
    (ψₖ : (F.obj k ⊗[R] D) →ₐ[F.obj k] (F.obj k ⊗[R] B))
    (hφₖ :
      (filteredTensorToColimitAlgHom c k (A := D)).comp
          (φₖ.restrictScalars R) =
        (e.toAlgHom.restrictScalars R).comp
          (filteredTensorToColimitAlgHom c k (A := B)))
    (hψₖ :
      (filteredTensorToColimitAlgHom c k (A := B)).comp
          (ψₖ.restrictScalars R) =
        (e.symm.toAlgHom.restrictScalars R).comp
          (filteredTensorToColimitAlgHom c k (A := D))) :
    let R₀ : CommRingCat.{u} := CommRingCat.of R
    let B₀ : CommRingCat.{u} := CommRingCat.of B
    let D₀ : CommRingCat.{u} := CommRingCat.of D
    let tB : Under R₀ ⥤ Under B₀ := CommRingCat.tensorProd R₀ B₀
    let tD : Under R₀ ⥤ Under D₀ := CommRingCat.tensorProd R₀ D₀
    let FB : J ⥤ Under B₀ := F ⋙ tB
    let FD : J ⥤ Under D₀ := F ⋙ tD
    let compB : B →ₐ[R] (B ⊗[R] F.obj k) :=
      (Algebra.TensorProduct.comm R (F.obj k) B).toAlgHom.comp
        (((ψₖ.comp φₖ).restrictScalars R).comp
          Algebra.TensorProduct.includeRight)
    let idB : B →ₐ[R] (B ⊗[R] F.obj k) :=
      Algebra.TensorProduct.includeLeft
    let compBB : (B ⊗[R] B) →ₐ[B] (B ⊗[R] F.obj k) :=
      AlgHom.liftEquiv R B B (B ⊗[R] F.obj k) compB
    let idBB : (B ⊗[R] B) →ₐ[B] (B ⊗[R] F.obj k) :=
      AlgHom.liftEquiv R B B (B ⊗[R] F.obj k) idB
    let compD : D →ₐ[R] (D ⊗[R] F.obj k) :=
      (Algebra.TensorProduct.comm R (F.obj k) D).toAlgHom.comp
        (((φₖ.comp ψₖ).restrictScalars R).comp
          Algebra.TensorProduct.includeRight)
    let idD : D →ₐ[R] (D ⊗[R] F.obj k) :=
      Algebra.TensorProduct.includeLeft
    let compDD : (D ⊗[R] D) →ₐ[D] (D ⊗[R] F.obj k) :=
      AlgHom.liftEquiv R D D (D ⊗[R] F.obj k) compD
    let idDD : (D ⊗[R] D) →ₐ[D] (D ⊗[R] F.obj k) :=
      AlgHom.liftEquiv R D D (D ⊗[R] F.obj k) idD
    ∃ (m : J) (hkm' : k ⟶ m),
      compBB.toUnder ≫ FB.map hkm' = idBB.toUnder ≫ FB.map hkm' ∧
      compDD.toUnder ≫ FD.map hkm' = idDD.toUnder ≫ FD.map hkm' ∧
      (filteredTensorToColimitAlgHom c m (A := B)).comp
          (Algebra.TensorProduct.map
            (CommRingCat.toAlgHom (F.map hkm')) (AlgHom.id R B)) =
        filteredTensorToColimitAlgHom c k ∧
      (filteredTensorToColimitAlgHom c m (A := D)).comp
          (Algebra.TensorProduct.map
            (CommRingCat.toAlgHom (F.map hkm')) (AlgHom.id R D)) =
        filteredTensorToColimitAlgHom c k := by
  classical
  let R₀ : CommRingCat.{u} := CommRingCat.of R
  let B₀ : CommRingCat.{u} := CommRingCat.of B
  let D₀ : CommRingCat.{u} := CommRingCat.of D
  let tB : Under R₀ ⥤ Under B₀ := CommRingCat.tensorProd R₀ B₀
  let tD : Under R₀ ⥤ Under D₀ := CommRingCat.tensorProd R₀ D₀
  let FB : J ⥤ Under B₀ := F ⋙ tB
  let FD : J ⥤ Under D₀ := F ⋙ tD
  let compB : B →ₐ[R] (B ⊗[R] F.obj k) :=
    (Algebra.TensorProduct.comm R (F.obj k) B).toAlgHom.comp
      (((ψₖ.comp φₖ).restrictScalars R).comp
        Algebra.TensorProduct.includeRight)
  let idB : B →ₐ[R] (B ⊗[R] F.obj k) :=
    Algebra.TensorProduct.includeLeft
  let compBB : (B ⊗[R] B) →ₐ[B] (B ⊗[R] F.obj k) :=
    AlgHom.liftEquiv R B B (B ⊗[R] F.obj k) compB
  let idBB : (B ⊗[R] B) →ₐ[B] (B ⊗[R] F.obj k) :=
    AlgHom.liftEquiv R B B (B ⊗[R] F.obj k) idB
  let compD : D →ₐ[R] (D ⊗[R] F.obj k) :=
    (Algebra.TensorProduct.comm R (F.obj k) D).toAlgHom.comp
      (((φₖ.comp ψₖ).restrictScalars R).comp
        Algebra.TensorProduct.includeRight)
  let idD : D →ₐ[R] (D ⊗[R] F.obj k) :=
    Algebra.TensorProduct.includeLeft
  let compDD : (D ⊗[R] D) →ₐ[D] (D ⊗[R] F.obj k) :=
    AlgHom.liftEquiv R D D (D ⊗[R] F.obj k) compD
  let idDD : (D ⊗[R] D) →ₐ[D] (D ⊗[R] F.obj k) :=
    AlgHom.liftEquiv R D D (D ⊗[R] F.obj k) idD
  obtain ⟨lB, hklB, hB⟩ :=
    exists_stage_comp_identity F c hc k e φₖ ψₖ hφₖ hψₖ
  obtain ⟨lD, hklD, hD⟩ :=
    exists_stage_comp_identity (B := D) (D := B)
      F c hc k e.symm ψₖ φₖ hψₖ hφₖ
  let l := IsFiltered.max lB lD
  let hlBl : lB ⟶ l := IsFiltered.leftToMax lB lD
  let hlDl : lD ⟶ l := IsFiltered.rightToMax lB lD
  let hkB : k ⟶ l := hklB ≫ hlBl
  let hkD : k ⟶ l := hklD ≫ hlDl
  let m := IsFiltered.coeq hkB hkD
  let hlm : l ⟶ m := IsFiltered.coeqHom hkB hkD
  have hkm : hkB ≫ hlm = hkD ≫ hlm :=
    IsFiltered.coeq_condition hkB hkD
  let hkm' : k ⟶ m := hkB ≫ hlm
  let fkm : F.obj k →ₐ[R] F.obj m := CommRingCat.toAlgHom (F.map hkm')
  have hclegApply (x : F.obj k) :
      CommRingCat.toAlgHom (c.ι.app m) (fkm x) =
        CommRingCat.toAlgHom (c.ι.app k) x := by
    have h := congrArg (fun q ↦ q.right x) (c.w hkm')
    change CommRingCat.toAlgHom (c.ι.app m)
        (CommRingCat.toAlgHom (F.map hkm') x) =
      CommRingCat.toAlgHom (c.ι.app k) x at h
    simpa only [fkm] using h
  have hcTensorB :
      (filteredTensorToColimitAlgHom c m (A := B)).comp
          (Algebra.TensorProduct.map fkm (AlgHom.id R B)) =
        filteredTensorToColimitAlgHom c k := by
    apply Algebra.TensorProduct.ext
    · ext x
      change CommRingCat.toAlgHom (c.ι.app m) (fkm x) ⊗ₜ[R] (1 : B) =
        CommRingCat.toAlgHom (c.ι.app k) x ⊗ₜ[R] (1 : B)
      rw [hclegApply]
    · ext b
      simp [filteredTensorToColimitAlgHom]
  have hcTensorD :
      (filteredTensorToColimitAlgHom c m (A := D)).comp
          (Algebra.TensorProduct.map fkm (AlgHom.id R D)) =
        filteredTensorToColimitAlgHom c k := by
    apply Algebra.TensorProduct.ext
    · ext x
      change CommRingCat.toAlgHom (c.ι.app m) (fkm x) ⊗ₜ[R] (1 : D) =
        CommRingCat.toAlgHom (c.ι.app k) x ⊗ₜ[R] (1 : D)
      rw [hclegApply]
    · ext d
      simp [filteredTensorToColimitAlgHom]
  have hB_m :
      compBB.toUnder ≫ FB.map hkm' = idBB.toUnder ≫ FB.map hkm' := by
    have hpath : hkm' = hklB ≫ (hlBl ≫ hlm) := by
      simp only [hkm', hkB, Category.assoc]
    rw [hpath]
    have h := congrArg (fun q ↦ q ≫ FB.map (hlBl ≫ hlm)) hB
    have hmap := FB.map_comp hklB (hlBl ≫ hlm)
    dsimp only [FB, tB, Functor.comp, CommRingCat.tensorProd] at hmap h ⊢
    simp only [Category.assoc] at h
    rw [← hmap] at h
    exact h
  have hD_m :
      compDD.toUnder ≫ FD.map hkm' = idDD.toUnder ≫ FD.map hkm' := by
    have hpath : hkm' = hklD ≫ (hlDl ≫ hlm) := by
      rw [show hkm' = hkD ≫ hlm from hkm]
      simp only [hkD, Category.assoc]
    rw [hpath]
    have h := congrArg (fun q ↦ q ≫ FD.map (hlDl ≫ hlm)) hD
    have hmap := FD.map_comp hklD (hlDl ≫ hlm)
    dsimp only [FD, tD, Functor.comp, CommRingCat.tensorProd] at hmap h ⊢
    simp only [Category.assoc] at h
    rw [← hmap] at h
    exact h
  exact ⟨m, hkm', hB_m, hD_m, hcTensorB, hcTensorD⟩

theorem

exists_tensorProduct_algEquiv_stage_of_filteredColimit

L576 ↗

EtaleFundamentalGroups.exists_tensorProduct_algEquiv_stage_of_filteredColimit

Documentation

An equivalence between two fixed finitely presented algebras after base change to a filtered colimit already exists at one finite stage.

Both displayed equalities use the literal tensor maps induced by the cocone, so the descended equivalence and its inverse recover the supplied equivalence at the colimit. In particular every distinguished coordinate in B or D is preserved without an additional comparison hypothesis.

This endpoint deliberately uses one universe for the rings and the filtered index category. That is the universe in which Mathlib currently exposes CommRingCat.isFinitelyPresentable_under; applications with a larger index universe must first choose an equivalent small filtered presentation.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u
local instance underCommRingCatAlgebraDescent
    {R : Type u} [CommRing R] (A : Under (CommRingCat.of R)) : Algebra R A :=
  RingHom.toAlgebra A.hom.hom

Lean source · statement

theorem exists_tensorProduct_algEquiv_stage_of_filteredColimit
    {R B D : Type u} [CommRing R] [CommRing B] [CommRing D]
    [Algebra R B] [Algebra R D]
    [Algebra.FinitePresentation R B]
    [Algebra.FinitePresentation R D]
    {J : Type u} [SmallCategory J] [IsFiltered J]
    (F : J ⥤ Under (CommRingCat.of R))
    (c : Cocone F) (hc : IsColimit c)
    (e : (c.pt ⊗[R] B) ≃ₐ[c.pt] (c.pt ⊗[R] D)) :
    ∃ (i : J)
      (eᵢ : (F.obj i ⊗[R] B) ≃ₐ[F.obj i] (F.obj i ⊗[R] D)),
      (filteredTensorToColimitAlgHom c i (A := D)).comp
          (eᵢ.toAlgHom.restrictScalars R) =
        (e.toAlgHom.restrictScalars R).comp
          (filteredTensorToColimitAlgHom c i (A := B)) ∧
      (filteredTensorToColimitAlgHom c i (A := B)).comp
          (eᵢ.symm.toAlgHom.restrictScalars R) =
        (e.symm.toAlgHom.restrictScalars R).comp
          (filteredTensorToColimitAlgHom c i (A := D))

theorem

exists_tensorProduct_family_eq_stage_of_filteredColimit

L838 ↗

EtaleFundamentalGroups.exists_tensorProduct_family_eq_stage_of_filteredColimit

Documentation

A finite family of equalities after tensor passage to the filtered colimit holds after one common stage transition. The auxiliary source is a polynomial algebra in finitely many variables over the fixed tensor factor; no finite presentation of that fixed factor over the original base is used.

Source context 6 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
open scoped TensorProduct
namespace EtaleFundamentalGroups
universe u
local instance underCommRingCatAlgebraDescent
    {R : Type u} [CommRing R] (A : Under (CommRingCat.of R)) : Algebra R A :=
  RingHom.toAlgebra A.hom.hom

Lean source · statement

theorem exists_tensorProduct_family_eq_stage_of_filteredColimit
    {R B : Type u} [CommRing R] [CommRing B] [Algebra R B]
    {J : Type u} [SmallCategory J] [IsFiltered J]
    (F : J ⥤ Under (CommRingCat.of R))
    (c : Cocone F) (hc : IsColimit c) (k : J)
    {ι : Type*} [Finite ι] (x y : ι → (F.obj k ⊗[R] B))
    (hxy : ∀ a, filteredTensorToColimitAlgHom c k (x a) =
      filteredTensorToColimitAlgHom c k (y a)) :
    ∃ (l : J) (u : k ⟶ l), ∀ a,
      Algebra.TensorProduct.map (CommRingCat.toAlgHom (F.map u)) (AlgHom.id R B) (x a) =
        Algebra.TensorProduct.map (CommRingCat.toAlgHom (F.map u)) (AlgHom.id R B) (y a)

Module documentation

Descending tensor-product equivalences from filtered colimits

Declarations