Skip to content

Commit 42ced2f

Browse files
mattrobballmattrobball
committed
Merge branch 'master' into mrb/instance_fields
2 parents 3c4f594 + 41b6cc2 commit 42ced2f

49 files changed

Lines changed: 852 additions & 164 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎Archive/MiuLanguage/DecisionSuf.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -153,7 +153,7 @@ private theorem le_pow2_and_pow2_eq_mod3' (c : ℕ) (x : ℕ) (h : c = 1 ∨ c =
153153
cases' h with hc hc <;> · rw [hc]; norm_num
154154
rcases hk with ⟨g, hkg, hgmod⟩
155155
by_cases hp : c + 3 * (k + 1) ≤ 2 ^ g
156-
· use g; exact ⟨hp, hgmod⟩
156+
· use g, hp, hgmod
157157
refine' ⟨g + 2, _, _⟩
158158
· rw [mul_succ, ← add_assoc, pow_add]
159159
change c + 3 * k + 3 ≤ 2 ^ g * (1 + 3); rw [mul_add (2 ^ g) 1 3, mul_one]

‎Archive/Wiedijk100Theorems/SumOfPrimeReciprocalsDiverges.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -152,7 +152,7 @@ theorem card_le_two_pow {x k : ℕ} :
152152
intro m hm
153153
simp only [M, mem_filter, mem_range, mem_powerset, mem_image, exists_prop] at hm ⊢
154154
obtain ⟨⟨-, hmp⟩, hms⟩ := hm
155-
use ⟨(m + 1).factors, ?_⟩
155+
use! (m + 1).factors
156156
· rwa [Multiset.coe_nodup, ← Nat.squarefree_iff_nodup_factors m.succ_ne_zero]
157157
refine' ⟨fun p => _, _⟩
158158
· suffices p ∈ (m + 1).factors → ∃ a : ℕ, a < k ∧ a.succ = p by simpa

‎Mathlib.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1664,7 +1664,6 @@ import Mathlib.Data.Polynomial.HasseDeriv
16641664
import Mathlib.Data.Polynomial.Identities
16651665
import Mathlib.Data.Polynomial.Induction
16661666
import Mathlib.Data.Polynomial.Inductions
1667-
import Mathlib.Data.Polynomial.IntegralNormalization
16681667
import Mathlib.Data.Polynomial.Laurent
16691668
import Mathlib.Data.Polynomial.Lifts
16701669
import Mathlib.Data.Polynomial.Mirror
@@ -2818,6 +2817,7 @@ import Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
28182817
import Mathlib.RingTheory.Polynomial.GaussLemma
28192818
import Mathlib.RingTheory.Polynomial.Hermite.Basic
28202819
import Mathlib.RingTheory.Polynomial.Hermite.Gaussian
2820+
import Mathlib.RingTheory.Polynomial.IntegralNormalization
28212821
import Mathlib.RingTheory.Polynomial.Opposites
28222822
import Mathlib.RingTheory.Polynomial.Pochhammer
28232823
import Mathlib.RingTheory.Polynomial.Quotient

