English
If Q is in a commutative square with V monadic on the right, and R has a left adjoint, then Q has a left adjoint.
Русский
Если в коммутативном квадрате справа V монадический, и R имеет левое сопряжение, то Q имеет левое сопряжение.
LaTeX
$$$$\\text{If } V \\text{ is monadic and } R \\text{ has a left adjoint, then } Q \\text{ has a left adjoint}. $$$$
Lean4
/-- The homset equivalence which helps show that `L` is a left adjoint. -/
@[simps!]
noncomputable def constructRightAdjointEquiv [∀ X : B, RegularMono (adj₁.unit.app X)] (Y : C) (X : B) :
(Y ⟶ constructRightAdjointObj _ _ adj₁ adj₂ X) ≃ (L.obj Y ⟶ X) :=
calc
(Y ⟶ constructRightAdjointObj _ _ adj₁ adj₂ X) ≃
{ f : Y ⟶ U'.obj (F.obj X) // f ≫ U'.map (F.map (adj₁.unit.app X)) = f ≫ (otherMap _ _ adj₁ adj₂ X) } :=
Fork.IsLimit.homIso (limit.isLimit _) _
_ ≃ { g : F.obj (L.obj Y) ⟶ F.obj X // F.map (adj₁.unit.app _ ≫ U.map g) = g ≫ F.map (adj₁.unit.app _) } :=
by
apply (adj₂.homEquiv _ _).symm.subtypeEquiv _
intro f
rw [← (adj₂.homEquiv _ _).injective.eq_iff, eq_comm, otherMap, ← adj₂.homEquiv_naturality_right_symm,
adj₂.homEquiv_unit, ← adj₂.unit_naturality_assoc, adj₂.homEquiv_counit]
simp
_ ≃
{ z : L.obj Y ⟶ U.obj (F.obj X) //
z ≫ U.map (F.map (adj₁.unit.app X)) = z ≫ adj₁.unit.app (U.obj (F.obj X)) } :=
by
apply (adj₁.homEquiv _ _).subtypeEquiv
intro g
rw [← (adj₁.homEquiv _ _).injective.eq_iff, adj₁.homEquiv_unit, adj₁.homEquiv_unit, adj₁.homEquiv_unit, eq_comm]
simp
_ ≃ (L.obj Y ⟶ X) := (Fork.IsLimit.homIso (unitEqualises adj₁ X) _).symm
