# Zulip Chat Archive

## Stream: maths

### Topic: Ideal lemma

#### orlando (Mar 28 2020 at 09:16):

Hello,

I have a little problem !

lemma Test_2 (A B C:Type)[comm_ring A][comm_ring B][comm_ring C] (I : ideal A)(f: A → B) (g: B → C)[is_ring_hom f][is_ring_hom g]: ideal.map (g ∘ f) I = ideal.map g (ideal.map f I) := begin sorry, end

#### orlando (Mar 28 2020 at 09:17):

There is map_comp for module but not for ideal ! I don't understand how to deal !!!

#### Mario Carneiro (Mar 28 2020 at 09:21):

I think `ideal.map`

is just sugar over `module.map`

, so you may be able to prove this by just applying `module.map_comp`

#### orlando (Mar 28 2020 at 09:31):

Ok, but the little problem is $g$ is not $A$ module morphism

lemma map_comp (f : M →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) (p : submodule R M) : ```

#### Mario Carneiro (Mar 28 2020 at 09:34):

welp, I guess you will have to prove it ;)

#### Kevin Buzzard (Mar 28 2020 at 09:37):

`is_ring_hom`

is deprecated right? @orlando you should stop using it and use `ring_hom`

#### Kenny Lau (Mar 28 2020 at 09:37):

import ring_theory.ideal_operations lemma Test_2 (A B C : Type) [comm_ring A] [comm_ring B] [comm_ring C] (I : ideal A) (f : A → B) (g : B → C) [is_ring_hom f] [is_ring_hom g] : ideal.map (g ∘ f) I = ideal.map g (ideal.map f I) := le_antisymm (ideal.map_le_iff_le_comap.2 $ λ x hxI, ideal.mem_map_of_mem $ ideal.mem_map_of_mem hxI) (ideal.map_le_iff_le_comap.2 $ ideal.map_le_iff_le_comap.2 $ λ x hxI, ideal.mem_map_of_mem hxI)

#### Kevin Buzzard (Mar 28 2020 at 09:37):

Kenny can you do this with ring_hom?

#### Kevin Buzzard (Mar 28 2020 at 09:37):

Just to show Orlando the bundled approach?

#### Mario Carneiro (Mar 28 2020 at 09:37):

what was that galois connection emoji again

#### Kenny Lau (Mar 28 2020 at 09:38):

`ideal.map`

takes `is_ring_hom`

#### Kevin Buzzard (Mar 28 2020 at 09:39):

:-/

#### Mario Carneiro (Mar 28 2020 at 09:39):

refactor time

#### Kevin Buzzard (Mar 28 2020 at 09:41):

It's submodule.map we should be talking about not module.map

#### Kevin Buzzard (Mar 28 2020 at 09:42):

Ideals are submodules not modules

#### Mario Carneiro (Mar 28 2020 at 09:42):

zulip needs autocompletion

#### Kevin Buzzard (Mar 28 2020 at 09:42):

And easy ability to input Unicode on phones

#### orlando (Mar 28 2020 at 09:48):

I don't understand anything Mario ! But it's work :tada:

#### orlando (Mar 28 2020 at 09:51):

What is the $ ???

#### Kevin Buzzard (Mar 28 2020 at 09:51):

`a $ b c d`

is just `a (b c d)`

#### Kevin Buzzard (Mar 28 2020 at 09:52):

`$`

is notation (anything which is not letters and `_`

is usually notation) and you can see what it does with `#print notation $`

#### Mario Carneiro (Mar 28 2020 at 09:52):

we should put that in the faq

#### Kevin Buzzard (Mar 28 2020 at 09:53):

The output is `_ `$`:1 _:0 := #1 #0`

which means `a $ b := a b`

and make it right associative and have "power" 1 (which is low). Here's more information written for mathematicians

#### Mario Carneiro (Mar 28 2020 at 09:55):

It's too bad that looking up info on one piece of unfamimiar notation shows a whole bunch of unfamiliar notation

#### Kevin Buzzard (Mar 28 2020 at 09:55):

`$`

is particularly bad in this regard

#### Kevin Buzzard (Mar 28 2020 at 09:56):

because the binding powers are 1 and 0, and the missing variables are `#1`

and `#0`

#### Mario Carneiro (Mar 28 2020 at 09:56):