‎Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -133,8 +133,7 @@ theorem exists_rat_eq_of_terminates (terminates : (of v).Terminates) : ∃ q :
133133
obtain ⟨q, conv_eq_q⟩ : ∃ q : ℚ, (of v).convergents n = (↑q : K)
134134
exact exists_rat_eq_nth_convergent v n
135135
have : v = (↑q : K) := Eq.trans v_eq_conv conv_eq_q
136-
-- Porting note(https://github.com/leanprover-community/mathlib4/issues/5072): was `use`
137-
exact ⟨q, this⟩
136+
use q, this
138137
#align generalized_continued_fraction.exists_rat_eq_of_terminates GeneralizedContinuedFraction.exists_rat_eq_of_terminates
139138

140139
end RatOfTerminates
@@ -317,7 +316,7 @@ theorem stream_nth_fr_num_le_fr_num_sub_n_rat :
317316
theorem exists_nth_stream_eq_none_of_rat (q : ℚ) : ∃ n : ℕ, IntFractPair.stream q n = none := by
318317
let fract_q_num := (Int.fract q).num; let n := fract_q_num.natAbs + 1
319318
cases' stream_nth_eq : IntFractPair.stream q n with ifp
320-
· use n; exact stream_nth_eq
319+
· use n, stream_nth_eq
321320
· -- arrive at a contradiction since the numerator decreased num + 1 times but every fractional
322321
-- value is nonnegative.
323322
have ifp_fr_num_le_q_fr_num_sub_n : ifp.fr.num ≤ fract_q_num - n :=

‎Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean‎

Lines changed: 313 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -404,10 +404,323 @@ variable {φ h₁ h₂}
404404
lemma congr_φH {γ₁ γ₂ : RightHomologyMapData φ h₁ h₂} (eq : γ₁ = γ₂) : γ₁.φH = γ₂.φH := by rw [eq]
405405
lemma congr_φQ {γ₁ γ₂ : RightHomologyMapData φ h₁ h₂} (eq : γ₁ = γ₂) : γ₁.φQ = γ₂.φQ := by rw [eq]
406406

407+
/-- When `S₁.f`, `S₁.g`, `S₂.f` and `S₂.g` are all zero, the action on right homology of a
408+
morphism `φ : S₁ ⟶ S₂` is given by the action `φ.τ₂` on the middle objects. -/
409+
@[simps]
410+
def ofZeros (φ : S₁ ⟶ S₂) (hf₁ : S₁.f = 0) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0) (hg₂ : S₂.g = 0) :
411+
RightHomologyMapData φ (RightHomologyData.ofZeros S₁ hf₁ hg₁)
412+
(RightHomologyData.ofZeros S₂ hf₂ hg₂) where
413+
φQ := φ.τ₂
414+
φH := φ.τ₂
415+
416+
/-- When `S₁.f` and `S₂.f` are zero and we have chosen limit kernel forks `c₁` and `c₂`
417+
for `S₁.g` and `S₂.g` respectively, the action on right homology of a morphism `φ : S₁ ⟶ S₂` of
418+
short complexes is given by the unique morphism `f : c₁.pt ⟶ c₂.pt` such that
419+
`c₁.ι ≫ φ.τ₂ = f ≫ c₂.ι`. -/
420+
@[simps]
421+
def ofIsLimitKernelFork (φ : S₁ ⟶ S₂)
422+
(hf₁ : S₁.f = 0) (c₁ : KernelFork S₁.g) (hc₁ : IsLimit c₁)
423+
(hf₂ : S₂.f = 0) (c₂ : KernelFork S₂.g) (hc₂ : IsLimit c₂) (f : c₁.pt ⟶ c₂.pt)
424+
(comm : c₁.ι ≫ φ.τ₂ = f ≫ c₂.ι) :
425+
RightHomologyMapData φ (RightHomologyData.ofIsLimitKernelFork S₁ hf₁ c₁ hc₁)
426+
(RightHomologyData.ofIsLimitKernelFork S₂ hf₂ c₂ hc₂) where
427+
φQ := φ.τ₂
428+
φH := f
429+
commg' := by simp only [RightHomologyData.ofIsLimitKernelFork_g', φ.comm₂₃]
430+
commι := comm.symm
431+
432+
/-- When `S₁.g` and `S₂.g` are zero and we have chosen colimit cokernel coforks `c₁` and `c₂`
433+
for `S₁.f` and `S₂.f` respectively, the action on right homology of a morphism `φ : S₁ ⟶ S₂` of
434+
short complexes is given by the unique morphism `f : c₁.pt ⟶ c₂.pt` such that
435+
`φ.τ₂ ≫ c₂.π = c₁.π ≫ f`. -/
436+
@[simps]
437+
def ofIsColimitCokernelCofork (φ : S₁ ⟶ S₂)
438+
(hg₁ : S₁.g = 0) (c₁ : CokernelCofork S₁.f) (hc₁ : IsColimit c₁)
439+
(hg₂ : S₂.g = 0) (c₂ : CokernelCofork S₂.f) (hc₂ : IsColimit c₂) (f : c₁.pt ⟶ c₂.pt)
440+
(comm : φ.τ₂ ≫ c₂.π = c₁.π ≫ f) :
441+
RightHomologyMapData φ (RightHomologyData.ofIsColimitCokernelCofork S₁ hg₁ c₁ hc₁)
442+
(RightHomologyData.ofIsColimitCokernelCofork S₂ hg₂ c₂ hc₂) where
443+
φQ := f
444+
φH := f
445+
commp := comm.symm
446+
447+
variable (S)
448+
449+
/-- When both maps `S.f` and `S.g` of a short complex `S` are zero, this is the homology map
450+
data (for the identity of `S`) which relates the right homology data
451+
`RightHomologyData.ofIsLimitKernelFork` and `ofZeros` . -/
452+
@[simps]
453+
def compatibilityOfZerosOfIsLimitKernelFork (hf : S.f = 0) (hg : S.g = 0)
454+
(c : KernelFork S.g) (hc : IsLimit c) :
455+
RightHomologyMapData (𝟙 S)
456+
(RightHomologyData.ofIsLimitKernelFork S hf c hc)
457+
(RightHomologyData.ofZeros S hf hg) where
458+
φQ := 𝟙 _
459+
φH := c.ι
460+
461+
/-- When both maps `S.f` and `S.g` of a short complex `S` are zero, this is the homology map
462+
data (for the identity of `S`) which relates the right homology data `ofZeros` and
463+
`ofIsColimitCokernelCofork`. -/
464+
@[simps]
465+
def compatibilityOfZerosOfIsColimitCokernelCofork (hf : S.f = 0) (hg : S.g = 0)
466+
(c : CokernelCofork S.f) (hc : IsColimit c) :
467+
RightHomologyMapData (𝟙 S)
468+
(RightHomologyData.ofZeros S hf hg)
469+
(RightHomologyData.ofIsColimitCokernelCofork S hg c hc) where
470+
φQ := c.π
471+
φH := c.π
472+
407473
end RightHomologyMapData
408474

