NYLL
Module

Mathlib_Algebra_IsDirectLimit.lean

Nyll.AlgebraicCurves.Foundations.Algebra.Mathlib_Algebra_IsDirectLimit
20 declarations indexed from sourceView source ↗

Module documentation

Mathlib Algebra Is Direct Limit

Imports4
  • Mathlib.Algebra.Colimit.Module
  • Mathlib.Tactic.ApplyFun
  • Mathlib.Tactic.MkIffOfInductiveProp
  • Mathlib.Tactic.SimpRw
Imported by21

Declarations

class

IsDirectLimit

L33 ↗
Documentation

The cocone realizes a direct limit: every element lifts and equal lifts eventually agree.

Source context 2 commands

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

section
variable {ι : Type*} [Preorder ι] {M : ι → Type*} {P : Type*}
  (f : (i j : ι) → (h : i ≤ j) → M i → M j) (g : ∀ i, M i → P)
Lean source · full declaration
class IsDirectLimit [DirectedSystem M f] : Prop where
  /-- Every element has a representative at some stage. -/
  surj : ∀ m : P, ∃ i, ∃ mi : M i, g i mi = m
  /-- Representatives with the same image agree at a common later stage. -/
  inj :  ∀ i j, ∀ mi : M i, ∀ mj : M j, g i mi = g j mj → ∃ (k : ι) (hik : i ≤ k) (hjk : j ≤ k),
      f i k hik mi = f j k hjk mj
  /-- The cocone maps commute with the transition maps. -/
  compatibility : ∀ i j hij x, g j (f i j hij x) = g i x
theorem

compatibility'

L46 ↗
IsDirectLimit.compatibility'
Source context 4 commands

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

section
variable {ι : Type*} [Preorder ι] {M : ι → Type*} {P : Type*}
  (f : (i j : ι) → (h : i ≤ j) → M i → M j) (g : ∀ i, M i → P)
variable [DirectedSystem M f] [IsDirectLimit f g]
namespace IsDirectLimit
Lean source · statement
theorem compatibility' {i j hij} (x : M i) : g j (f i j hij x) = g i x
theorem

is_injective

L49 ↗
IsDirectLimit.is_injective
Source context 4 commands

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

section
variable {ι : Type*} [Preorder ι] {M : ι → Type*} {P : Type*}
  (f : (i j : ι) → (h : i ≤ j) → M i → M j) (g : ∀ i, M i → P)
variable [DirectedSystem M f] [IsDirectLimit f g]
namespace IsDirectLimit
Lean source · statement
theorem is_injective {i j} {mi : M i} {mj : M j} (h : g i mi = g j mj) :
    ∃ (k : ι) (hik : i ≤ k) (hjk : j ≤ k), f i k hik mi = f j k hjk mj
theorem

is_surjective

L54 ↗
IsDirectLimit.is_surjective
Source context 5 commands

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

section
variable {ι : Type*} [Preorder ι] {M : ι → Type*} {P : Type*}
  (f : (i j : ι) → (h : i ≤ j) → M i → M j) (g : ∀ i, M i → P)
variable [DirectedSystem M f] [IsDirectLimit f g]
namespace IsDirectLimit
include f in
Lean source · statement
theorem is_surjective : ∀ m : P, ∃ i, ∃ mi : M i, g i mi = m
def

preimage_index

L58 ↗
IsDirectLimit.preimage_index
Documentation

A chosen stage containing a representative of the given direct-limit element.

Source context 4 commands

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

section
variable {ι : Type*} [Preorder ι] {M : ι → Type*} {P : Type*}
  (f : (i j : ι) → (h : i ≤ j) → M i → M j) (g : ∀ i, M i → P)
variable [DirectedSystem M f] [IsDirectLimit f g]
namespace IsDirectLimit
Lean source · statement
def preimage_index (p : P) : ι
def

preimage

L61 ↗
IsDirectLimit.preimage
Documentation

A chosen representative of the element at its chosen stage.

