weaker condition?

Stream: new members

[Yi.Yuan]

 import Mathlib
 ​
 universe u v w
 ​
 variable {ι : Type v} [OrderedAddCommMonoid ι]
 ​
 /--For `σ` satisfying `SetLike σ A`, an increasing series of `F` in `σ` is filtration if
 there is another series `F_lt` equal to the supremum of `F` with smaller index-/
 class IsFiltration {A : Type u} {σ : Type*} [SetLike σ A](F : ι → σ) (F_lt : outParam <| ι → σ) : Prop where
   mono {i j} : i ≤ j → F i ≤ F j
   is_le {i} : i < j → F i ≤ F_lt j
   is_sup (B : σ) (j : ι) : (∀ i < j, F i ≤ B) → F_lt j ≤ B
 /- In fact `F_lt j = ⨆ i < j, F i`, the design of `F_lt` can handle different conditions in the
 same structure, it avoid adding `CompleteLattice` to `σ`, also providing convenience when the index
 is `ℤ`-/
 ​
 variable {A : Type*} (σA : Type*) [SetLike σA A] {B : Type*}  (σB : Type*) [SetLike σB B]
 ​
 class SubmonoidClassHom (f : A → B) where
   map : σA → σB
   coe_map (x : σA) : f '' (x : Set A) = map x
   comap : σB → σA/-I want to change `comap` and `coe_comap` to some weaker conditions-/
   coe_comap (y : σB) : (comap y : Set A) = f ⁻¹' y
 ​
 lemma IsFiltration_isSup (FA : ι → σA) (FA_lt : ι → σA) (f : A → B) [fil : IsFiltration FA FA_lt]
 [SubmonoidClassHom σA σB f] (Sup : σB) (j : ι) : ∀ i < j, SubmonoidClassHom.map f (FA i) ≤ Sup →
  ((SubmonoidClassHom.map f (FA_lt j) : σB): Set B) ≤ (Sup : Set B) := by
   intro i i_lt_j h
   rw[← SubmonoidClassHom.coe_map <| FA_lt j]
   refine Set.le_iff_subset.mpr <| Set.image_subset_iff.mpr ?_
   have h : ∀ i < j, ↑(FA i) ≤ f ⁻¹' ↑Sup := by
     intro i i_lt_j
     have : f '' (FA i) ≤ Sup := by
       have : ((SubmonoidClassHom.map f (FA i) : σB) : Set B) ≤ (Sup : Set B) := h i i_lt_j
       rwa[← SubmonoidClassHom.coe_map <| FA i] at this
     exact Set.le_iff_subset.mpr <| Set.image_subset_iff.mp this

   /-How to finish the proof by using weaker conditions? -/
   have : (SubmonoidClassHom.comap f Sup : σA) = f ⁻¹' Sup := SubmonoidClassHom.coe_comap Sup
   rw[← this] at h ⊢
   exact IsFiltration.is_sup (SubmonoidClassHom.comap f Sup : σA) j h

In mathmatics, we have two sets σA and σB of type A and B (It may be empty sets in lean!, so we add conditions to describ them) and f : A → B , we need to add some conditions to describe σA and σB in order to proof : ∀ i < j, f (FA i) ≤ Sup → f (FA_lt j) ≤ Sup

the first and second condition in SubmonoidClassHom is necessary to ensure f (FA i) exist in σB. Now, the question is how to weaker the third and fourth condition(comap and coe_comap)?

[Aaron Liu]

Your code snippet has no-break spaces (U+00A0) and zero-width spaces (U+200B) everywhere, causing it to not parse in the web editor. This makes it difficult for me to edit your code. Could you please remove these no-break spaces and zero-width spaces?

[Yi.Yuan]

Yes, of couse. I will send a lean file a here
InducedMaps-Isuuse.lean

[Yi.Yuan]

import Mathlib
universe u v w
variable {ι : Type v} [OrderedAddCommMonoid ι]
/--For `σ` satisfying `SetLike σ A`, an increasing series of `F` in `σ` is filtration if
there is another series `F_lt` equal to the supremum of `F` with smaller index-/
class IsFiltration {A : Type u} {σ : Type*} [SetLike σ A](F : ι → σ) (F_lt : outParam <| ι → σ) : Prop where
  mono {i j} : i ≤ j → F i ≤ F j
  is_le {i} : i < j → F i ≤ F_lt j
  is_sup (B : σ) (j : ι) : (∀ i < j, F i ≤ B) → F_lt j ≤ B
