Module

Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation

26 declarations indexed from sourceView source ↗

Module documentation

Descend a finitely presented module to a stage of a direct limit.

Imports18

Mathlib.Algebra.Module.FinitePresentation
Mathlib.RingTheory.PicardGroup
Mathlib.Algebra.Colimit.Module
Mathlib.LinearAlgebra.TensorProduct.DirectLimit
Mathlib.LinearAlgebra.TensorProduct.Map
Mathlib.LinearAlgebra.TensorProduct.RightExactness
Mathlib.LinearAlgebra.TensorProduct.Pi
Mathlib.LinearAlgebra.TensorProduct.Quotient
Mathlib.LinearAlgebra.TensorProduct.Tower
Mathlib.RingTheory.TensorProduct.Basic
Mathlib.RingTheory.TensorProduct.Finite
Mathlib.RingTheory.Finiteness.Defs
Mathlib.RingTheory.Finiteness.Basic
Mathlib.LinearAlgebra.Finsupp.LinearCombination
Mathlib.LinearAlgebra.Pi
Mathlib.Data.Finset.Order
Mathlib.Order.DirectedInverseSystem
Mathlib.Tactic.Choose

Imported by2

theorem

rTensor_algHom_smul

L50 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation.S17LFP.rTensor_algHom_smul

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation
open TensorProduct
namespace S17LFP
section Helpers
variable {R : Type*} [CommRing R] {S T : Type*} [CommRing S] [CommRing T] [Algebra R S] [Algebra
    R T]

Lean source · statement

theorem rTensor_algHom_smul (σ : S →ₐ[R] T) (Q : Type*) [AddCommGroup Q] [Module R Q]
    (b : S) (z : S ⊗[R] Q) :
    σ.toLinearMap.rTensor Q (b • z) = σ b • σ.toLinearMap.rTensor Q z

theorem

ext_one_tmul

L57 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation.S17LFP.ext_one_tmul

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation
open TensorProduct
namespace S17LFP
section Helpers
variable {R : Type*} [CommRing R] {S T : Type*} [CommRing S] [CommRing T] [Algebra R S] [Algebra
    R T]

Lean source · statement

theorem ext_one_tmul {P N : Type*} [AddCommGroup P] [Module R P] [AddCommGroup N] [Module R N]
    [Module S N] [IsScalarTower R S N]
    {f₁ f₂ : S ⊗[R] P →ₗ[S] N} (h : ∀ p, f₁ (1 ⊗ₜ p) = f₂ (1 ⊗ₜ p)) : f₁ = f₂

theorem

rTensor_comp_apply_tmul

L65 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation.S17LFP.rTensor_comp_apply_tmul

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation
open TensorProduct
namespace S17LFP
section Helpers
variable {R : Type*} [CommRing R] {S T : Type*} [CommRing S] [CommRing T] [Algebra R S] [Algebra
    R T]

Lean source · statement

theorem rTensor_comp_apply_tmul (σ : S →ₐ[R] T) {P Q : Type*} [AddCommGroup P] [Module R P]
    [AddCommGroup Q] [Module R Q] (ξ : S ⊗[R] P →ₗ[S] S ⊗[R] Q) (b : S) (p : P) :
    (σ.toLinearMap.rTensor Q ∘ₗ ξ.restrictScalars R) (b ⊗ₜ p) =
      σ b • σ.toLinearMap.rTensor Q (ξ (1 ⊗ₜ p))

theorem

comp_rTensor_apply_tmul

L72 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation.S17LFP.comp_rTensor_apply_tmul

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation
open TensorProduct
namespace S17LFP
section Helpers
variable {R : Type*} [CommRing R] {S T : Type*} [CommRing S] [CommRing T] [Algebra R S] [Algebra
    R T]

Lean source · statement

theorem comp_rTensor_apply_tmul (σ : S →ₐ[R] T) {P N : Type*} [AddCommGroup P] [Module R P]
    [AddCommGroup N] [Module R N] [Module T N] [IsScalarTower R T N]
    (ξ : T ⊗[R] P →ₗ[T] N) (b : S) (p : P) :
    (ξ.restrictScalars R ∘ₗ σ.toLinearMap.rTensor P) (b ⊗ₜ p) = σ b • ξ (1 ⊗ₜ p)

theorem

rTensor_liftBaseChange_tmul

L80 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation.S17LFP.rTensor_liftBaseChange_tmul

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation
open TensorProduct
namespace S17LFP
section Helpers
variable {R : Type*} [CommRing R] {S T : Type*} [CommRing S] [CommRing T] [Algebra R S] [Algebra
    R T]

Lean source · statement

theorem rTensor_liftBaseChange_tmul (σ : S →ₐ[R] T) {P Q : Type*} [AddCommGroup P] [Module R P]
    [AddCommGroup Q] [Module R Q] (u : P →ₗ[R] S ⊗[R] Q) (b : S) (p : P) :
    σ.toLinearMap.rTensor Q (u.liftBaseChange S (b ⊗ₜ p)) = σ b • σ.toLinearMap.rTensor Q (u p)

theorem

finitePresentation_tensorProduct

L86 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation.S17LFP.finitePresentation_tensorProduct

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation
open TensorProduct
namespace S17LFP
section Helpers
variable {R : Type*} [CommRing R] {S T : Type*} [CommRing S] [CommRing T] [Algebra R S] [Algebra
    R T]