Source context 4 commands

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

section
variable {ι : Type*} [Preorder ι] {M : ι → Type*} {P : Type*}
  (f : (i j : ι) → (h : i ≤ j) → M i → M j) (g : ∀ i, M i → P)
variable [DirectedSystem M f] [IsDirectLimit f g]
namespace IsDirectLimit
Lean source · statement
def preimage (p : P) : M (preimage_index f g p)
theorem

image_preimage

L64 ↗
IsDirectLimit.image_preimage
Source context 4 commands

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

section
variable {ι : Type*} [Preorder ι] {M : ι → Type*} {P : Type*}
  (f : (i j : ι) → (h : i ≤ j) → M i → M j) (g : ∀ i, M i → P)
variable [DirectedSystem M f] [IsDirectLimit f g]
namespace IsDirectLimit
Lean source · statement
theorem image_preimage (p : P) :
    g (preimage_index f g p) (preimage f g p) = p
def

lift

L71 ↗
IsDirectLimit.lift
Documentation

The map from the direct limit induced by a compatible family of maps.

Source context 5 commands

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

section
variable {ι : Type*} [Preorder ι] {M : ι → Type*} {P : Type*}
  (f : (i j : ι) → (h : i ≤ j) → M i → M j) (g : ∀ i, M i → P)
variable [DirectedSystem M f] [IsDirectLimit f g]
namespace IsDirectLimit
variable {P₁ P₂ : Type*} (g₁ : ∀ i, M i → P₁) (g₂ : ∀ i, M i → P₂)
Lean source · statement
def lift [IsDirectLimit f g₁] (p : P₁) : P₂
theorem

lift_of

L74 ↗
IsDirectLimit.lift_of
Source context 5 commands

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

section
variable {ι : Type*} [Preorder ι] {M : ι → Type*} {P : Type*}
  (f : (i j : ι) → (h : i ≤ j) → M i → M j) (g : ∀ i, M i → P)
variable [DirectedSystem M f] [IsDirectLimit f g]
namespace IsDirectLimit
variable {P₁ P₂ : Type*} (g₁ : ∀ i, M i → P₁) (g₂ : ∀ i, M i → P₂)
Lean source · statement
theorem lift_of [IsDirectLimit f g₁] (Hg : ∀ i j hij x, g₂ j (f i j hij x) = g₂ i x) {i} (x) :
    (lift f g₁ g₂) (g₁ i x) = g₂ i x
def

Equiv

L81 ↗
IsDirectLimit.Equiv
Documentation

The canonical equivalence between two realizations of the same direct limit.

Source context 5 commands

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

section
variable {ι : Type*} [Preorder ι] {M : ι → Type*} {P : Type*}
  (f : (i j : ι) → (h : i ≤ j) → M i → M j) (g : ∀ i, M i → P)
