New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(Condensed): discrete-underlying adjunction #8270
Conversation
variable (D : Type w) [Category.{max v u} D] | ||
|
||
/-- The constant presheaf functor is left adjoint to evaluation at a terminal object. -/ | ||
noncomputable def constantPresheafAdj {T : C} (hT : IsTerminal T) : |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
variable (D : Type w) [Category.{max v u} D] | |
/-- The constant presheaf functor is left adjoint to evaluation at a terminal object. -/ | |
noncomputable def constantPresheafAdj {T : C} (hT : IsTerminal T) : | |
variable (D : Type w) [Category.{max v u} D] | |
/-- The constant presheaf functor is left adjoint to evaluation at a terminal object. -/ | |
noncomputable def constantPresheafAdj {T : C} (hT : IsTerminal T) : |
For this definition, the universe assumption on D
could be relaxed.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I just removed the explicit universes, Lean figures them out in the correct generality
Thanks! bors merge |
We define a functor, associating to an object of a concrete category with nice properties, a "discrete" condensed object, and prove that this functor is left adjoint to the forgetful functor from `Condensed C` to `C`.
Pull request successfully merged into master. Build succeeded: |
We define a functor, associating to an object of a concrete category with nice properties, a "discrete" condensed object, and prove that this functor is left adjoint to the forgetful functor from `Condensed C` to `C`.
We define a functor, associating to an object of a concrete category with nice properties, a "discrete" condensed object, and prove that this functor is left adjoint to the forgetful functor from
Condensed C
toC
.