Lean source · statement

theorem finitePresentation_tensorProduct (M N : Type*) [AddCommGroup M] [Module R M]
    [AddCommGroup N] [Module R N] [Module.FinitePresentation R M] [Module.FinitePresentation R N] :
    Module.FinitePresentation R (M ⊗[R] N)

theorem

exists_ge_ge

L111 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation.S17LFP.exists_ge_ge

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation
open TensorProduct
namespace S17LFP
section Cocone
variable {R : Type*} [CommRing R] {ι : Type*} [Preorder ι] [Nonempty ι] [IsDirectedOrder ι]
  {G : ι → Type*} [∀ i, AddCommGroup (G i)] [∀ i, Module R (G i)]
  (t : ∀ i j, i ≤ j → G i →ₗ[R] G j)
  {A : Type*} [AddCommGroup A] [Module R A] (ψ : ∀ i, G i →ₗ[R] A)
omit [Nonempty ι] in

Lean source · statement

theorem exists_ge_ge (i j : ι) : ∃ k, i ≤ k ∧ j ≤ k

theorem

cocone_rTensor_surj

L113 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation.S17LFP.cocone_rTensor_surj

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation
open TensorProduct
namespace S17LFP
section Cocone
variable {R : Type*} [CommRing R] {ι : Type*} [Preorder ι] [Nonempty ι] [IsDirectedOrder ι]
  {G : ι → Type*} [∀ i, AddCommGroup (G i)] [∀ i, Module R (G i)]
  (t : ∀ i j, i ≤ j → G i →ₗ[R] G j)
  {A : Type*} [AddCommGroup A] [Module R A] (ψ : ∀ i, G i →ₗ[R] A)
omit [Nonempty ι] in

Lean source · statement

theorem cocone_rTensor_surj (hψ : ∀ i j (h : i ≤ j) x, ψ j (t i j h x) = ψ i x)
    (hsurj : ∀ a, ∃ i x, ψ i x = a) (Q : Type*) [AddCommGroup Q] [Module R Q]
    (z : A ⊗[R] Q) : ∃ (i : ι) (x : G i ⊗[R] Q), (ψ i).rTensor Q x = z

theorem

lift_bijective

L129 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation.S17LFP.lift_bijective

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation
open TensorProduct
namespace S17LFP
section Cocone
variable {R : Type*} [CommRing R] {ι : Type*} [Preorder ι] [Nonempty ι] [IsDirectedOrder ι]
  {G : ι → Type*} [∀ i, AddCommGroup (G i)] [∀ i, Module R (G i)]
  (t : ∀ i j, i ≤ j → G i →ₗ[R] G j)
  {A : Type*} [AddCommGroup A] [Module R A] (ψ : ∀ i, G i →ₗ[R] A)

Lean source · statement

theorem lift_bijective [DecidableEq ι] (hψ : ∀ i j (h : i ≤ j) x, ψ j (t i j h x) = ψ i x)
    (hsurj : ∀ a, ∃ i x, ψ i x = a)
    (hzero : ∀ i x, ψ i x = 0 → ∃ (j : ι) (h : i ≤ j), t i j h x = 0) :
    Function.Bijective (Module.DirectLimit.lift R ι G t ψ hψ)

theorem

cocone_rTensor_zero

L144 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation.S17LFP.cocone_rTensor_zero

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation
open TensorProduct
namespace S17LFP
section Cocone
variable {R : Type*} [CommRing R] {ι : Type*} [Preorder ι] [Nonempty ι] [IsDirectedOrder ι]
  {G : ι → Type*} [∀ i, AddCommGroup (G i)] [∀ i, Module R (G i)]
  (t : ∀ i j, i ≤ j → G i →ₗ[R] G j)
  {A : Type*} [AddCommGroup A] [Module R A] (ψ : ∀ i, G i →ₗ[R] A)

Lean source · statement

theorem cocone_rTensor_zero [DirectedSystem G (t · · ·)]
    (hψ : ∀ i j (h : i ≤ j) x, ψ j (t i j h x) = ψ i x)
    (hsurj : ∀ a, ∃ i x, ψ i x = a)
    (hzero : ∀ i x, ψ i x = 0 → ∃ (j : ι) (h : i ≤ j), t i j h x = 0)
    (Q : Type*) [AddCommGroup Q] [Module R Q] (i : ι) (x : G i ⊗[R] Q)
    (hx : (ψ i).rTensor Q x = 0) : ∃ (j : ι) (h : i ≤ j), (t i j h).rTensor Q x = 0

theorem

exists_comp_eq_of_finite

L163 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation.S17LFP.exists_comp_eq_of_finite

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation
open TensorProduct
namespace S17LFP
section Cocone
variable {R : Type*} [CommRing R] {ι : Type*} [Preorder ι] [Nonempty ι] [IsDirectedOrder ι]
  {G : ι → Type*} [∀ i, AddCommGroup (G i)] [∀ i, Module R (G i)]
  (t : ∀ i j, i ≤ j → G i →ₗ[R] G j)
  {A : Type*} [AddCommGroup A] [Module R A] (ψ : ∀ i, G i →ₗ[R] A)

Lean source · statement