variable [DirectedSystem M f] [IsDirectLimit f g]
namespace IsDirectLimit
variable {P₁ P₂ : Type*} (g₁ : ∀ i, M i → P₁) (g₂ : ∀ i, M i → P₂)
Lean source · full declaration
def Equiv [h₁ : IsDirectLimit f g₁] [h₂ : IsDirectLimit f g₂] :
    P₁ ≃ P₂ where
  toFun := lift f g₁ g₂
  invFun := lift f g₂ g₁
  left_inv x := by
    obtain ⟨i, mi, hmi⟩ := h₁.surj x
    rw [← hmi]
    simp only [compatibility', implies_true, lift_of]
  right_inv x := by
    obtain ⟨i, mi, hmi⟩ := h₂.surj x
    rw [← hmi]
    simp only [compatibility', implies_true, lift_of]
lemma

Equiv_apply

L94 ↗
IsDirectLimit.Equiv_apply
Source context 5 commands

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

section
variable {ι : Type*} [Preorder ι] {M : ι → Type*} {P : Type*}
  (f : (i j : ι) → (h : i ≤ j) → M i → M j) (g : ∀ i, M i → P)
variable [DirectedSystem M f] [IsDirectLimit f g]
namespace IsDirectLimit
variable {P₁ P₂ : Type*} (g₁ : ∀ i, M i → P₁) (g₂ : ∀ i, M i → P₂)
Lean source · statement
lemma Equiv_apply (i : ι) (x : M i) [IsDirectLimit f g₁] [IsDirectLimit f g₂] :
  Equiv f g₁ g₂ (g₁ i x) = g₂ i x
lemma

linearEquiv_symm_apply

L98 ↗
IsDirectLimit.linearEquiv_symm_apply
Source context 5 commands

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

section
variable {ι : Type*} [Preorder ι] {M : ι → Type*} {P : Type*}
  (f : (i j : ι) → (h : i ≤ j) → M i → M j) (g : ∀ i, M i → P)
variable [DirectedSystem M f] [IsDirectLimit f g]
namespace IsDirectLimit
variable {P₁ P₂ : Type*} (g₁ : ∀ i, M i → P₁) (g₂ : ∀ i, M i → P₂)
Lean source · statement
lemma linearEquiv_symm_apply (i : ι) (x : M i) [IsDirectLimit f g₁]
  [IsDirectLimit f g₂] : (Equiv f g₁ g₂).symm (g₂ i x) = g₁ i x
instance

(anonymous instance)

L108 ↗
Source context 7 commands

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

section
variable {ι : Type*} [Preorder ι] {M : ι → Type*} {P : Type*}
  (f : (i j : ι) → (h : i ≤ j) → M i → M j) (g : ∀ i, M i → P)
variable [DirectedSystem M f] [IsDirectLimit f g]
namespace IsDirectLimit
variable {P₁ P₂ : Type*} (g₁ : ∀ i, M i → P₁) (g₂ : ∀ i, M i → P₂)
namespace Module
variable {R : Type*} [Semiring R] [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)]
  [AddCommMonoid P] [Module R P] (f : (i j : ι) → i ≤ j → M i →ₗ[R] M j)
  [DirectedSystem M (f · · ·)] [IsDirectLimit (fun ⦃i j⦄ h => f i j h) g] [IsDirected ι (· ≤ ·)]
Lean source · full declaration
instance [DecidableEq ι] [Nonempty ι] :
    IsDirectLimit (f · · ·) (Module.DirectLimit.of R ι M f ·) where
  surj := Module.DirectLimit.exists_of
  inj i j mi mj h := by
    apply_fun Module.DirectLimit.linearEquiv _ _ at h
    simp_rw [Module.DirectLimit.linearEquiv_of, Quotient.eq] at h
    exact h
  compatibility i j hij x := Module.DirectLimit.of_f
theorem

compatibility_module

L121 ↗
IsDirectLimit.Module.compatibility_module
Source context 9 commands

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

section
variable {ι : Type*} [Preorder ι] {M : ι → Type*} {P : Type*}
  (f : (i j : ι) → (h : i ≤ j) → M i → M j) (g : ∀ i, M i → P)
variable [DirectedSystem M f] [IsDirectLimit f g]
namespace IsDirectLimit
variable {P₁ P₂ : Type*} (g₁ : ∀ i, M i → P₁) (g₂ : ∀ i, M i → P₂)
namespace Module
variable {R : Type*} [Semiring R] [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)]
  [AddCommMonoid P] [Module R P] (f : (i j : ι) → i ≤ j → M i →ₗ[R] M j)
  [DirectedSystem M (f · · ·)] [IsDirectLimit (fun ⦃i j⦄ h => f i j h) g] [IsDirected ι (· ≤ ·)]
variable [AddCommMonoid P₁] [Module R P₁] [AddCommMonoid P₂] [Module R P₂]
  (g₁ : ∀ i, M i →ₗ[R] P₁) (g₂ : ∀ i, M i →ₗ[R] P₂) [h₁ : IsDirectLimit (f · · ·) (g₁ · ·)]