409475
end
410476

477+
section
478+
479+
variable (S)
480+
variable [S.HasRightHomology]
481+
482+
/-- The right homology of a short complex,
483+
given by the `H` field of a chosen right homology data. -/
484+
noncomputable def rightHomology : C := S.rightHomologyData.H
485+
486+
/-- The "opcycles" of a short complex, given by the `Q` field of a chosen right homology data.
487+
This is the dual notion to cycles. -/
488+
noncomputable def opcycles : C := S.rightHomologyData.Q
489+
490+
/-- The canonical map `S.rightHomology ⟶ S.opcycles`. -/
491+
noncomputable def rightHomologyι : S.rightHomology ⟶ S.opcycles :=
492+
S.rightHomologyData.ι
493+
494+
/-- The projection `S.X₂ ⟶ S.opcycles`. -/
495+
noncomputable def pOpcycles : S.X₂ ⟶ S.opcycles := S.rightHomologyData.p
496+
497+
/-- The canonical map `S.opcycles ⟶ X₃`. -/
498+
noncomputable def fromOpcycles : S.opcycles ⟶ S.X₃ := S.rightHomologyData.g'
499+
500+
@[reassoc (attr := simp)]
501+
lemma f_pOpcycles : S.f ≫ S.pOpcycles = 0 := S.rightHomologyData.wp
502+
503+
@[reassoc (attr := simp)]
504+
lemma p_fromOpcycles : S.pOpcycles ≫ S.fromOpcycles = S.g := S.rightHomologyData.p_g'
505+
506+
instance : Epi S.pOpcycles := by
507+
dsimp only [pOpcycles]
508+
infer_instance
509+
510+
instance : Mono S.rightHomologyι := by
511+
dsimp only [rightHomologyι]
512+
infer_instance
513+
514+
lemma rightHomology_ext_iff (f₁ f₂ : A ⟶ S.rightHomology) :
515+
f₁ = f₂ ↔ f₁ ≫ S.rightHomologyι = f₂ ≫ S.rightHomologyι := by
516+
rw [cancel_mono]
517+
518+
@[ext]
519+
lemma rightHomology_ext (f₁ f₂ : A ⟶ S.rightHomology)
520+
(h : f₁ ≫ S.rightHomologyι = f₂ ≫ S.rightHomologyι) : f₁ = f₂ := by
521+
simpa only [rightHomology_ext_iff]
522+
523+
lemma opcycles_ext_iff (f₁ f₂ : S.opcycles ⟶ A) :
524+
f₁ = f₂ ↔ S.pOpcycles ≫ f₁ = S.pOpcycles ≫ f₂ := by
525+
rw [cancel_epi]
526+
527+
@[ext]
528+
lemma opcycles_ext (f₁ f₂ : S.opcycles ⟶ A)
529+
(h : S.pOpcycles ≫ f₁ = S.pOpcycles ≫ f₂) : f₁ = f₂ := by
530+
simpa only [opcycles_ext_iff]
531+
532+
lemma isIso_pOpcycles (hf : S.f = 0) : IsIso S.pOpcycles :=
533+
RightHomologyData.isIso_p _ hf
534+
535+
/-- When `S.f = 0`, this is the canonical isomorphism `S.opcycles ≅ S.X₂`
536+
induced by `S.pOpcycles`. -/
537+
@[simps! inv]
538+
noncomputable def opcyclesIsoX₂ (hf : S.f = 0) : S.opcycles ≅ S.X₂ := by
539+
have := S.isIso_pOpcycles hf
540+
exact (asIso S.pOpcycles).symm
541+
542+
@[reassoc (attr := simp)]
543+
lemma opcyclesIsoX₂_inv_hom_id (hf : S.f = 0) :
544+
S.pOpcycles ≫ (S.opcyclesIsoX₂ hf).hom = 𝟙 _ := (S.opcyclesIsoX₂ hf).inv_hom_id
545+
546+
@[reassoc (attr := simp)]
547+
lemma opcyclesIsoX₂_hom_inv_id (hf : S.f = 0) :
548+
(S.opcyclesIsoX₂ hf).hom ≫ S.pOpcycles = 𝟙 _ := (S.opcyclesIsoX₂ hf).hom_inv_id
549+
550+
lemma isIso_rightHomologyι (hg : S.g = 0) : IsIso S.rightHomologyι :=
551+
RightHomologyData.isIso_ι _ hg
552+
553+
/-- When `S.g = 0`, this is the canonical isomorphism `S.opcycles ≅ S.rightHomology` induced
554+
by `S.rightHomologyι`. -/
555+
@[simps! inv]
556+
noncomputable def opcyclesIsoRightHomology (hg : S.g = 0) : S.opcycles ≅ S.rightHomology := by
557+
have := S.isIso_rightHomologyι hg
558+
exact (asIso S.rightHomologyι).symm
559+
560+
@[reassoc (attr := simp)]
561+
lemma opcyclesIsoRightHomology_inv_hom_id (hg : S.g = 0) :
562+
S.rightHomologyι ≫ (S.opcyclesIsoRightHomology hg).hom = 𝟙 _ :=
563+
(S.opcyclesIsoRightHomology hg).inv_hom_id
564+
565+
@[reassoc (attr := simp)]
566+
lemma opcyclesIsoRightHomology_hom_inv_id (hg : S.g = 0) :
567+
(S.opcyclesIsoRightHomology hg).hom ≫ S.rightHomologyι = 𝟙 _ :=
568+
(S.opcyclesIsoRightHomology hg).hom_inv_id
569+
570+
end
571+
572+
section
573+
574+
variable (φ : S₁ ⟶ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData)
575+
576+
/-- The (unique) right homology map data associated to a morphism of short complexes that
577+
are both equipped with right homology data. -/
578+
def rightHomologyMapData : RightHomologyMapData φ h₁ h₂ := default
579+
580+
/-- Given a morphism `φ : S₁ ⟶ S₂` of short complexes and right homology data `h₁` and `h₂`
581+
for `S₁` and `S₂` respectively, this is the induced right homology map `h₁.H ⟶ h₁.H`. -/
582+
def rightHomologyMap' : h₁.H ⟶ h₂.H := (rightHomologyMapData φ _ _).φH
583+
584+
/-- Given a morphism `φ : S₁ ⟶ S₂` of short complexes and right homology data `h₁` and `h₂`
585+
for `S₁` and `S₂` respectively, this is the induced morphism `h₁.K ⟶ h₁.K` on opcycles. -/
586+
def opcyclesMap' : h₁.Q ⟶ h₂.Q := (rightHomologyMapData φ _ _).φQ
587+
588+
@[reassoc (attr := simp)]
589+
lemma p_opcyclesMap' : h₁.p ≫ opcyclesMap' φ h₁ h₂ = φ.τ₂ ≫ h₂.p :=
590+
RightHomologyMapData.commp _
591+
592+
@[reassoc (attr := simp)]
593+
lemma opcyclesMap'_g' : opcyclesMap' φ h₁ h₂ ≫ h₂.g' = h₁.g' ≫ φ.τ₃ := by
594+
simp only [← cancel_epi h₁.p, assoc, φ.comm₂₃, p_opcyclesMap'_assoc,
595+
RightHomologyData.p_g'_assoc, RightHomologyData.p_g']
596+
597+
@[reassoc (attr := simp)]
598+
lemma rightHomologyι_naturality' :
599+
rightHomologyMap' φ h₁ h₂ ≫ h₂.ι = h₁.ι ≫ opcyclesMap' φ h₁ h₂ :=
600+
RightHomologyMapData.commι _
601+
602+
end
603+
604+
section
605+
606+
variable [HasRightHomology S₁] [HasRightHomology S₂] (φ : S₁ ⟶ S₂)
607+
608+
/-- The (right) homology map `S₁.rightHomology ⟶ S₂.rightHomology` induced by a morphism
609+
`S₁ ⟶ S₂` of short complexes. -/
610+
noncomputable def rightHomologyMap : S₁.rightHomology ⟶ S₂.rightHomology :=
611+
rightHomologyMap' φ _ _
612+
613+
/-- The morphism `S₁.opcycles ⟶ S₂.opcycles` induced by a morphism `S₁ ⟶ S₂` of short complexes. -/
614+
noncomputable def opcyclesMap : S₁.opcycles ⟶ S₂.opcycles :=
615+
opcyclesMap' φ _ _
616+
617+
@[reassoc (attr := simp)]
618+
lemma p_opcyclesMap : S₁.pOpcycles ≫ opcyclesMap φ = φ.τ₂ ≫ S₂.pOpcycles :=
619+
p_opcyclesMap' _ _ _
620+
621+
@[reassoc (attr := simp)]
622+
lemma fromOpcycles_naturality : opcyclesMap φ ≫ S₂.fromOpcycles = S₁.fromOpcycles ≫ φ.τ₃ :=
623+
opcyclesMap'_g' _ _ _
624+
625+
@[reassoc (attr := simp)]
626+
lemma rightHomologyι_naturality :
627+
rightHomologyMap φ ≫ S₂.rightHomologyι = S₁.rightHomologyι ≫ opcyclesMap φ :=
628+
rightHomologyι_naturality' _ _ _
629+
630+
end
631+
632+
namespace RightHomologyMapData
633+
634+
variable {φ : S₁ ⟶ S₂} {h₁ : S₁.RightHomologyData} {h₂ : S₂.RightHomologyData}
635+
(γ : RightHomologyMapData φ h₁ h₂)
636+
637+
lemma rightHomologyMap'_eq : rightHomologyMap' φ h₁ h₂ = γ.φH :=
638+
RightHomologyMapData.congr_φH (Subsingleton.elim _ _)
639+
640+
lemma opcyclesMap'_eq : opcyclesMap' φ h₁ h₂ = γ.φQ :=
641+
RightHomologyMapData.congr_φQ (Subsingleton.elim _ _)
642+
643+
end RightHomologyMapData
644+
645+
@[simp]
646+
lemma rightHomologyMap'_id (h : S.RightHomologyData) :
647+
rightHomologyMap' (𝟙 S) h h = 𝟙 _ :=
648+
(RightHomologyMapData.id h).rightHomologyMap'_eq
649+
650+
@[simp]
651+
lemma opcyclesMap'_id (h : S.RightHomologyData) :
652+
opcyclesMap' (𝟙 S) h h = 𝟙 _ :=
653+
(RightHomologyMapData.id h).opcyclesMap'_eq
654+
655+
variable (S)
656+
657+
@[simp]
658+
lemma rightHomologyMap_id [HasRightHomology S] :
659+
rightHomologyMap (𝟙 S) = 𝟙 _ :=
660+
rightHomologyMap'_id _
661+
662+
@[simp]
663+
lemma opcyclesMap_id [HasRightHomology S] :
664+
opcyclesMap (𝟙 S) = 𝟙 _ :=
665+
opcyclesMap'_id _
666+
667+
@[simp]
668+
lemma rightHomologyMap'_zero (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) :
669+
rightHomologyMap' 0 h₁ h₂ = 0 :=
670+
(RightHomologyMapData.zero h₁ h₂).rightHomologyMap'_eq
671+
672+
@[simp]
673+
lemma opcyclesMap'_zero (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) :
674+
opcyclesMap' 0 h₁ h₂ = 0 :=
675+
(RightHomologyMapData.zero h₁ h₂).opcyclesMap'_eq
676+
677+
variable (S₁ S₂)
678+
679+
@[simp]
680+
lemma rightHomologyMap_zero [HasRightHomology S₁] [HasRightHomology S₂] :
681+
rightHomologyMap (0 : S₁ ⟶ S₂) = 0 :=
682+
rightHomologyMap'_zero _ _
683+
684+
@[simp]
685+
lemma opcyclesMap_zero [HasRightHomology S₁] [HasRightHomology S₂] :
686+
opcyclesMap (0 : S₁ ⟶ S₂) = 0 :=
687+
opcyclesMap'_zero _ _
688+
689+
variable {S₁ S₂}
690+
691+
@[reassoc]
692+
lemma rightHomologyMap'_comp (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃)
693+
(h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) (h₃ : S₃.RightHomologyData) :
694+
rightHomologyMap' (φ₁ ≫ φ₂) h₁ h₃ = rightHomologyMap' φ₁ h₁ h₂ ≫
695+
rightHomologyMap' φ₂ h₂ h₃ := by
696+
let γ₁ := rightHomologyMapData φ₁ h₁ h₂
697+
let γ₂ := rightHomologyMapData φ₂ h₂ h₃
698+
rw [γ₁.rightHomologyMap'_eq, γ₂.rightHomologyMap'_eq, (γ₁.comp γ₂).rightHomologyMap'_eq,
699+
RightHomologyMapData.comp_φH]
700+
701+
@[reassoc]
702+
lemma opcyclesMap'_comp (φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃)
703+
(h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData) (h₃ : S₃.RightHomologyData) :
704+
opcyclesMap' (φ₁ ≫ φ₂) h₁ h₃ = opcyclesMap' φ₁ h₁ h₂ ≫ opcyclesMap' φ₂ h₂ h₃ := by
705+
let γ₁ := rightHomologyMapData φ₁ h₁ h₂
706+
let γ₂ := rightHomologyMapData φ₂ h₂ h₃
707+
rw [γ₁.opcyclesMap'_eq, γ₂.opcyclesMap'_eq, (γ₁.comp γ₂).opcyclesMap'_eq,
708+
RightHomologyMapData.comp_φQ]
709+
710+
@[simp]
711+
lemma rightHomologyMap_comp [HasRightHomology S₁] [HasRightHomology S₂] [HasRightHomology S₃]
712+
(φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃) :
713+
rightHomologyMap (φ₁ ≫ φ₂) = rightHomologyMap φ₁ ≫ rightHomologyMap φ₂ :=
714+
rightHomologyMap'_comp _ _ _ _ _
715+
716+
@[simp]
717+
lemma opcyclesMap_comp [HasRightHomology S₁] [HasRightHomology S₂] [HasRightHomology S₃]
718+
(φ₁ : S₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃) :
719+
opcyclesMap (φ₁ ≫ φ₂) = opcyclesMap φ₁ ≫ opcyclesMap φ₂ :=
720+
opcyclesMap'_comp _ _ _ _ _
721+
722+
attribute [simp] rightHomologyMap_comp opcyclesMap_comp
723+
411724
end ShortComplex
412725