theorem exists_comp_eq_of_finite [DirectedSystem G (t · · ·)]
    (hzero : ∀ i x, ψ i x = 0 → ∃ (j : ι) (h : i ≤ j), t i j h x = 0)
    {M : Type*} [AddCommGroup M] [Module R M] [Module.Finite R M]
    {i : ι} (u v : M →ₗ[R] G i) (huv : ψ i ∘ₗ u = ψ i ∘ₗ v) :
    ∃ (j : ι) (hij : i ≤ j), t i j hij ∘ₗ u = t i j hij ∘ₗ v

theorem

exists_factor_of_finitePresentation

L186 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation.S17LFP.exists_factor_of_finitePresentation

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation
open TensorProduct
namespace S17LFP
section Cocone
variable {R : Type*} [CommRing R] {ι : Type*} [Preorder ι] [Nonempty ι] [IsDirectedOrder ι]
  {G : ι → Type*} [∀ i, AddCommGroup (G i)] [∀ i, Module R (G i)]
  (t : ∀ i j, i ≤ j → G i →ₗ[R] G j)
  {A : Type*} [AddCommGroup A] [Module R A] (ψ : ∀ i, G i →ₗ[R] A)

Lean source · statement

theorem exists_factor_of_finitePresentation [DirectedSystem G (t · · ·)]
    (hψ : ∀ i j (h : i ≤ j) x, ψ j (t i j h x) = ψ i x)
    (hsurj : ∀ a, ∃ i x, ψ i x = a)
    (hzero : ∀ i x, ψ i x = 0 → ∃ (j : ι) (h : i ≤ j), t i j h x = 0)
    {M : Type*} [AddCommGroup M] [Module R M] [Module.FinitePresentation R M]
    (φ : M →ₗ[R] A) : ∃ (i : ι) (u : M →ₗ[R] G i), ψ i ∘ₗ u = φ

theorem

directedSystem_linear

L239 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation.S17LFP.directedSystem_linear

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation
open TensorProduct
namespace S17LFP
section Descent
universe u v w
variable {ι : Type v} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]
  {B₀ : Type u} [CommRing B₀]
  (B : ι → Type u) [∀ i, CommRing (B i)] [∀ i, Algebra B₀ (B i)]
  (τ : ∀ i j, i ≤ j → B i →ₐ[B₀] B j) [DirectedSystem B (fun i j h => τ i j h)]
  (Bω : Type u) [CommRing Bω] [Algebra B₀ Bω] (g : ∀ i, B i →ₐ[B₀] Bω)
  (hg : ∀ i j (h : i ≤ j), (g j).comp (τ i j h) = g i)
  (hsurj : ∀ b : Bω, ∃ i x, g i x = b)
  (hzero : ∀ i (x : B i), g i x = 0 → ∃ (j : ι) (h : i ≤ j), τ i j h x = 0)
  (P Q : Type*) [AddCommGroup P] [Module B₀ P] [AddCommGroup Q] [Module B₀ Q]
omit [IsDirectedOrder ι] [Nonempty ι] in

Lean source · full declaration

theorem directedSystem_linear : DirectedSystem B (fun i j h => (τ i j h).toLinearMap) :=
  ⟨fun _ x => DirectedSystem.map_self (f := fun i j h => ⇑(τ i j h)) x,
    fun _ _ _ h₁ h₂ x => DirectedSystem.map_map (f := fun i j h => ⇑(τ i j h)) h₁ h₂ x⟩

theorem

rTensor_self

L243 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation.S17LFP.rTensor_self

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation
open TensorProduct
namespace S17LFP
section Descent
universe u v w
variable {ι : Type v} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]
  {B₀ : Type u} [CommRing B₀]
  (B : ι → Type u) [∀ i, CommRing (B i)] [∀ i, Algebra B₀ (B i)]
  (τ : ∀ i j, i ≤ j → B i →ₐ[B₀] B j) [DirectedSystem B (fun i j h => τ i j h)]
  (Bω : Type u) [CommRing Bω] [Algebra B₀ Bω] (g : ∀ i, B i →ₐ[B₀] Bω)
  (hg : ∀ i j (h : i ≤ j), (g j).comp (τ i j h) = g i)
  (hsurj : ∀ b : Bω, ∃ i x, g i x = b)
  (hzero : ∀ i (x : B i), g i x = 0 → ∃ (j : ι) (h : i ≤ j), τ i j h x = 0)
  (P Q : Type*) [AddCommGroup P] [Module B₀ P] [AddCommGroup Q] [Module B₀ Q]
omit [IsDirectedOrder ι] [Nonempty ι] in

Lean source · statement

theorem rTensor_self (i : ι) {M : Type*} [AddCommGroup M] [Module B₀ M] (z : B i ⊗[B₀] M) :
    (τ i i le_rfl).toLinearMap.rTensor M z = z

theorem

glin_comp