omit [IsDirected ι (· ≤ ·)] in
Lean source · statement
theorem compatibility_module {i j hij} (x : M i) : g₁ j (f i j hij x) = g₁ i x
def

lift

L125 ↗
IsDirectLimit.Module.lift
Documentation

The linear map induced from a compatible family of linear maps on the stages.

Source context 8 commands

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

section
variable {ι : Type*} [Preorder ι] {M : ι → Type*} {P : Type*}
  (f : (i j : ι) → (h : i ≤ j) → M i → M j) (g : ∀ i, M i → P)
variable [DirectedSystem M f] [IsDirectLimit f g]
namespace IsDirectLimit
variable {P₁ P₂ : Type*} (g₁ : ∀ i, M i → P₁) (g₂ : ∀ i, M i → P₂)
namespace Module
variable {R : Type*} [Semiring R] [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)]
  [AddCommMonoid P] [Module R P] (f : (i j : ι) → i ≤ j → M i →ₗ[R] M j)
  [DirectedSystem M (f · · ·)] [IsDirectLimit (fun ⦃i j⦄ h => f i j h) g] [IsDirected ι (· ≤ ·)]
variable [AddCommMonoid P₁] [Module R P₁] [AddCommMonoid P₂] [Module R P₂]
  (g₁ : ∀ i, M i →ₗ[R] P₁) (g₂ : ∀ i, M i →ₗ[R] P₂) [h₁ : IsDirectLimit (f · · ·) (g₁ · ·)]