/- In fact `F_lt j = ⨆ i < j, F i`, the design of `F_lt` can handle different conditions in the
same structure, it avoid adding `CompleteLattice` to `σ`, also providing convenience when the index
is `ℤ`-/
variable {A : Type*} (σA : Type*) [SetLike σA A] {B : Type*}  (σB : Type*) [SetLike σB B]
class SubmonoidClassHom (f : A → B) where
  map : σA → σB
  coe_map (x : σA) : f '' (x : Set A) = map x
  comap : σB → σA/-I want to change `comap` and `coe_comap` to some weaker conditions-/
  coe_comap (y : σB) : (comap y : Set A) = f ⁻¹' y
def FB (FA : ι → σA) (f : A → B) [SubmonoidClassHom σA σB f]: ι → σB :=
  fun i ↦ SubmonoidClassHom.map f (FA i)
def FB_lt (FA_lt : ι → σA) (f : A → B) [SubmonoidClassHom σA σB f] : outParam <| ι → σB :=
  fun i ↦ SubmonoidClassHom.map f (FA_lt i)
open SubmonoidClassHom Set
/-
When FA and FA_lt is a filtration of A, then f: A → B induce a filtration of B
-/
lemma IsFiltration_isSup (FA : ι → σA) (FA_lt : ι → σA) (f : A → B) [fil : IsFiltration FA FA_lt]
[SubmonoidClassHom σA σB f] (Sup : σB)(h : ∀ i < j, FB σA σB FA f i ≤ Sup)
: ((SubmonoidClassHom.map f (FA_lt j) : σB): Set B) ≤ (Sup : Set B) := by
  rw[← SubmonoidClassHom.coe_map <| FA_lt j]
  refine Set.le_iff_subset.mpr <| Set.image_subset_iff.mpr ?_
  have h : ∀ i < j, ↑(FA i) ≤ f ⁻¹' ↑Sup := by
    intro i i_lt_j
    have : f '' (FA i) ≤ Sup := by
      have : ((SubmonoidClassHom.map f (FA i) : σB) : Set B) ≤ (Sup : Set B) := h i i_lt_j
      rwa[← SubmonoidClassHom.coe_map <| FA i] at this
    exact Set.le_iff_subset.mpr <| Set.image_subset_iff.mp this
/-How to finish the proof by using weaker conditions? -/
  have : (SubmonoidClassHom.comap f Sup : σA) = f ⁻¹' Sup := SubmonoidClassHom.coe_comap Sup
  rw[← this] at h ⊢
  exact IsFiltration.is_sup (SubmonoidClassHom.comap f Sup : σA) j h

[Aaron Liu]

I was able to make the condition weaker.

import Mathlib.Algebra.Order.Monoid.Defs
import Mathlib.Data.SetLike.Basic
import Mathlib.Order.GaloisConnection.Defs

variable {ι : Type*} [OrderedAddCommMonoid ι]

/--For `σ` satisfying `SetLike σ A`, an increasing series of `F` in `σ` is filtration if
there is another series `F_lt` equal to the supremum of `F` with smaller index-/

class IsFiltration {A σ : Type*} [SetLike σ A] (F : ι → σ) (F_lt : outParam (ι → σ)) : Prop where
  mono {i j} : i ≤ j → F i ≤ F j
  is_le {i} : i < j → F i ≤ F_lt j
  is_sup (B : σ) (j : ι) : (∀ i < j, F i ≤ B) → F_lt j ≤ B

/- In fact `F_lt j = ⨆ i < j, F i`, the design of `F_lt` can handle different conditions in the
same structure, it avoid adding `CompleteLattice` to `σ`, also providing convenience when the index
is `ℤ`-/
variable {A : Type*} (σA : Type*) [SetLike σA A] {B : Type*} (σB : Type*) [SetLike σB B]

-- f is now unused
class SubmonoidClassHom (f : A → B) where
  map : σA → σB
  comap : σB → σA
  galois : GaloisConnection map comap

open SubmonoidClassHom Set

/-
When FA and FA_lt is a filtration of A, then f: A → B induce a filtration of B
-/

lemma IsFiltration_isSup (FA FA_lt : ι → σA) (f : A → B) [fil : IsFiltration FA FA_lt]
    [SubmonoidClassHom σA σB f] (Sup : σB) (h : ∀ i < j, map f (FA i) ≤ Sup) :
    map f (FA_lt j) ≤ Sup := by
  apply galois.l_le
  have h : ∀ i < j, FA i ≤ comap f Sup := by
    intro i i_lt_j
    apply galois.le_u
    exact h i i_lt_j
  exact IsFiltration.is_sup (comap f Sup) j h

[Yi.Yuan]

thank you very much, it is a genius solution!!