L253 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation.S17LFP.glin_comp

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation
open TensorProduct
namespace S17LFP
section Descent
universe u v w
variable {ι : Type v} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]
  {B₀ : Type u} [CommRing B₀]
  (B : ι → Type u) [∀ i, CommRing (B i)] [∀ i, Algebra B₀ (B i)]
  (τ : ∀ i j, i ≤ j → B i →ₐ[B₀] B j) [DirectedSystem B (fun i j h => τ i j h)]
  (Bω : Type u) [CommRing Bω] [Algebra B₀ Bω] (g : ∀ i, B i →ₐ[B₀] Bω)
  (hg : ∀ i j (h : i ≤ j), (g j).comp (τ i j h) = g i)
  (hsurj : ∀ b : Bω, ∃ i x, g i x = b)
  (hzero : ∀ i (x : B i), g i x = 0 → ∃ (j : ι) (h : i ≤ j), τ i j h x = 0)
  (P Q : Type*) [AddCommGroup P] [Module B₀ P] [AddCommGroup Q] [Module B₀ Q]
omit [DirectedSystem B (fun i j h => τ i j h)] [IsDirectedOrder ι] [Nonempty ι] in
include hg in

Lean source · statement

theorem glin_comp (k l : ι) (h : k ≤ l) :
    (g l).toLinearMap ∘ₗ (τ k l h).toLinearMap = (g k).toLinearMap

theorem

glin_compat

L258 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation.S17LFP.glin_compat

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation
open TensorProduct
namespace S17LFP
section Descent
universe u v w
variable {ι : Type v} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]
  {B₀ : Type u} [CommRing B₀]
  (B : ι → Type u) [∀ i, CommRing (B i)] [∀ i, Algebra B₀ (B i)]
  (τ : ∀ i j, i ≤ j → B i →ₐ[B₀] B j) [DirectedSystem B (fun i j h => τ i j h)]
  (Bω : Type u) [CommRing Bω] [Algebra B₀ Bω] (g : ∀ i, B i →ₐ[B₀] Bω)
  (hg : ∀ i j (h : i ≤ j), (g j).comp (τ i j h) = g i)
  (hsurj : ∀ b : Bω, ∃ i x, g i x = b)
  (hzero : ∀ i (x : B i), g i x = 0 → ∃ (j : ι) (h : i ≤ j), τ i j h x = 0)
  (P Q : Type*) [AddCommGroup P] [Module B₀ P] [AddCommGroup Q] [Module B₀ Q]
omit [DirectedSystem B (fun i j h => τ i j h)] [IsDirectedOrder ι] [Nonempty ι] in
include hg in

Lean source · statement

theorem glin_compat : ∀ k l (h : k ≤ l) (x : B k),
    (g l).toLinearMap ((τ k l h).toLinearMap x) = (g k).toLinearMap x

theorem

gQ_compat

L263 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation.S17LFP.gQ_compat

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation
open TensorProduct
namespace S17LFP
section Descent
universe u v w
variable {ι : Type v} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]
  {B₀ : Type u} [CommRing B₀]
  (B : ι → Type u) [∀ i, CommRing (B i)] [∀ i, Algebra B₀ (B i)]
  (τ : ∀ i j, i ≤ j → B i →ₐ[B₀] B j) [DirectedSystem B (fun i j h => τ i j h)]
  (Bω : Type u) [CommRing Bω] [Algebra B₀ Bω] (g : ∀ i, B i →ₐ[B₀] Bω)
  (hg : ∀ i j (h : i ≤ j), (g j).comp (τ i j h) = g i)
  (hsurj : ∀ b : Bω, ∃ i x, g i x = b)
  (hzero : ∀ i (x : B i), g i x = 0 → ∃ (j : ι) (h : i ≤ j), τ i j h x = 0)
  (P Q : Type*) [AddCommGroup P] [Module B₀ P] [AddCommGroup Q] [Module B₀ Q]
omit [DirectedSystem B (fun i j h => τ i j h)] [IsDirectedOrder ι] [Nonempty ι] in
include hg in

Lean source · statement

theorem gQ_compat (Q : Type*) [AddCommGroup Q] [Module B₀ Q] : ∀ k l (h : k ≤ l) (x : B k ⊗[B₀] Q),
    (g l).toLinearMap.rTensor Q ((τ k l h).toLinearMap.rTensor Q x) = (g k).toLinearMap.rTensor
      Q x

theorem

gQ_surj

L271 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation.S17LFP.gQ_surj

Source context 11 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation
open TensorProduct
namespace S17LFP
section Descent
universe u v w
variable {ι : Type v} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]
  {B₀ : Type u} [CommRing B₀]
  (B : ι → Type u) [∀ i, CommRing (B i)] [∀ i, Algebra B₀ (B i)]
  (τ : ∀ i j, i ≤ j → B i →ₐ[B₀] B j) [DirectedSystem B (fun i j h => τ i j h)]
  (Bω : Type u) [CommRing Bω] [Algebra B₀ Bω] (g : ∀ i, B i →ₐ[B₀] Bω)
  (hg : ∀ i j (h : i ≤ j), (g j).comp (τ i j h) = g i)
  (hsurj : ∀ b : Bω, ∃ i x, g i x = b)
  (hzero : ∀ i (x : B i), g i x = 0 → ∃ (j : ι) (h : i ≤ j), τ i j h x = 0)
  (P Q : Type*) [AddCommGroup P] [Module B₀ P] [AddCommGroup Q] [Module B₀ Q]
include hg hsurj in
omit [DirectedSystem B (fun i j h => τ i j h)] in
omit [Nonempty ι] in

Lean source · statement