and they are numbered in reverse order because de bruijn thought it would be a good idea

#### Johan Commelin (Mar 28 2020 at 09:57):

Yes, I'm still wondering why he didn't use negative integers, so that they would be ordered the right way :rolling_on_the_floor_laughing:

#### Kevin Buzzard (Mar 28 2020 at 09:59):

You might naively think he'd want to use non-positive ones, but the negative integers are the inbuilt constructor

#### orlando (Mar 28 2020 at 18:35):

I make Ideals into a functor :grinning_face_with_smiling_eyes:

For the moment and don't understand really the difference between ring_hom and `(ψ : A ⟶ B)`

import algebra.category.CommRing import category_theory.types import ring_theory.ideals import ring_theory.ideal_operations universes u local notation `Ring` := CommRing.{u} local notation `Set` := Type u namespace ideal lemma ideal_id (A : Ring) (I : ideal A) : ideal.map (𝟙 A)I = I := begin have g : set.image (𝟙 A) I = (I : set A), exact set.image_id ↑I, unfold ideal.map, rw g, exact ideal.span_eq I, end lemma ideal_comp (A B C : Ring)(I : ideal A) (f : A ⟶ B) (g : B ⟶ C) : ideal.map (f ≫ g) I = ideal.map g (ideal.map f I) := le_antisymm (ideal.map_le_iff_le_comap.2 $ λ x hxI, ideal.mem_map_of_mem $ ideal.mem_map_of_mem hxI) (ideal.map_le_iff_le_comap.2 $ ideal.map_le_iff_le_comap.2 $ λ x hxI, ideal.mem_map_of_mem hxI) end ideal namespace Omega def Ω_obj (A : Ring):= ideal A def Ω_map (A B :Ring)(ψ : A ⟶ B) : Ω_obj A → Ω_obj B:= λ I,begin exact ideal.map ψ I, end def Ω : Ring ⥤ Set := { obj := Ω_obj, map := Ω_map, map_id' := λ A, begin funext I, rw category_theory.types_id, exact ideal.ideal_id A I, end, map_comp' := begin rintros, rw category_theory.types_comp, funext I, exact ideal.ideal_comp X Y Z I f g, end, } end Omega

#### Kevin Buzzard (Mar 28 2020 at 18:46):

The difference between `ring_hom`

and `is_ring_hom`

is the same as the difference between `CommRing`

and `comm_ring`

. With `ring_hom`

, the function is "bundled" as part of the structure. With `is_ring_hom`

it is an input. Similarly `comm_ring`

takes an input `R`

but `CommRing`

does not.

#### Johan Commelin (Mar 28 2020 at 18:47):

There isn't really a difference between those two types of homs. The difference is in what kind of objects you can stick at the end of the arrow (-;

If you use `ring_hom`

you give it two types `R`

and `S`

, and make sure that there are instances of `ring R`

or `comm_semiring S`

etc floating around.

If you use the category theory arrow, then you have to provide objects of the category `Ring`

or `CommRing`

, and those objects are types + a suitable instance, packaged together.

#### Kevin Buzzard (Mar 28 2020 at 18:48):

@orlando you can replace

λ I,begin exact ideal.map ψ I, end

with `exact ideal.map ψ`

. You don't even need to enter tactic mode.

#### Kevin Buzzard (Mar 28 2020 at 18:48):

Oh! You're talking about the `\hom`

arrow? Right, the only difference is that for one the inputs are unbundled and for the other the inputs are bundled.

#### Kevin Buzzard (Mar 28 2020 at 18:49):

Did you see the definition of functor in mathlib?

#### orlando (Mar 28 2020 at 18:49):

An exemple :

def V_obj (S : set R)(A : Ring) : Type u := { ζ : ring_hom R A | ∀ x ∈ S, ζ (x) = 0} --- if i use ζ : R ⟶ A i can't use ζ x = 0 ! Is it normal ?

#### Kevin Buzzard (Mar 28 2020 at 18:50):

structure functor (C : Type u₁) [category.{v₁} C] (D : Type u₂) [category.{v₂} D] : Type (max v₁ v₂ u₁ u₂) := (obj : C → D) (map : Π {X Y : C}, (X ⟶ Y) → ((obj X) ⟶ (obj Y))) (map_id' : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X) . obviously) (map_comp' : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = (map f) ≫ (map g) . obviously)