413726
end CategoryTheory

‎Mathlib/Algebra/Homology/ShortExact/Abelian.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@ theorem isIso_of_shortExact_of_isIso_of_isIso (h : ShortExact f g) (h' : ShortEx
3535
(comm₂ : i₂ ≫ g' = g ≫ i₃ := by aesop_cat) [IsIso i₁] [IsIso i₃] : IsIso i₂ := by
3636
obtain ⟨_⟩ := h
3737
obtain ⟨_⟩ := h'
38-
refine @Abelian.isIso_of_isIso_of_isIso_of_isIso_of_isIso 𝒜 _ _ 0 _ _ _ 0 _ _ _ 0 f g 0 f' g'
38+
refine @Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono 𝒜 _ _ 0 _ _ _ 0 _ _ _ 0 f g 0 f' g'
3939
0 i₁ i₂ i₃ ?_ comm₁ comm₂ 0 0 0 0 0 ?_ ?_ ?_ ?_ ?_ ?_ ?_ _ _ _ _
4040
all_goals try simp
4141
all_goals try assumption

‎Mathlib/AlgebraicGeometry/Morphisms/RingHomProperties.lean‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -501,8 +501,6 @@ theorem source_affine_openCover_iff {X Y : Scheme.{u}} (f : X ⟶ Y) [IsAffine Y
501501
· have h := (hP.affine_openCover_TFAE f).out 1 0
502502
apply h.mp
503503
use 𝒰
504-
use inferInstance
505-
exact H
506504
#align ring_hom.property_is_local.source_affine_open_cover_iff RingHom.PropertyIsLocal.source_affine_openCover_iff
507505

508506
theorem isLocal_sourceAffineLocally : (sourceAffineLocally @P).IsLocal :=

0 commit comments

Comments
 (0)