theorem gQ_surj (Q : Type*) [AddCommGroup Q] [Module B₀ Q] :
    ∀ z : Bω ⊗[B₀] Q, ∃ (i : ι) (x : B i ⊗[B₀] Q), (g i).toLinearMap.rTensor Q x = z

theorem

gQ_zero

L276 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation.S17LFP.gQ_zero

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation
open TensorProduct
namespace S17LFP
section Descent
universe u v w
variable {ι : Type v} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]
  {B₀ : Type u} [CommRing B₀]
  (B : ι → Type u) [∀ i, CommRing (B i)] [∀ i, Algebra B₀ (B i)]
  (τ : ∀ i j, i ≤ j → B i →ₐ[B₀] B j) [DirectedSystem B (fun i j h => τ i j h)]
  (Bω : Type u) [CommRing Bω] [Algebra B₀ Bω] (g : ∀ i, B i →ₐ[B₀] Bω)
  (hg : ∀ i j (h : i ≤ j), (g j).comp (τ i j h) = g i)
  (hsurj : ∀ b : Bω, ∃ i x, g i x = b)
  (hzero : ∀ i (x : B i), g i x = 0 → ∃ (j : ι) (h : i ≤ j), τ i j h x = 0)
  (P Q : Type*) [AddCommGroup P] [Module B₀ P] [AddCommGroup Q] [Module B₀ Q]
include hg hsurj hzero in

Lean source · statement

theorem gQ_zero (Q : Type*) [AddCommGroup Q] [Module B₀ Q] :
    ∀ (i : ι) (x : B i ⊗[B₀] Q), (g i).toLinearMap.rTensor Q x = 0 →
      ∃ (j : ι) (h : i ≤ j), (τ i j h).toLinearMap.rTensor Q x = 0

theorem

hom_inj

L283 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation.S17LFP.hom_inj

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation
open TensorProduct
namespace S17LFP
section Descent
universe u v w
variable {ι : Type v} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]
  {B₀ : Type u} [CommRing B₀]
  (B : ι → Type u) [∀ i, CommRing (B i)] [∀ i, Algebra B₀ (B i)]
  (τ : ∀ i j, i ≤ j → B i →ₐ[B₀] B j) [DirectedSystem B (fun i j h => τ i j h)]
  (Bω : Type u) [CommRing Bω] [Algebra B₀ Bω] (g : ∀ i, B i →ₐ[B₀] Bω)
  (hg : ∀ i j (h : i ≤ j), (g j).comp (τ i j h) = g i)
  (hsurj : ∀ b : Bω, ∃ i x, g i x = b)
  (hzero : ∀ i (x : B i), g i x = 0 → ∃ (j : ι) (h : i ≤ j), τ i j h x = 0)
  (P Q : Type*) [AddCommGroup P] [Module B₀ P] [AddCommGroup Q] [Module B₀ Q]
include hg hsurj hzero in

Lean source · statement

theorem hom_inj [Module.Finite B₀ P] (i : ι) (φ φ' : B i ⊗[B₀] P →ₗ[B i] B i ⊗[B₀] Q)
    (h : (g i).toLinearMap.rTensor Q ∘ₗ φ.restrictScalars B₀ =
      (g i).toLinearMap.rTensor Q ∘ₗ φ'.restrictScalars B₀) :
    ∃ (j : ι) (h : i ≤ j),
      (τ i j h).toLinearMap.rTensor Q ∘ₗ φ.restrictScalars B₀ =
        (τ i j h).toLinearMap.rTensor Q ∘ₗ φ'.restrictScalars B₀

theorem

hom_surj

L302 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation.S17LFP.hom_surj

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation
open TensorProduct
namespace S17LFP
section Descent
universe u v w
variable {ι : Type v} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]
  {B₀ : Type u} [CommRing B₀]
  (B : ι → Type u) [∀ i, CommRing (B i)] [∀ i, Algebra B₀ (B i)]
  (τ : ∀ i j, i ≤ j → B i →ₐ[B₀] B j) [DirectedSystem B (fun i j h => τ i j h)]
  (Bω : Type u) [CommRing Bω] [Algebra B₀ Bω] (g : ∀ i, B i →ₐ[B₀] Bω)
  (hg : ∀ i j (h : i ≤ j), (g j).comp (τ i j h) = g i)
  (hsurj : ∀ b : Bω, ∃ i x, g i x = b)
  (hzero : ∀ i (x : B i), g i x = 0 → ∃ (j : ι) (h : i ≤ j), τ i j h x = 0)
  (P Q : Type*) [AddCommGroup P] [Module B₀ P] [AddCommGroup Q] [Module B₀ Q]
include hg hsurj hzero in

Lean source · statement

theorem hom_surj [Module.FinitePresentation B₀ P] (φ : Bω ⊗[B₀] P →ₗ[Bω] Bω ⊗[B₀] Q) :
    ∃ (i : ι) (φᵢ : B i ⊗[B₀] P →ₗ[B i] B i ⊗[B₀] Q),
      φ.restrictScalars B₀ ∘ₗ (g i).toLinearMap.rTensor P =
        (g i).toLinearMap.rTensor Q ∘ₗ φᵢ.restrictScalars B₀

theorem

iso_desc

L318 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation.S17LFP.iso_desc

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation
open TensorProduct
namespace S17LFP
section Descent
universe u v w
variable {ι : Type v} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]
  {B₀ : Type u} [CommRing B₀]
  (B : ι → Type u) [∀ i, CommRing (B i)] [∀ i, Algebra B₀ (B i)]
  (τ : ∀ i j, i ≤ j → B i →ₐ[B₀] B j) [DirectedSystem B (fun i j h => τ i j h)]
  (Bω : Type u) [CommRing Bω] [Algebra B₀ Bω] (g : ∀ i, B i →ₐ[B₀] Bω)
  (hg : ∀ i j (h : i ≤ j), (g j).comp (τ i j h) = g i)
  (hsurj : ∀ b : Bω, ∃ i x, g i x = b)
  (hzero : ∀ i (x : B i), g i x = 0 → ∃ (j : ι) (h : i ≤ j), τ i j h x = 0)
  (P Q : Type*) [AddCommGroup P] [Module B₀ P] [AddCommGroup Q] [Module B₀ Q]