The last two structure fields -- `map_id'`

and `map_comp'`

have `. obviously`

at the end, which means "if the user does not prove them, try proving them yourself with the `obviously`

tactic".

#### Kevin Buzzard (Mar 28 2020 at 18:51):

I think it is possible to somehow train `obviously`

to be able to solve these things.

#### orlando (Mar 28 2020 at 18:51):

Hum the definition of functor yes but i don't understand ` obiously `

In my case of $\Omega$, without map_id' this doesn't works !

#### Kevin Buzzard (Mar 28 2020 at 18:52):

I don't understand it either. @Scott Morrison where do we learn about how to train `obviously`

to solve these cases of `map_id'`

and `map_comp'`

? Does it work like that?

#### Johan Commelin (Mar 28 2020 at 18:53):

Kevin Buzzard said:

I think it is possible to somehow train

`obviously`

to be able to solve these things.

The training is mostly done by proving the right simp-lemmas before you define the functor.

#### Johan Commelin (Mar 28 2020 at 18:54):

Currently `obviously`

cannot do `rw`

#### Johan Commelin (Mar 28 2020 at 18:54):

So if your proof really needs to do a `rw`

, then you have to do it your self.

#### Johan Commelin (Mar 28 2020 at 18:54):

But if the proof is something like `intros, ext, simp, assumption`

, then `obviously`

will fill in the proof for you.

#### Kevin Buzzard (Mar 28 2020 at 18:55):

So we need to make it a confluent rewrite situation

#### Reid Barton (Mar 28 2020 at 18:58):

I mean, you already did the work manually by proving `ideal_id`

and `ideal_comp`

, it just wasn't quite the right work

#### Kevin Buzzard (Mar 28 2020 at 18:58):

So we should be tagging these with `simp`

and also proving something about \Omega_map \b1 or something.

#### Reid Barton (Mar 28 2020 at 19:00):

The rewrites in `Ω`

are definitional equalities anyways. You could omit them and write the whole proof in term mode and it would be very short.

#### Kevin Buzzard (Mar 28 2020 at 19:00):

@orlando you should try and make the following proofs work:

map_id' := λ A, begin funext I, simp end, map_comp' := begin rintros, simp, funext I, simp end,

#### Reid Barton (Mar 28 2020 at 19:00):

Like, shorter than those proofs.

#### Reid Barton (Mar 28 2020 at 19:01):

(Although I guess the point is that you won't have to write those proofs because of `obviously`

)

#### Kevin Buzzard (Mar 28 2020 at 19:01):

See how far they get, and then if they don't finish the job, look at where they are stuck and add some simp lemmas to unstick them. Or is Reid saying that there's another way?

#### Reid Barton (Mar 28 2020 at 19:01):

Isn't `map_id' := \lam A, funext (\lam I, ideal.ideal_id A I)`

#### Kevin Buzzard (Mar 28 2020 at 19:01):

`attribute [simp] ideal.ideal_id`

I already got

#### Kevin Buzzard (Mar 28 2020 at 19:02):

but now I have

a : x_1 ∈ Ω_map X X (𝟙 X) x ⊢ x_1 ∈ x

#### Reid Barton (Mar 28 2020 at 19:02):

It's better to "inline" `Ω_obj`

`Ω_map`

anyways

#### Reid Barton (Mar 28 2020 at 19:03):

i.e.

def Ω : Ring ⥤ Set := { obj := ideal, ...

#### Kevin Buzzard (Mar 28 2020 at 19:03):

obj := λ A, ideal A, map := λ A B ψ, ideal.map ψ,

I can't get rid of A or psi

#### Reid Barton (Mar 28 2020 at 19:04):

Yeah, Lean is sometimes dumb :shrug:

#### orlando (Mar 28 2020 at 19:04):

The rw ` rw category_theory.types_id, `

in ` map_id ' `

is not necesarry

#### Kevin Buzzard (Mar 28 2020 at 19:09):

