source
A complete abelian category with enough injectives and a separator has an injective coseparator #
Future work #
Once we know that Grothendieck categories have enough injectives, we can use this to conclude
that Grothendieck categories have an injective coseparator.
References #
General documentation
Additional documentation
Library
core
data
buffer
init
algebra
control
data
array
bool
char
fin
int
list
nat
option
ordering
sigma
string
subtype
sum
unsigned
meta
converter
lean
smt
widget
system
mathlib
algebra
algebra
subalgebra
big_operators
category
Algebra
FinVect
Group
Module
Mon
Ring
Semigroup
char_p
char_zero
continued_fractions
computation
direct_sum
field
gcd_monoid
group
group_power
group_with_zero
hom
homology
short_exact
jordan
lie
module
submodule
monoid_algebra
order
hom
positive
polynomial
regular
ring
star
tropical
algebraic_geometry
locally_ringed_space
morphisms
presheafed_space
prime_spectrum
projective_spectrum
algebraic_topology
dold_kan
fundamental_groupoid
analysis
ODE
analytic
asymptotics
box_integral
box
partition
calculus
conformal
complex
upper_half_plane
convex
cone
simplicial_complex
inner_product_space
locally_convex
normed
field
group
SemiNormedGroup
normed_space
hahn_banach
star
special_functions
complex
log
trigonometric
specific_limits
von_neumann_algebra
category_theory
abelian
diagram_lemmas
additive
adjunction
bicategory
category
Cat
closed
concrete_category
endofunctor
enriched
functor
idempotents
lifting_properties
limits
constructions
over
preserves
shapes
shapes
normal_mono
linear
localization
monad
monoidal
free
internal
rigid
pi
preadditive
products
sigma
sites
subobject
sums
triangulated
combinatorics
additive
derangements
hall
quiver
set_family
compression
simple_graph
regularity
computability
control
bitraversable
equiv_functor
functor
monad
traversable
data
W
analysis
array
bitvec
bool
buffer
parser
complex
countable
dfinsupp
dlist
fin
tuple
finite
finset
finsupp
fintype
fp
fun_like
int
cast
lazy_list
list
matrix
multiset
mv_polynomial
nat
cast
choose
factorial
factorization
num
option
ordmap
pfunctor
multivariate
univariate
pi
pnat
polynomial
degree
prod
psigma
qpf
multivariate
constructions
univariate
rat
rbmap
rbtree
real
pi
seq
set
intervals
set_like
setoid
sigma
stream
string
sum
sym
vector
zmod
deprecated
dynamics
circle
rotation_number
ergodic
fixed_points
field_theory
finite
is_alg_closed
geometry
euclidean
manifold
algebra
instances
group_theory
group_action
sub_mul_action
perm
cycle
specific_groups
subgroup
submonoid
subsemigroup
information_theory
linear_algebra
affine_space
charpoly
clifford_algebra
direct_sum
exterior_algebra
free_module
finite
matrix
charpoly
multilinear
projective_space
quadratic_form
tensor_algebra
logic
encodable
equiv
function
measure_theory
category
constructions
covering
decomposition
function
conditional_expectation
group
integral
measure
meta
model_theory
number_theory
class_number
cyclotomic
legendre_symbol
liouville
modular_forms
padics
zsqrtd
order
category
filter
heyting
hom
partition
succ_pred
probability
martingale
probability_mass_function
representation_theory
ring_theory
adjoin
coprime
dedekind_domain
graded_algebra
ideal
int
localization
mv_polynomial
ore_localization
polynomial
cyclotomic
power_series
ring_hom
subring
subsemiring
valuation
witt_vector
set_theory
cardinal
game
ordinal
surreal
zfc
tactic
converter
linarith
lint
monotonicity
nth_rewrite
omega
int
nat
rewrite_all
rewrite_search
testing
slim_check
topology
algebra
module
nonarchimedean
order
bornology
category
CompHaus
Profinite
Top
continuous_function
hom
homotopy
instances
locally_constant
metric_space
order
hom
sets
sheaves
sheaf_condition
spectral
uniform_space
vector_bundle
Color scheme