Lean source · full declaration
def lift
    (Hg : ∀ i j hij x, g₂ j (f i j hij x) = g₂ i x) : P₁ →ₗ[R] P₂ where
  toFun := IsDirectLimit.lift (f · · ·) (g₁ · ·) (g₂ · · )
  map_add' x y := by
    obtain ⟨k, hxk, hyk⟩ :=
      IsDirected.directed (r := (· ≤ ·)) (preimage_index (f · · ·) (g₁ · ·) x)
      (preimage_index (f · · ·) (g₁ · ·) y)
    obtain ⟨k', hxyk', hkk'⟩ := IsDirected.directed (r := (· ≤ ·))
      (preimage_index (f · · ·) (g₁ · ·) (x+y)) k
    have sum_eq : g₁ k' (f (preimage_index (f · · ·) (g₁ · ·) x) k' (le_trans hxk hkk')
      (preimage (f · · ·) (g₁ · ·) x) + f (preimage_index (f · · ·) (g₁ · ·) y) k'
      (le_trans hyk hkk') (preimage (f · · ·) (g₁ · ·) y)) =
        g₁ (preimage_index (f · · ·) (g₁ · ·) (x+y)) (preimage (f · · ·) (g₁ · ·) (x+y)) := by
      simp only [LinearMap.map_add, image_preimage]
      repeat rw [compatibility' (f · · ·) (g₁ · ·),
        image_preimage (f := (f · · ·)) (g := (g₁ · ·))]
    obtain ⟨k'', hk'k'', hxyk'', h'''⟩ := is_injective (f · · ·) (g₁ · ·) sum_eq
    simpa [Hg, IsDirectLimit.lift] using congr_arg (g₂ k'') h'''.symm
  map_smul' r x := by
    have smul_eq : g₁ (preimage_index (f · · ·) (g₁ · ·) (r • x)) (preimage (f · · ·) (g₁ · ·)
      (r • x)) = g₁ (preimage_index (f · · ·) (g₁ · ·) x) (r • preimage (f · · ·) (g₁ · ·) x) := by
      simp only [image_preimage, map_smul]
    obtain ⟨k, hixk, hirxk, h_smul⟩ := is_injective (f · · ·) (g₁ · ·) smul_eq
    simpa [Hg, IsDirectLimit.lift] using congr_arg (g₂ k) h_smul
theorem

lift_of

L150 ↗
IsDirectLimit.Module.lift_of
Source context 8 commands

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

section
variable {ι : Type*} [Preorder ι] {M : ι → Type*} {P : Type*}
  (f : (i j : ι) → (h : i ≤ j) → M i → M j) (g : ∀ i, M i → P)
variable [DirectedSystem M f] [IsDirectLimit f g]
namespace IsDirectLimit
variable {P₁ P₂ : Type*} (g₁ : ∀ i, M i → P₁) (g₂ : ∀ i, M i → P₂)
namespace Module
variable {R : Type*} [Semiring R] [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)]
  [AddCommMonoid P] [Module R P] (f : (i j : ι) → i ≤ j → M i →ₗ[R] M j)
  [DirectedSystem M (f · · ·)] [IsDirectLimit (fun ⦃i j⦄ h => f i j h) g] [IsDirected ι (· ≤ ·)]
variable [AddCommMonoid P₁] [Module R P₁] [AddCommMonoid P₂] [Module R P₂]
  (g₁ : ∀ i, M i →ₗ[R] P₁) (g₂ : ∀ i, M i →ₗ[R] P₂) [h₁ : IsDirectLimit (f · · ·) (g₁ · ·)]
Lean source · statement
theorem lift_of (Hg : ∀ i j hij x, g₂ j (f i j hij x) = g₂ i x) {i} (x) :
    (Module.lift f g₁ g₂ Hg) (g₁ i x) = g₂ i x
theorem

lift_unique

L155 ↗
IsDirectLimit.Module.lift_unique
Source context 8 commands

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

section
variable {ι : Type*} [Preorder ι] {M : ι → Type*} {P : Type*}
  (f : (i j : ι) → (h : i ≤ j) → M i → M j) (g : ∀ i, M i → P)
variable [DirectedSystem M f] [IsDirectLimit f g]
namespace IsDirectLimit
variable {P₁ P₂ : Type*} (g₁ : ∀ i, M i → P₁) (g₂ : ∀ i, M i → P₂)
namespace Module
variable {R : Type*} [Semiring R] [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)]
  [AddCommMonoid P] [Module R P] (f : (i j : ι) → i ≤ j → M i →ₗ[R] M j)
  [DirectedSystem M (f · · ·)] [IsDirectLimit (fun ⦃i j⦄ h => f i j h) g] [IsDirected ι (· ≤ ·)]
variable [AddCommMonoid P₁] [Module R P₁] [AddCommMonoid P₂] [Module R P₂]
  (g₁ : ∀ i, M i →ₗ[R] P₁) (g₂ : ∀ i, M i →ₗ[R] P₂) [h₁ : IsDirectLimit (f · · ·) (g₁ · ·)]
Lean source · full declaration
theorem lift_unique (F : P₁ →ₗ[R] P₂) (x) : F x = (Module.lift f g₁ (fun i ↦ F.comp <| g₁ i)
    (fun i j hij x ↦ by
      simp only [LinearMap.coe_comp, Function.comp_apply]
      exact LinearMap.congr_arg (IsDirectLimit.compatibility (f := (f · · ·))
      (g := (g₁ · ·)) i j hij x))) x := by
  simp only [lift, IsDirectLimit.lift,
    LinearMap.coe_comp, Function.comp_apply, LinearMap.coe_mk, AddHom.coe_mk, image_preimage]
def

linearEquiv

L166 ↗
IsDirectLimit.Module.linearEquiv
Documentation

The linear equivalence between two realizations of the same module direct limit.

Source context 9 commands

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

section
variable {ι : Type*} [Preorder ι] {M : ι → Type*} {P : Type*}
  (f : (i j : ι) → (h : i ≤ j) → M i → M j) (g : ∀ i, M i → P)
variable [DirectedSystem M f] [IsDirectLimit f g]
namespace IsDirectLimit
variable {P₁ P₂ : Type*} (g₁ : ∀ i, M i → P₁) (g₂ : ∀ i, M i → P₂)
namespace Module
variable {R : Type*} [Semiring R] [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)]
  [AddCommMonoid P] [Module R P] (f : (i j : ι) → i ≤ j → M i →ₗ[R] M j)
  [DirectedSystem M (f · · ·)] [IsDirectLimit (fun ⦃i j⦄ h => f i j h) g] [IsDirected ι (· ≤ ·)]
variable [AddCommMonoid P₁] [Module R P₁] [AddCommMonoid P₂] [Module R P₂]
  (g₁ : ∀ i, M i →ₗ[R] P₁) (g₂ : ∀ i, M i →ₗ[R] P₂) [h₁ : IsDirectLimit (f · · ·) (g₁ · ·)]
variable [h₂ : IsDirectLimit (f · · ·) (g₂ · ·)]
Lean source · statement
def linearEquiv : P₁ ≃ₗ[R] P₂
lemma

linearEquiv_apply

L171 ↗
IsDirectLimit.Module.linearEquiv_apply
Source context 9 commands

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

section
variable {ι : Type*} [Preorder ι] {M : ι → Type*} {P : Type*}
  (f : (i j : ι) → (h : i ≤ j) → M i → M j) (g : ∀ i, M i → P)
variable [DirectedSystem M f] [IsDirectLimit f g]
namespace IsDirectLimit
variable {P₁ P₂ : Type*} (g₁ : ∀ i, M i → P₁) (g₂ : ∀ i, M i → P₂)
namespace Module
variable {R : Type*} [Semiring R] [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)]
  [AddCommMonoid P] [Module R P] (f : (i j : ι) → i ≤ j → M i →ₗ[R] M j)
  [DirectedSystem M (f · · ·)] [IsDirectLimit (fun ⦃i j⦄ h => f i j h) g] [IsDirected ι (· ≤ ·)]
variable [AddCommMonoid P₁] [Module R P₁] [AddCommMonoid P₂] [Module R P₂]
  (g₁ : ∀ i, M i →ₗ[R] P₁) (g₂ : ∀ i, M i →ₗ[R] P₂) [h₁ : IsDirectLimit (f · · ·) (g₁ · ·)]
variable [h₂ : IsDirectLimit (f · · ·) (g₂ · ·)]
Lean source · statement
lemma linearEquiv_apply (i : ι) (x : M i) :
  linearEquiv f g₁ g₂ (g₁ i x) = g₂ i x
lemma

linearEquiv_symm_apply

L175 ↗
IsDirectLimit.Module.linearEquiv_symm_apply
Source context 9 commands

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

section
variable {ι : Type*} [Preorder ι] {M : ι → Type*} {P : Type*}
  (f : (i j : ι) → (h : i ≤ j) → M i → M j) (g : ∀ i, M i → P)
variable [DirectedSystem M f] [IsDirectLimit f g]
namespace IsDirectLimit
variable {P₁ P₂ : Type*} (g₁ : ∀ i, M i → P₁) (g₂ : ∀ i, M i → P₂)
namespace Module
variable {R : Type*} [Semiring R] [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)]
  [AddCommMonoid P] [Module R P] (f : (i j : ι) → i ≤ j → M i →ₗ[R] M j)
  [DirectedSystem M (f · · ·)] [IsDirectLimit (fun ⦃i j⦄ h => f i j h) g] [IsDirected ι (· ≤ ·)]
variable [AddCommMonoid P₁] [Module R P₁] [AddCommMonoid P₂] [Module R P₂]
  (g₁ : ∀ i, M i →ₗ[R] P₁) (g₂ : ∀ i, M i →ₗ[R] P₂) [h₁ : IsDirectLimit (f · · ·) (g₁ · ·)]
variable [h₂ : IsDirectLimit (f · · ·) (g₂ · ·)]
Lean source · statement
lemma linearEquiv_symm_apply (i : ι) (x : M i) :
  (linearEquiv f g₁ g₂).symm (g₂ i x) = g₁ i x

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