Conversation
algebra/direct_limit.lean
Outdated
| open lattice | ||
|
|
||
| def is_add_group_hom {α : Type*} {β : Type*} [add_group α] [add_group β] (f : α → β) : Prop := | ||
| @is_group_hom (multiplicative α) (multiplicative β) _ _ f |
algebra/direct_limit.lean
Outdated
|
|
||
| theorem congr_arg₂ {α β γ : Type*} (f : α → β → γ) {x₁ x₂ : α} {y₁ y₂ : β} | ||
| (Hx : x₁ = x₂) (Hy : y₁ = y₂) : f x₁ y₁ = f x₂ y₂ := | ||
| eq.drec (eq.drec rfl Hy) Hx |
There was a problem hiding this comment.
This is in the wrong place, but I don't know why you need it. by congr should do the job
algebra/direct_limit.lean
Outdated
| variables [∀ i, add_comm_group (G i)] (f : Π i j, i ≤ j → G i → G j) | ||
| variables [∀ i j h, is_add_group_hom (f i j h)] [directed_system f] | ||
|
|
||
| instance direct_limit.setoid : setoid (sigma G) := |
There was a problem hiding this comment.
This cannot be an instance because it depends on f which is not in the type
| repeat { rw directed_system.Hcomp f }, | ||
| repeat { apply_instance } | ||
| end⟩, | ||
| .. direct_limit.add_comm_group' f } |
There was a problem hiding this comment.
These proofs are rather messy. You should state the types more, maybe use a calc block
algebra/direct_limit.lean
Outdated
| (f : α → β) [is_ring_hom f] : is_add_group_hom f := | ||
| ⟨λ _ _, is_ring_hom.map_add f⟩ | ||
|
|
||
| variables {ι : out_param (Type u)} [inhabited ι] [semilattice_sup ι] {G : ι → Type v} |
There was a problem hiding this comment.
Normally a direct limit is defined as being indexed on a directed set, the difference being that we only assume that any two elements have some upper bound, rather than a least upper bound. This is the natural level of generality since it is a sufficient condition for the colimit to be constructed as a quotient of a disjoint union (in a finitary algebraic category like abelian groups).
Would it be too awkward to extend the construction to this setting? I noticed you do use sup_le in several places, though I didn't attempt to work out what it is being used for.
|
I think you need to prove that |
|
Were I able to figure out how to edit this PR myself, I would suggest adding the following lines to the bottom of namespace direct_limit
variables [∀ i, comm_ring (G i)] (f : Π i j, i ≤ j → G i → G j)
variables [∀ i j h, is_ring_hom (f i j h)] [directed_system f]
local attribute [instance] direct_limit.setoid
instance comm_ring' : comm_ring (quotient (direct_limit.setoid f)) :=
{
mul_comm := λ i j, quotient.induction_on₂ i j $ λ ⟨p, xp⟩ ⟨q, xq⟩, quotient.sound
⟨(p ⊔ q) ⊔ (q ⊔ p), le_sup_left, le_sup_right,
by dsimp; simp [directed_system.map_mul f, directed_system.mul f, directed_system.Hcomp f, mul_comm]⟩
.. direct_limit.ring' f }
instance: comm_ring (direct_limit f) :=
direct_limit.comm_ring' f
end direct_limit(because I need them for my schemes work) |
kbuzzard
left a comment
There was a problem hiding this comment.
comments on notation and conventions used in this PR
| (f : α → β) [is_ring_hom f] : is_add_group_hom f := | ||
| ⟨λ _ _, is_ring_hom.map_add f⟩ | ||
|
|
||
| class directed_order (α : Type u) extends has_sup α, partial_order α := |
There was a problem hiding this comment.
This definition uses inaccurate terminology. I don't know how much of an issue this is. has_sup is clearly intended for situations where two objects have a supremum, or least upper bound. For directed sets (perhaps "directed types" would be better in this context, I am less sure about "directed orders") we definitely don't want to demand that two objects have a supremum, just a common upper bound. In particular the use of sup and the corresponding symbol is arguably misleading in this context.
There was a problem hiding this comment.
I agree - I don't think a directed order should be associated with any additional operations at all, just an existence claim for each pair of points in the type. I think in many situations there is no canonical choice for the witness, so we shouldn't bake in a particular one or else it will mess up equality of structures.
There was a problem hiding this comment.
So you would prefer an exists statement? But you've seen the proofs -- calc f (p ⊔ q) (p ⊔ q ⊔ (r ⊔ s) ⊔ (t ⊔ u)) .... Presumably there's some sensible way to make it so that the proofs can stay looking like this -- some noncomputable function with notation attached I guess. What would be good notation for this?
There was a problem hiding this comment.
I don't think that expression is needed in the first place. If you want larger suprema, you can prove that any list / finset of elements has an upper bound. Even in traditional mathematics it seems a bit weird to have a function here, unless you need it for a particular choicey construction.
There was a problem hiding this comment.
To put this into some context, I would like to use this direct limit stuff in the following situation: X is a top space, B is a basis of open sets, x is in X, and the system is the set of basic open sets containing x. The intersection of two basis elements need not be a basis element, but will contain a basis element which contains x. I would define i <= j iff j is contained in i. So what Mario says (the bare existence statement) is exactly what comes out of the definition of a basis.
There was a problem hiding this comment.
@digama0 I don't understand. How do I make the function computable if I use existentials?
| variables {G : ι → Type v} | ||
|
|
||
| class directed_system (f : Π i j, i ≤ j → G i → G j) : Prop := | ||
| (Hcomp : ∀ i j k hij hjk x, f j k hjk (f i j hij x) = f i k (le_trans hij hjk) x) |
There was a problem hiding this comment.
This is a non-standard definition of a directed system. You have omitted the axiom that if i = j then the induced map G i -> G j is the identity. Here's a sketch of why dropping the axiom doesn't affect things much -- the Hcomp axiom implies that e_i : G i -> G i is idempotent (that is, equals its own square) and commutes with all other maps to and from G i. In particular, one can replace G i with G' i, the image of e i, and get a modified system which now does satisfy the standard axioms for a direct system, and whose direct limit is the limit computed in the file here. In particular, dropping the identity axiom amounts to nothing more than allowing some extra noise. The problem I have with the definition as it stands is that it is non-standard -- this is not what a mathematician calls a direct system so I would strongly argue that it should not be what mathlib calls a direct system -- the axiom should be added. It is never used in the proofs here but it is used in explicit computations of direct limits and it will lead to confusion if it is not added. If it is decided not to add the axiom then I would strongly recommend changing the name of the function, because what we have here is not a direct system, even though it shares many of the properties of a direct system.
There was a problem hiding this comment.
I've realised another way of formalising what I'm saying. There are theorems about direct limit (for example -- if the partially ordered set is discrete, so i <= j iff i = j, then the direct limit is the disjoint union) which will not be provable in Lean if we use this non-standard definition.
There was a problem hiding this comment.
@kbuzzard I don't know what you're talking about; a discrete set isn't directed.
There was a problem hiding this comment.
Aah yes you're right. I'd better stick with the first way :-)
|
I'm not really sure what to do with this commit, it needs work but I'm not in a position to do the work. I'm closing this and sending it to the community fork at https://github.com/leanprover-community/mathlib/tree/direct_limit; someone can revive it from there if they want. |
|
I think we have a workflow problem here. The way you sent this to the community fork looses connection with the extensive discussion on this page. |
|
That's because I didn't create a PR from the community fork, only a branch. If someone works on this branch and eventually PR's it, then they should reference this PR so we have a link to it. |
Local copy: https://github.com/kckennylau/Lean/blob/master/direct_limit.lean