attribute [simp] ideal.ideal_id namespace Omega @[simp] lemma ideal.map_id (A : Ring) (J : ideal A) : ideal.map (𝟙 A) J = J := begin ext, simp, end def Ω : Ring ⥤ Set := { obj := λ A, ideal A, map := λ A B ψ, ideal.map ψ, map_comp' := begin rintros, rw category_theory.types_comp, funext I, exact ideal.ideal_comp X Y Z I f g, end, } end Omega

I now just get a (deterministic) timeout :-/

#### Kevin Buzzard (Mar 28 2020 at 19:09):

(having removed `map_id'`

)

#### Kevin Buzzard (Mar 28 2020 at 19:11):

wait what? `map_id' := begin intros, ext, simp end`

works fine, but `obviously`

just gets stuck in a loop :-(

#### Kevin Buzzard (Mar 28 2020 at 19:12):

No, I tell a lie!

#### Kevin Buzzard (Mar 28 2020 at 19:13):

I had assumed that this was going to end badly, but in fact it compiles fine!

elaboration of Ω took 75.4s

#### Kevin Buzzard (Mar 28 2020 at 19:14):

Scott -- is this a new record?

#### Reid Barton (Mar 28 2020 at 19:14):

can you have `tidy`

print a trace, then?

#### Kevin Buzzard (Mar 28 2020 at 19:14):

elaboration: tactic execution took 69.8s num. allocated objects: 1711 num. allocated closures: 1503 num. allocated big nums: 4 69848ms 100.0% tactic.replacer 69848ms 100.0% interaction_monad_orelse 69848ms 100.0% tactic.istep 69848ms 100.0% tactic.chain_core 69848ms 100.0% tactic.chain_many 69848ms 100.0% tactic.tidy.core 69848ms 100.0% tactic.step 69848ms 100.0% tactic.chain_many._main._lambda_1 69848ms 100.0% _interaction._lambda_2 69848ms 100.0% tactic.istep._lambda_1 69848ms 100.0% tactic.tidy 69848ms 100.0% tactic.first 69848ms 100.0% tactic.chain_single 69848ms 100.0% tactic.chain 69848ms 100.0% _interaction 69848ms 100.0% tactic.replacer_core 69848ms 100.0% scope_trace 69848ms 100.0% tactic.replacer_core._main._lambda_4 69800ms 99.9% tactic.tidy.default_tactics._lambda_3 68698ms 98.4% tactic.to_expr 68698ms 98.4% tactic.tidy.default_tactics._lambda_4 68698ms 98.4% tactic.interactive.exact 1014ms 1.5% tactic.tidy.default_tactics._lambda_8 1013ms 1.5% tactic.interactive.dsimp ...

#### Kevin Buzzard (Mar 28 2020 at 19:15):

Reid Barton said:

can you have

`tidy`

print a trace, then?

just a minute

#### Kevin Buzzard (Mar 28 2020 at 19:16):

Oh I just changed `obviously`

to `tidy`

assuming that this was what you meant, and it's no different. How do I get tidy to print a trace?

#### Reid Barton (Mar 28 2020 at 19:17):

`tidy?`

I think?

#### Kevin Buzzard (Mar 28 2020 at 19:17):

just a minute

#### Reid Barton (Mar 28 2020 at 19:18):

or slightly longer in this case

#### Kevin Buzzard (Mar 28 2020 at 19:18):

Try this: intros X, dsimp at *, ext1, dsimp at *, simp at *

#### Reid Barton (Mar 28 2020 at 19:19):

sometimes it is better to write the 1-line term mode proof and move on

#### Kevin Buzzard (Mar 28 2020 at 19:19):

Oh but that compiles in a reasonable time -- elaboration takes 1 second

#### Reid Barton (Mar 28 2020 at 19:20):

I guess it could be trying other things that fail

#### Kevin Buzzard (Mar 28 2020 at 19:20):

So every time there's an `obviously`

used in the library, we might be losing up to a minute of compile time when we could just go through them all and replace them with the one-liners which obviously finds, thus speeding up compile time but making the code look uglier.

#### Rob Lewis (Mar 28 2020 at 19:21):

(https://github.com/leanprover-community/mathlib/pull/1204)

#### Johan Commelin (Mar 28 2020 at 19:22):

It might be fun to count how many times there is a transparent call to `obviously`

in the library. Probably a lot.

#### Kevin Buzzard (Mar 28 2020 at 19:22):

`obviously`

should learn to tidy up after itself: it found `intros X, dsimp at *, ext1, dsimp at *, simp at *`

but `intros X, ext1, simp`

also works and is in some sense a strict subset of the proof originally found.

#### Kevin Buzzard (Mar 28 2020 at 19:24):

Yes I remember some discussion about this sort of thing when we were doing the T5000 challenge or whatever it was called. But I didn't understand things so well then -- I was more concerned with learning how to do mathematics in Lean at that time rather than learning how it all actually worked.

#### Kevin Buzzard (Mar 28 2020 at 19:27):

Hey many thanks for that link Rob -- there's a link to the T50000 thread and for me it's well worth a re-read. In particular Floris' comment to me near the top used to say (to me) "blah blah blah, it's like proving 1000+1000=2000 by rfl" which showed me what the problem basically was, but now I can understand what the problem actually was. At the time \ggg terrified me.

#### orlando (Mar 28 2020 at 19:51):

I read slowly,

So Kevin this work !

attribute [simp] ideal.ideal_id attribute [simp] ideal.ideal_comp namespace Omega def Ω_obj (A : Ring):= ideal A def Ω_map (A B :Ring)(ψ : A ⟶ B) : Ω_obj A → Ω_obj B:= λ I,begin exact ideal.map ψ I, end def Ω : Ring ⥤ Set := { obj := λ A, ideal A, map := λ A B ψ, ideal.map ψ, } end Omega

#### orlando (Mar 28 2020 at 19:51):

it's your code !

#### Kevin Buzzard (Mar 28 2020 at 19:53):

You can delete `\Omega_obj`

and `Omega_map`

-- Reid says it's better to just define them directly in the structure (like you are doing now)

#### orlando (Mar 28 2020 at 19:54):

yes !

#### Kevin Buzzard (Mar 28 2020 at 20:19):

Does your code now take 10 minutes to compile though? :-/

#### orlando (Mar 28 2020 at 20:32):

20 seconde with simp and 1 seconde with the first code !

#### orlando (Mar 28 2020 at 20:34):

I will make a natural transformation $\Omega \to \Omega$ given by $I \mapsto I^2$ , that's fun :grinning_face_with_smiling_eyes:

#### Kevin Buzzard (Mar 28 2020 at 20:45):

Well you can either prove the missing lemmas with `tidy`

and then click on "try this" (and then it will be quick again) or you can finish this file now, compile it into an olean file, and then import it :-)

#### orlando (Mar 28 2020 at 20:46):

hum what is olean ?

#### orlando (Mar 28 2020 at 20:46):

perhaps i don't understand "compile"

#### Kevin Buzzard (Mar 28 2020 at 20:47):

Are you making these files in a lean project? I hope so. You can just stop editing this file now and start a new file and import this file

#### Kevin Buzzard (Mar 28 2020 at 20:48):

Because this file takes 20 seconds to compile now (the orange bars) but if you import it then it will just compile once and then never compile again until you restart VS code or lean

#### orlando (Mar 28 2020 at 20:48):

Yes yes in a lean project, ok

#### orlando (Mar 28 2020 at 20:48):

i understand

#### Kevin Buzzard (Mar 28 2020 at 20:49):

Or alternatively you can write `lean --make path/to/file.lean`

and then you will have a compiled olean file on your computer

#### Kevin Buzzard (Mar 28 2020 at 20:50):

And then even after you restart lean and Vs code it will still be quick because the olean file stores the 20 seconds

#### Kevin Buzzard (Mar 28 2020 at 20:50):

The reason you don't get orange bars for one hour when you start to use mathlib is because all the oleans are on your computer thanks to leanproject

#### orlando (Mar 28 2020 at 20:51):

ohhh ok !!!

#### Kevin Buzzard (Mar 28 2020 at 20:51):

But in your project there are probably no olean files

#### Kevin Buzzard (Mar 28 2020 at 20:52):

So every time you open the project it has to compile all the files you made which you use or import

#### Kevin Buzzard (Mar 28 2020 at 20:53):

And if one of them takes 20 seconds then this is a pain

#### orlando (Mar 28 2020 at 20:57):

hum i do lean --make but i don't see olean file !

#### Kevin Buzzard (Mar 28 2020 at 21:05):

Do lean --make src/file.lean and it will make file.olean in src

#### Reid Barton (Mar 28 2020 at 21:07):

is `leanpkg build`

no longer a cool thing to do?

#### Kevin Buzzard (Mar 28 2020 at 22:23):

Leanproject build ftw

#### orlando (Mar 30 2020 at 08:15):

Hello, just a question

0/ Omega is the previous files.

1/ In square_ideal_naturality : is it possible to simplify the construction without using the line ` have H : (Ω.map ψ ∘ square_ideal_app A) I = ideal.map ψ (I * I) `

and do the `rw H `

directly ?

open Omega variables (A :Ring) def square_ideal_app (A : Ring) : ideal A → ideal A := λ I, begin exact (I * I), end def square_ideal_naturality (A B :Ring) (ψ : A ⟶ B) : Ω.map ψ ≫ square_ideal_app B = square_ideal_app A ≫ Ω.map ψ := begin rw [category_theory.types_comp,category_theory.types_comp], funext I, have H : (Ω.map ψ ∘ square_ideal_app A) I = ideal.map ψ (I * I), exact rfl, rw H, rw ideal.map_mul ψ I I, exact rfl, end def square_ideal : Ω ⟶ Ω := { app := λ A : Ring, square_ideal_app A, naturality' := square_ideal_naturality, } end Omega_2

#### Kenny Lau (Mar 30 2020 at 08:25):

`rw [show _ = _, from rfl]`

#### orlando (Mar 30 2020 at 08:33):

Ok, thx Kenny,

#### orlando (Apr 07 2020 at 19:43):

Hello,

Another problem with Ideal :confused:

import algebra.category.CommRing import ring_theory.ideals import ring_theory.ideal_operations universes u local notation `Ring` := CommRing.{u} local notation `Set` := Type u lemma set_image_S_subset_set_image_span_S (A B : Ring )(f : A ⟶ B) (S : set A) : set.image f S ⊆ set.image f (ideal.span S) := begin apply set.image_subset, exact ideal.subset_span, end lemma ideal.map_span_eq_span_image(A B : Ring )(f : A ⟶ B) (S : set A): ideal.span (set.image f S) = ideal.map f (ideal.span S) := begin unfold ideal.map, apply le_antisymm, exact ideal.span_mono (set_image_S_subset_set_image_span_S A B f S), have ccl : set.image f (ideal.span S) ⊆ ideal.span (set.image f S), sorry, ---- HERE !!!! apply ideal.span_le.2 ccl, end

#### Yury G. Kudryashov (Apr 07 2020 at 19:48):

Here is the proof for `submonoid`

s:

lemma closure_preimage_le (f : M →* N) (s : set N) : closure (f ⁻¹' s) ≤ (closure s).comap f := closure_le.2 $ λ x hx, mem_coe.2 $ mem_comap.2 $ subset_closure hx lemma map_mclosure (f : M →* N) (s : set M) : (closure s).map f = closure (f '' s) := le_antisymm (map_le_iff_le_comap.2 $ le_trans (closure_mono $ set.subset_preimage_image _ _) (closure_preimage_le _ _)) (closure_le.2 $ set.image_subset _ subset_closure)

#### Yury G. Kudryashov (Apr 07 2020 at 19:49):

I think that something similar can be done for ideals as well.

#### orlando (Apr 07 2020 at 19:56):

ok i thinck ` (closure_le.2 $ set.image_subset _ subset_closure) `

is the same than my ` exact ideal.span_mono (set_image_S_subset_set_image_span_S A B f S), `

So if i understand, i have to deal with ` comap `

... ahah Kenny play also with comap at the beginning of the topic here

#### Yury G. Kudryashov (Apr 07 2020 at 19:57):

`comap`

is the preimage

#### Kevin Buzzard (Apr 07 2020 at 20:16):

`map`

= image = pushforward, `comap`

= pullback = preimage

#### orlando (Apr 07 2020 at 20:27):

Ok perhaps it's not the shortest proof :joy:

import algebra.category.CommRing import ring_theory.ideals import ring_theory.ideal_operations universes u local notation `Ring` := CommRing.{u} local notation `Set` := Type u lemma set_image_S_subset_set_image_span_S (A B : Ring )(f : A ⟶ B) (S : set A) : set.image f S ⊆ set.image f (ideal.span S) := begin apply set.image_subset, exact ideal.subset_span, end lemma ideal.map_span_eq_span_image(A B : Ring )(f : A ⟶ B) (S : set A): ideal.span (set.image f S) = ideal.map f (ideal.span S) := begin -- unfold ideal.map, apply le_antisymm, exact ideal.span_mono (set_image_S_subset_set_image_span_S A B f S), have ccl3 : S ≤ ideal.comap f (ideal.span (set.image f S)), unfold ideal.comap, have T : S ⊆ ⇑f ⁻¹' ↑(ideal.span (⇑f '' S)), have T' : set.image f S ⊆ ↑(ideal.span (⇑f '' S)), exact ideal.subset_span, apply set.image_subset_iff.1 T', exact T, have ccl2 : ideal.span S ≤ ideal.comap f (ideal.span (set.image f S)), apply ideal.span_le.2 ccl3, have ccl : ideal.map f (ideal.span S) ≤ ideal.span (set.image f S), apply ideal.map_le_iff_le_comap.2 ccl2, exact ccl, end

#### orlando (Apr 07 2020 at 20:35):

lemma set_image_S_subset_set_image_span_S (A B : Ring )(f : A ⟶ B) (S : set A) : set.image f S ⊆ set.image f (ideal.span S) := begin apply set.image_subset, exact ideal.subset_span, end lemma ideal.map_span_eq_span_image(A B : Ring )(f : A ⟶ B) (S : set A): ideal.span (set.image f S) = ideal.map f (ideal.span S) := begin apply le_antisymm, exact ideal.span_mono (set_image_S_subset_set_image_span_S A B f S), exact ideal.map_le_iff_le_comap.2 (ideal.span_le.2 (set.image_subset_iff.1 (ideal.subset_span))), end

#### orlando (Apr 07 2020 at 20:36):

shorter :grinning_face_with_smiling_eyes:

#### Yury G. Kudryashov (Apr 07 2020 at 20:44):

I wonder what is the general statement here. Probably it should involve four `galois_insertion`

s (two closure/coe, image/preimage, and map/comap).

#### Kevin Buzzard (Apr 07 2020 at 20:54):

Hey @orlando it's great that your proofs got shorter -- now can you write them in term mode? That way they will compile quicker

#### Patrick Massot (Apr 07 2020 at 20:55):

I'm not sure this is true.

#### Kevin Buzzard (Apr 07 2020 at 20:55):

Opening up tactic mode has a cost, no?

#### Yury G. Kudryashov (Apr 07 2020 at 20:59):

For short proofs this should be true but for longer proofs elaborating parts one after another may help Lean. At least I remember some proofs that were failing in term mode because Lean wanted to elaborate arguments left to right. Rewriting using `refine; exact`

made them work. I suspect that it's possible to make an example where "fails" will be replaced by "slow".

#### orlando (Apr 07 2020 at 20:59):

without Begin end ??? Kevin ?

#### Yury G. Kudryashov (Apr 07 2020 at 21:05):

BTW, you can use `#print`

to see the term mode proof generated by your tactic mode proof.

#### Yury G. Kudryashov (Apr 07 2020 at 21:05):

It can be much longer than the tactic proof.

#### orlando (Apr 09 2020 at 15:34):

hum another problem i don't know how to do this without the description in term of linear combinaison :confused:

import algebra.category.CommRing import ring_theory.ideals import ring_theory.ideal_operations local notation `Ring` := CommRing. lemma inverse_image_ideal (A B : Ring)(f : A ⟶ B)(S : set B) : ideal.span (set.preimage f S) = ideal.comap f (ideal.span S) := begin apply le_antisymm, -- double inclusion rw ideal.span_le, -- span S \leq I ↔ S ≤ I apply set.preimage_mono ideal.subset_span, sorry, end

#### Kevin Buzzard (Apr 09 2020 at 15:43):

Is this true?

#### Kevin Buzzard (Apr 09 2020 at 15:44):

What about $A=\mathbb{Z}$ and $B=\mathbb{C}$ and $S=\{\pi\}$?

#### Kevin Buzzard (Apr 09 2020 at 15:46):

You have access to "proof using linear combination" with things like `submodule.span_induction`

#### orlando (Apr 09 2020 at 16:03):

:face_palm: :face_palm:

Last updated: May 19 2021 at 02:10 UTC