include hg hsurj hzero in

Lean source · statement

theorem iso_desc [Module.FinitePresentation B₀ P] [Module.FinitePresentation B₀ Q]
    (e : Bω ⊗[B₀] P ≃ₗ[Bω] Bω ⊗[B₀] Q) :
    ∃ (i : ι) (eᵢ : B i ⊗[B₀] P ≃ₗ[B i] B i ⊗[B₀] Q),
      (e : _ →ₗ[Bω] _).restrictScalars B₀ ∘ₗ (g i).toLinearMap.rTensor P =
        (g i).toLinearMap.rTensor Q ∘ₗ (eᵢ : _ →ₗ[B i] _).restrictScalars B₀

theorem

obj

L433 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation.S17LFP.obj

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation
open TensorProduct
namespace S17LFP
section Descent
universe u v w
variable {ι : Type v} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]
  {B₀ : Type u} [CommRing B₀]
  (B : ι → Type u) [∀ i, CommRing (B i)] [∀ i, Algebra B₀ (B i)]
  (τ : ∀ i j, i ≤ j → B i →ₐ[B₀] B j) [DirectedSystem B (fun i j h => τ i j h)]
  (Bω : Type u) [CommRing Bω] [Algebra B₀ Bω] (g : ∀ i, B i →ₐ[B₀] Bω)
  (hg : ∀ i j (h : i ≤ j), (g j).comp (τ i j h) = g i)
  (hsurj : ∀ b : Bω, ∃ i x, g i x = b)
  (hzero : ∀ i (x : B i), g i x = 0 → ∃ (j : ι) (h : i ≤ j), τ i j h x = 0)
  (P Q : Type*) [AddCommGroup P] [Module B₀ P] [AddCommGroup Q] [Module B₀ Q]
omit [DirectedSystem B (fun i j h => τ i j h)] in
include hg hsurj in

Lean source · full declaration

theorem obj (Y : Type w) [AddCommGroup Y] [Module Bω Y] [Module.FinitePresentation Bω Y] :
    ∃ (i : ι) (Pᵢ : Type u) (_ : AddCommGroup Pᵢ) (_ : Module (B i) Pᵢ),
      Module.FinitePresentation (B i) Pᵢ ∧
      Nonempty (letI := (g i).toRingHom.toAlgebra; Bω ⊗[B i] Pᵢ ≃ₗ[Bω] Y) := by
  classical
  obtain ⟨n, K, e, hK⟩ := Module.FinitePresentation.exists_fin Bω Y
  obtain ⟨m, v, hv⟩ := Submodule.fg_iff_exists_fin_generating_family.mp hK
  choose i₀ x₀ hx₀ using fun a : Fin m × Fin n => hsurj (v a.1 a.2)
  obtain ⟨i, hi⟩ := Finset.exists_le (Finset.univ.image i₀)
  have hle : ∀ a, i₀ a ≤ i := fun a => hi _ (Finset.mem_image_of_mem _ (Finset.mem_univ a))
  let y : Fin m → (Fin n → B i) := fun a k => τ (i₀ (a, k)) i (hle _) (x₀ (a, k))
  have hy : ∀ a k, g i (y a k) = v a k := fun a k => by
    simp only [y]
    rw [← AlgHom.comp_apply, hg]
    exact hx₀ (a, k)
  let Kᵢ : Submodule (B i) (Fin n → B i) := Submodule.span (B i) (Set.range y)
  let : Algebra (B i) Bω := (g i).toRingHom.toAlgebra
  have halg : ∀ b : B i, algebraMap (B i) Bω b = g i b := fun b => rfl
  refine ⟨i, (Fin n → B i) ⧸ Kᵢ, inferInstance, inferInstance, ?_, ⟨?_⟩⟩
  · exact Module.finitePresentation_of_surjective Kᵢ.mkQ (Submodule.mkQ_surjective Kᵢ)
      (by rw [Submodule.ker_mkQ]; exact Submodule.fg_span (Set.finite_range y))
  · let π := TensorProduct.piScalarRight (B i) Bω Bω (Fin n)
    refine TensorProduct.AlgebraTensorModule.tensorQuotientEquiv Bω (B i) Bω Kᵢ ≪≫ₗ
      Submodule.Quotient.equiv _ K π ?_ ≪≫ₗ e.symm
    apply le_antisymm
    · rintro _ ⟨x, ⟨w, rfl⟩, rfl⟩
      induction w using TensorProduct.inductionOn with
      | add w₁ w₂ h₁ h₂ => simpa only [map_add] using add_mem h₁ h₂
      | tmul b k =>
        obtain ⟨k, hk⟩ := k
        simp only [TensorProduct.AlgebraTensorModule.lTensor_tmul, LinearMap.restrictScalars_apply,
          Submodule.subtype_apply, LinearEquiv.coe_coe, π, TensorProduct.piScalarRight_apply,
          TensorProduct.piScalarRightHom_tmul]
        induction hk using Submodule.span_induction generalizing b with
        | mem z hz =>
          obtain ⟨a, rfl⟩ := hz
          have : (fun j => y a j • b) = b • v a := by
            funext j
            simp [Algebra.smul_def, halg, hy, mul_comm]
          rw [this, ← hv]
          exact Submodule.smul_mem _ _ (Submodule.subset_span ⟨a, rfl⟩)
        | zero =>
          simp only [Pi.zero_apply, zero_smul]
          exact zero_mem K
        | add z₁ z₂ _ _ h₁ h₂ =>
          have : (fun j => (z₁ + z₂) j • b) = (fun j => z₁ j • b) + (fun j => z₂ j • b) := by
            funext j
            simp [add_smul]
          rw [this]
          exact add_mem (h₁ b) (h₂ b)
        | smul c z _ hz =>
          have : (fun j => (c • z) j • b) = fun j => z j • (c • b) := by
            funext j
            simp [mul_comm c, mul_smul]
          rw [this]
          exact hz _
    · rw [← hv, Submodule.span_le]
      rintro _ ⟨a, rfl⟩
      refine ⟨(1 : Bω) ⊗ₜ y a, ⟨(1 : Bω) ⊗ₜ ⟨y a, Submodule.subset_span ⟨a, rfl⟩⟩, rfl⟩, ?_⟩
      simp only [LinearEquiv.coe_coe, π, TensorProduct.piScalarRight_apply,
        TensorProduct.piScalarRightHom_tmul]
      funext j
      simp [Algebra.smul_def, halg, hy]

