feat(order/galois_connection): add exists_eq_{l,u}, tidy up lemmas (#9904)

This makes some arguments implicit to `compose` as these are inferrable from the other arguments, and changes `u_l_u_eq_u` and `l_u_l_eq_l` to be applied rather than unapplied, which shortens both the proof and the places where the lemma is used.

Author: eric-wieser

src/algebraic_geometry/prime_spectrum.lean

@@ -167,7 +167,7 @@ lemma gc_set : @galois_connection
   (set R) (order_dual (set (prime_spectrum R))) _ _
   (λ s, zero_locus s) (λ t, vanishing_ideal t) :=
 have ideal_gc : galois_connection (ideal.span) coe := (submodule.gi R R).gc,
-by simpa [zero_locus_span, function.comp] using galois_connection.compose _ _ _ _ ideal_gc (gc R)
+by simpa [zero_locus_span, function.comp] using ideal_gc.compose (gc R)
 
 lemma subset_zero_locus_iff_subset_vanishing_ideal (t : set (prime_spectrum R)) (s : set R) :
   t ⊆ zero_locus s ↔ s ⊆ vanishing_ideal t :=
@@ -191,7 +191,7 @@ begin
 end
 
 @[simp] lemma zero_locus_radical (I : ideal R) : zero_locus (I.radical : set R) = zero_locus I :=
-vanishing_ideal_zero_locus_eq_radical I ▸ congr_fun (gc R).l_u_l_eq_l I
+vanishing_ideal_zero_locus_eq_radical I ▸ (gc R).l_u_l_eq_l I
 
 lemma subset_zero_locus_vanishing_ideal (t : set (prime_spectrum R)) :
   t ⊆ zero_locus (vanishing_ideal t) :=
@@ -375,7 +375,7 @@ end
 
 lemma vanishing_ideal_closure (t : set (prime_spectrum R)) :
   vanishing_ideal (closure t) = vanishing_ideal t :=
-zero_locus_vanishing_ideal_eq_closure t ▸ congr_fun (gc R).u_l_u_eq_u t
+zero_locus_vanishing_ideal_eq_closure t ▸ (gc R).u_l_u_eq_u t
 
 section comap
 variables {S : Type v} [comm_ring S] {S' : Type*} [comm_ring S']

src/group_theory/submonoid/operations.lean

@@ -248,11 +248,11 @@ lemma monotone_comap {f : M →* N} : monotone (comap f) :=
 
 @[simp, to_additive]
 lemma map_comap_map {f : M →* N} : ((S.map f).comap f).map f = S.map f :=
-congr_fun ((gc_map_comap f).l_u_l_eq_l) _
+(gc_map_comap f).l_u_l_eq_l _
 
 @[simp, to_additive]
 lemma comap_map_comap {S : submonoid N} {f : M →* N} : ((S.comap f).map f).comap f = S.comap f :=
-congr_fun ((gc_map_comap f).u_l_u_eq_u) _
+(gc_map_comap f).u_l_u_eq_u _
 
 @[to_additive]
 lemma map_sup (S T : submonoid M) (f : M →* N) : (S ⊔ T).map f = S.map f ⊔ T.map f :=

src/model_theory/basic.lean

@@ -637,12 +637,12 @@ lemma monotone_comap {f : M →[L] N} : monotone (comap f) :=
 
 @[simp]
 lemma map_comap_map {f : M →[L] N} : ((S.map f).comap f).map f = S.map f :=
-congr_fun ((gc_map_comap f).l_u_l_eq_l) _
+(gc_map_comap f).l_u_l_eq_l _
 
 @[simp]
 lemma comap_map_comap {S : L.substructure N} {f : M →[L] N} :
   ((S.comap f).map f).comap f = S.comap f :=
-congr_fun ((gc_map_comap f).u_l_u_eq_u) _
+(gc_map_comap f).u_l_u_eq_u _
 
 lemma map_sup (S T : L.substructure M) (f : M →[L] N) : (S ⊔ T).map f = S.map f ⊔ T.map f :=
 (gc_map_comap f).l_sup

src/order/closure.lean

@@ -287,7 +287,7 @@ def closure_operator :
 { to_fun := λ x, u (l x),
   monotone' := l.monotone,
   le_closure' := l.le_closure,
-  idempotent' := λ x, show (u ∘ l ∘ u) (l x) = u (l x), by rw l.gc.u_l_u_eq_u }
+  idempotent' := λ x, l.gc.u_l_u_eq_u (l x) }
 
 lemma idempotent (x : α) : u (l (u (l x))) = u (l x) :=
 l.closure_operator.idempotent _

src/order/galois_connection.lean

@@ -121,28 +121,40 @@ section partial_order
 variables [partial_order α] [preorder β] {l : α → β} {u : β → α} (gc : galois_connection l u)
 include gc
 
-lemma u_l_u_eq_u : u ∘ l ∘ u = u :=
-funext (λ x, (gc.monotone_u (gc.l_u_le _)).antisymm (gc.le_u_l _))
+lemma u_l_u_eq_u (b : β) : u (l (u b)) = u b :=
+(gc.monotone_u (gc.l_u_le _)).antisymm (gc.le_u_l _)
+
+lemma u_l_u_eq_u' : u ∘ l ∘ u = u := funext gc.u_l_u_eq_u
 
 lemma u_unique {l' : α → β} {u' : β → α} (gc' : galois_connection l' u')
   (hl : ∀ a, l a = l' a) {b : β} : u b = u' b :=
 le_antisymm (gc'.le_u $ hl (u b) ▸ gc.l_u_le _)
   (gc.le_u $ (hl (u' b)).symm ▸ gc'.l_u_le _)
 
+/-- If there exists a `b` such that `a = u a`, then `b = l a` is one such element. -/
+lemma exists_eq_u (a : α) : (∃ b : β, a = u b) ↔ a = u (l a) :=
+⟨λ ⟨S, hS⟩, hS.symm ▸ (gc.u_l_u_eq_u _).symm, λ HI, ⟨_, HI⟩ ⟩
+
 end partial_order
 
 section partial_order
 variables [preorder α] [partial_order β] {l : α → β} {u : β → α} (gc : galois_connection l u)
 include gc
 
-lemma l_u_l_eq_l : l ∘ u ∘ l = l :=
-funext (λ x, (gc.l_u_le _).antisymm (gc.monotone_l (gc.le_u_l _)))
+lemma l_u_l_eq_l (a : α) : l (u (l a)) = l a :=
+(gc.l_u_le _).antisymm (gc.monotone_l (gc.le_u_l _))
+
+lemma l_u_l_eq_l' : l ∘ u ∘ l = l := funext gc.l_u_l_eq_l
 
 lemma l_unique {l' : α → β} {u' : β → α} (gc' : galois_connection l' u')
   (hu : ∀ b, u b = u' b) {a : α} : l a = l' a :=
 le_antisymm (gc.l_le $ (hu (l' a)).symm ▸ gc'.le_u_l _)
   (gc'.l_le $ hu (l a) ▸ gc.le_u_l _)
 
+/-- If there exists an `a` such that `b = l a`, then `a = u b` is one such element. -/
+lemma exists_eq_l (b : β) : (∃ a : α, b = l a) ↔ b = l (u b) :=
+⟨λ ⟨S, hS⟩, hS.symm ▸ (gc.l_u_l_eq_l _).symm, λ HI, ⟨_, HI⟩ ⟩
+
 end partial_order
 
 section order_top
@@ -205,15 +217,15 @@ protected lemma id [pα : preorder α] : @galois_connection α α pα pα id id
 λ a b, iff.intro (λ x, x) (λ x, x)
 
 protected lemma compose [preorder α] [preorder β] [preorder γ]
-  (l1 : α → β) (u1 : β → α) (l2 : β → γ) (u2 : γ → β)
+  {l1 : α → β} {u1 : β → α} {l2 : β → γ} {u2 : γ → β}
   (gc1 : galois_connection l1 u1) (gc2 : galois_connection l2 u2) :
   galois_connection (l2 ∘ l1) (u1 ∘ u2) :=
 by intros a b; rw [gc2, gc1]
 
 protected lemma dfun {ι : Type u} {α : ι → Type v} {β : ι → Type w}
   [∀ i, preorder (α i)] [∀ i, preorder (β i)]
   (l : Πi, α i → β i) (u : Πi, β i → α i) (gc : ∀ i, galois_connection (l i) (u i)) :
-  @galois_connection (Π i, α i) (Π i, β i) _ _ (λ a i, l i (a i)) (λ b i, u i (b i)) :=
+  galois_connection (λ (a : Π i, α i) i, l i (a i)) (λ b i, u i (b i)) :=
 λ a b, forall_congr $ λ i, gc i (a i) (b i)
 
 end constructions

src/ring_theory/ideal/operations.lean

@@ -792,7 +792,7 @@ lemma comap_comap {T : Type*} [ring T] {I : ideal T} (f : R →+* S)
 
 lemma map_map {T : Type*} [ring T] {I : ideal R} (f : R →+* S)
   (g : S →+*T) : (I.map f).map g = I.map (g.comp f) :=
-((gc_map_comap f).compose _ _ _ _ (gc_map_comap g)).l_unique
+((gc_map_comap f).compose (gc_map_comap g)).l_unique
   (gc_map_comap (g.comp f)) (λ _, comap_comap _ _)
 
 lemma map_span (f : R →+* S) (s : set R) :
@@ -828,10 +828,10 @@ lemma map_comap_le : (K.comap f).map f ≤ K :=
 variables (f I J K L)
 
 @[simp] lemma map_comap_map : ((I.map f).comap f).map f = I.map f :=
-congr_fun (gc_map_comap f).l_u_l_eq_l I
+(gc_map_comap f).l_u_l_eq_l I
 
 @[simp] lemma comap_map_comap : ((K.comap f).map f).comap f = K.comap f :=
-congr_fun (gc_map_comap f).u_l_u_eq_u K
+(gc_map_comap f).u_l_u_eq_u K
 
 lemma map_sup : (I ⊔ J).map f = I.map f ⊔ J.map f :=
 (gc_map_comap f).l_sup