## 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

:-/

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:

#### 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

$ 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): #### 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 submonoids: 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_insertions (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


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