theorem

iso_desc_stage

L498 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation.S17LFP.iso_desc_stage

Source context 10 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation
open TensorProduct
namespace S17LFP
section Descent
universe u v w
variable {ι : Type v} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]
  {B₀ : Type u} [CommRing B₀]
  (B : ι → Type u) [∀ i, CommRing (B i)] [∀ i, Algebra B₀ (B i)]
  (τ : ∀ i j, i ≤ j → B i →ₐ[B₀] B j) [DirectedSystem B (fun i j h => τ i j h)]
  (Bω : Type u) [CommRing Bω] [Algebra B₀ Bω] (g : ∀ i, B i →ₐ[B₀] Bω)
  (hg : ∀ i j (h : i ≤ j), (g j).comp (τ i j h) = g i)
  (hsurj : ∀ b : Bω, ∃ i x, g i x = b)
  (hzero : ∀ i (x : B i), g i x = 0 → ∃ (j : ι) (h : i ≤ j), τ i j h x = 0)
  (P Q : Type*) [AddCommGroup P] [Module B₀ P] [AddCommGroup Q] [Module B₀ Q]
omit [Nonempty ι] in
include hg hsurj hzero in

Lean source · full declaration

theorem iso_desc_stage {i : ι} (M N : Type*) [AddCommGroup M] [Module (B i) M]
    [Module.FinitePresentation (B i) M] [AddCommGroup N] [Module (B i) N]
    [Module.FinitePresentation (B i) N]
    (e : letI := (g i).toRingHom.toAlgebra; Bω ⊗[B i] M ≃ₗ[Bω] Bω ⊗[B i] N) :
    ∃ (j : ι) (hij : i ≤ j),
      Nonempty (letI := (τ i j hij).toRingHom.toAlgebra; B j ⊗[B i] M ≃ₗ[B j] B j ⊗[B i] N) := by
  let algω : Algebra (B i) Bω := (g i).toRingHom.toAlgebra
  let ι' := {j : ι // i ≤ j}
  let : Nonempty ι' := ⟨⟨i, le_rfl⟩⟩
  have : IsDirectedOrder ι' := ⟨fun a b => by
    obtain ⟨k, h1, h2⟩ := exists_ge_ge a.1 b.1
    exact ⟨⟨k, a.2.trans h1⟩, h1, h2⟩⟩
  let B' : ι' → Type u := fun j => B j.1
  let algj : ∀ j : ι', Algebra (B i) (B' j) := fun j => (τ i j.1 j.2).toRingHom.toAlgebra
  let τ' : ∀ j k : ι', j ≤ k → B' j →ₐ[B i] B' k := fun j k h =>
    { (τ j.1 k.1 h).toRingHom with
      commutes' := fun b => by
        change τ j.1 k.1 h (τ i j.1 j.2 b) = τ i k.1 k.2 b
        exact DirectedSystem.map_map (f := fun i j h => ⇑(τ i j h)) j.2 h b }
  have : DirectedSystem B' (fun j k h => τ' j k h) :=
    ⟨fun j x => DirectedSystem.map_self (f := fun i j h => ⇑(τ i j h)) x,
     fun a b c h1 h2 x => DirectedSystem.map_map (f := fun i j h => ⇑(τ i j h)) h1 h2 x⟩
  let g' : ∀ j : ι', B' j →ₐ[B i] Bω := fun j =>
    { (g j.1).toRingHom with
      commutes' := fun b => by
        change g j.1 (τ i j.1 j.2 b) = g i b
        rw [← AlgHom.comp_apply, hg] }
  have hg' : ∀ j k (h : j ≤ k), (g' k).comp (τ' j k h) = g' j := fun j k h =>
    AlgHom.ext fun x => by
      change g k.1 (τ j.1 k.1 h x) = g j.1 x
      rw [← AlgHom.comp_apply, hg]
  have hsurj' : ∀ b : Bω, ∃ j x, g' j x = b := fun b => by
    obtain ⟨i₁, x, rfl⟩ := hsurj b
    obtain ⟨k, h1, h2⟩ := exists_ge_ge i i₁
    refine ⟨⟨k, h1⟩, τ i₁ k h2 x, ?_⟩
    change g k (τ i₁ k h2 x) = g i₁ x
    rw [← AlgHom.comp_apply, hg]
  have hzero' : ∀ j (x : B' j), g' j x = 0 → ∃ (k : ι') (h : j ≤ k), τ' j k h x = 0 :=
    fun j x hx => by
      obtain ⟨k, hjk, hk⟩ := hzero j.1 x hx
      exact ⟨⟨k, j.2.trans hjk⟩, hjk, hk⟩
  obtain ⟨j, eⱼ, -⟩ := iso_desc B' τ' Bω g' hg' hsurj' hzero' M N e
  exact ⟨j.1, j.2, ⟨eⱼ⟩⟩

