mathlib3 documentation

lean-ga / for_mathlib.algebra.filtration

Filtrations of an algebra #

source
structure algebra.filtration (R : Type u_1) (A : Type u_2) (ι : Type u_3) [preorder ι] [has_add ι] [comm_semiring R] [semiring A] [algebra R A] :
Type (max u_2 u_3)

A filtration is an indexed family of submodules such that i ≤ j → S i ≤ S j and S i * S j = S (i + j)

Instances for algebra.filtration
source
@[protected, instance]
def algebra.filtration.has_coe_to_fun {R : Type u_1} {A : Type u_2} {ι : Type u_3} [preorder ι] [has_add ι] [comm_semiring R] [semiring A] [algebra R A] :
has_coe_to_fun (algebra.filtration R A ι) (λ (_x : algebra.filtration R A ι), ι → submodule R A)
Equations
source
@[simp]
theorem algebra.filtration.to_fun_eq_coe {R : Type u_1} {A : Type u_2} {ι : Type u_3} [preorder ι] [has_add ι] [comm_semiring R] [semiring A] [algebra R A] (f : algebra.filtration R A ι) :
f.to_fun = ⇑f
source
@[simp]
theorem algebra.filtration.mk_coe {R : Type u_1} {A : Type u_2} {ι : Type u_3} [preorder ι] [has_add ι] [comm_semiring R] [semiring A] [algebra R A] (f : ι → submodule R A) (h1 : monotone f) (h2 : ∀ (x : A), ∃ (i : ι), x ∈ f i) (h3 : ∀ (n m : ι), f (n + m) = f n * f m) :
⇑{to_fun := f, mono' := h1, complete' := h2, map_add' := h3} = f
source
theorem algebra.filtration.mono {R : Type u_1} {A : Type u_2} {ι : Type u_3} [preorder ι] [has_add ι] [comm_semiring R] [semiring A] [algebra R A] (f : algebra.filtration R A ι) :
monotone ⇑f
source
theorem algebra.filtration.map_add {R : Type u_1} {A : Type u_2} {ι : Type u_3} [preorder ι] [has_add ι] [comm_semiring R] [semiring A] [algebra R A] (f : algebra.filtration R A ι) {n m : ι} :
⇑f (n + m) = ⇑f n * ⇑f m
source
theorem algebra.filtration.complete {R : Type u_1} {A : Type u_2} {ι : Type u_3} [preorder ι] [has_add ι] [comm_semiring R] [semiring A] [algebra R A] (f : algebra.filtration R A ι) (x : A) :
∃ (i : ι), x ∈ ⇑f i
source
theorem algebra.filtration.supr_eq_top {R : Type u_1} {A : Type u_2} {ι : Type u_3} [preorder ι] [has_add ι] [comm_semiring R] [semiring A] [algebra R A] (f : algebra.filtration R A ι) (x : A) :
supr ⇑f = ⊤