theorem

inv_desc

L542 ↗

AlgebraicCurves.Foundations.Algebra.Proofs.Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation.S17LFP.inv_desc

Source context 9 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation
open TensorProduct
namespace S17LFP
section Descent
universe u v w
variable {ι : Type v} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]
  {B₀ : Type u} [CommRing B₀]
  (B : ι → Type u) [∀ i, CommRing (B i)] [∀ i, Algebra B₀ (B i)]
  (τ : ∀ i j, i ≤ j → B i →ₐ[B₀] B j) [DirectedSystem B (fun i j h => τ i j h)]
  (Bω : Type u) [CommRing Bω] [Algebra B₀ Bω] (g : ∀ i, B i →ₐ[B₀] Bω)
  (hg : ∀ i j (h : i ≤ j), (g j).comp (τ i j h) = g i)
  (hsurj : ∀ b : Bω, ∃ i x, g i x = b)
  (hzero : ∀ i (x : B i), g i x = 0 → ∃ (j : ι) (h : i ≤ j), τ i j h x = 0)
  (P Q : Type*) [AddCommGroup P] [Module B₀ P] [AddCommGroup Q] [Module B₀ Q]
include hg hsurj hzero in

Lean source · statement

theorem inv_desc [Module.FinitePresentation B₀ P] [Module.Invertible Bω (Bω ⊗[B₀] P)] :
    ∃ i : ι, Module.Invertible (B i) (B i ⊗[B₀] P)

theorem

exists_linearEquiv_of_finitePresentation

L580 ↗

Module.IsDirectLimit.exists_linearEquiv_of_finitePresentation

Source context 5 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.Algebra.Proofs
namespace Module_IsDirectLimit_exists_linearEquiv_of_finitePresentation
open TensorProduct
universe u v w

Lean source · full declaration

theorem _root_.Module.IsDirectLimit.exists_linearEquiv_of_finitePresentation
    {ι : Type v} [Preorder ι] [IsDirectedOrder ι] [Nonempty ι]
    {B₀ : Type u} [CommRing B₀]
    (B : ι → Type u) [∀ i, CommRing (B i)] [∀ i, Algebra B₀ (B i)]
    (τ : ∀ i j, i ≤ j → B i →ₐ[B₀] B j) [DirectedSystem B (fun i j h => τ i j h)]
    (Bω : Type u) [CommRing Bω] [Algebra B₀ Bω] (g : ∀ i, B i →ₐ[B₀] Bω)
    (hg : ∀ i j (h : i ≤ j), (g j).comp (τ i j h) = g i)
    (hsurj : ∀ b : Bω, ∃ i x, g i x = b)
    (hzero : ∀ i (x : B i), g i x = 0 → ∃ (j : ι) (h : i ≤ j), τ i j h x = 0)
    (P Q : Type w) [AddCommGroup P] [Module B₀ P] [AddCommGroup Q] [Module B₀ Q]
    [Module.FinitePresentation B₀ P] [Module.FinitePresentation B₀ Q]
    (e : TensorProduct B₀ Bω P ≃ₗ[Bω] TensorProduct B₀ Bω Q) :
    ∃ (i : ι) (eᵢ : TensorProduct B₀ (B i) P ≃ₗ[B i] TensorProduct B₀ (B i) Q),
      (e : _ →ₗ[Bω] _).restrictScalars B₀ ∘ₗ (g i).toLinearMap.rTensor P =
        (g i).toLinearMap.rTensor Q ∘ₗ (eᵢ : _ →ₗ[B i] _).restrictScalars B₀ :=
  S17LFP.iso_desc B τ Bω g hg hsurj hzero P Q e

Module documentation

Declarations